Masses Mass Genesis T10 Sqrt2 Source Intended Eq Phi21 Div4 Mul Sqrt Eigen

Where the square root of two enters

The square root of two, about 1.41421, is a number that appears throughout geometry as the diagonal of a unit square. In the Recognition Science account of particle masses, a candidate value for an absolute scale factor was flagged as suspicious because it contained this root. The suspicion was that the root had been inserted by hand, outside the framework's own logic. The declaration intended_eq_phi21_div4_mul_sqrtEigen resolves that suspicion by proving the candidate is not a new number at all: it is exactly the framework's intended amplitude, just written in a form that exposes the root.

The proof works by factoring the candidate. The value is phi^21 * sqrt(2) / 4, where phi is the golden ratio, about 1.61803. The declaration proves this equals the intended amplitude, which was already banked as the positive number whose square is phi^42 / 8. The factorization is exact, not approximate. The root is not an extra ingredient; it is the same quantity expressed with a square root sign. The declaration also proves the root enters through a specific mechanism: it is one quarter times the eigenvalue of a modular square-root operator, an object the framework forces to have eigenvalue sqrt(2).

What the declaration does not claim is just as important. It does not prove that the candidate value is the true absolute scale of the framework. That question is left open, explicitly marked as a conjecture layer. The declaration only names where the square root of two can enter, with machine-checked proofs, and shows that this particular route is the one that carries the candidate's root. A second route, through odd-length transport traces, also carries sqrt(2), but the proof shows that route provably cannot produce the candidate's value, because those traces are sqrt(2) times dyadic rationals while the candidate's prefactor phi^21/4 is irrational.

The practical consequence is that a number which looked like an unwelcome intrusion is certified as the framework's own intended amplitude, with its root traced to a forced eigenvalue. The framework's library of formal theorems establishes the factorization and the source of the root, while the larger question of whether this candidate is the actual scale remains a target for future work.

/-- **The tainted candidate IS the banked intended amplitude.** The banked
gap-one factor amplitude `f` satisfies `f^2 = phi^42/8`
(`gapOne_factorAmplitude_sq_eq_phi42_div_eight`) and `f > 0`
(`gapOne_factorAmplitude_pos`), so `f = sqrt(phi^42/8) =
phi^21 * sqrt2 / 4`: the tainted value is not a new number, it is the
intended amplitude written off-field. -/
theorem intended_eq_tainted : intendedGapOneFactorAmplitude = taintedAmplitude := by
  have hpos : 0 < intendedGapOneFactorAmplitude := by
    simpa [intendedGapOneFactorAmplitude] using gapOne_factorAmplitude_pos
  have hsq : intendedGapOneFactorAmplitude ^ 2 = Constants.phi ^ 42 / 8 := by
    simpa [intendedGapOneFactorAmplitude] using
      gapOne_factorAmplitude_sq_eq_phi42_div_eight
  have hsqrt : intendedGapOneFactorAmplitude = Real.sqrt (Constants.phi ^ 42 / 8) := by
    rw [← hsq]
    exact (Real.sqrt_sq hpos.le).symm
  rw [hsqrt]
  exact tainted_factorization

/-- **Task 2(i), factorization form.** The tainted amplitude is the
rational-phi scalar `phi^21/4` times the modular square root's posted-rung
eigenvalue `sqrtEigenvalue a 0 0 = sqrt(modularEigenvalue a 0 0) = sqrt 2`
(the eigenvalue `2` forced by the shared event functional). -/
theorem tainted_eq_phi21_div4_mul_sqrtEigen {a : ℝ} (ha : a ≠ 0) :
    taintedAmplitude = (Constants.phi ^ 21 / 4) * sqrtEigenvalue a 0 0 := by
  show Constants.phi ^ 21 * Real.sqrt 2 / 4 = _
  rw [sqrtEigen_00 ha]
  ring

/-- **Discrimination (THEOREM).** The tainted amplitude is NOT an odd-length
transport trace: every odd `2k+1` trace is `m * sqrt2 / 2^k` for an integer
`m` (`holonomyTrace_odd`), and equality would force `phi^21 = 4m/2^k` into
the rationals, against the Fibonacci reduction `phi^21 = 10946*phi + 6765`
and `phi`'s irrationality. So mechanism (ii) provably cannot carry the
tainted candidate: mechanism (i) is THE source of its `sqrt2`. -/
theorem tainted_ne_odd_trace :
    ¬ ∃ (k : ℕ) (m : ℤ), taintedAmplitude = (m : ℝ) * Real.sqrt 2 / 2 ^ k := by
  rintro ⟨k, m, h⟩
  have hs : Real.sqrt 2 ≠ 0 := ne_of_gt (Real.sqrt_pos_of_pos (by norm_num))
  have hp2 : (2 : ℝ) ^ k ≠ 0 := pow_ne_zero k (by norm_num)
  have ht : taintedAmplitude = Constants.phi ^ 21 * Real.sqrt 2 / 4 := rfl
  rw [ht, div_eq_iff (by norm_num : (4 : ℝ) ≠ 0), div_mul_eq_mul_div,
    eq_div_iff hp2] at h
  have key : (Constants.phi ^ 21 * (2 : ℝ) ^ k) * Real.sqrt 2 =
      (4 * (m : ℝ)) * Real.sqrt 2 := by
    linear_combination h
  have h3 : Constants.phi ^ 21 * (2 : ℝ) ^ k = 4 * (m : ℝ) :=
    mul_right_cancel₀ hs key
  have hf21 : Constants.phi ^ 21 = 10946 * Constants.phi + 6765 := by
    have hf := phi_pow_fib 21
    rw [show Nat.fib 21 = 10946 from by decide,
      show Nat.fib 22 = 17711 from by decide] at hf
    push_cast at hf
    linear_combination hf
  have key2 : (10946 * (2 : ℝ) ^ k) * Constants.phi =
      4 * (m : ℝ) - 6765 * (2 : ℝ) ^ k := by
    linear_combination h3 - (2 : ℝ) ^ k * hf21
  have hden : (10946 * (2 : ℝ) ^ k) ≠ 0 := ne_of_gt (by positivity)
  have hphirat : Constants.phi =
      (((4 * (m : ℚ) - 6765 * (2 : ℚ) ^ k) / (10946 * (2 : ℚ) ^ k) : ℚ) : ℝ) := by
    push_cast
    rw [eq_div_iff hden]
    linear_combination key2
  exact Constants.phi_irrational ⟨_, hphirat.symm⟩

What this page does not claim

The candidate value is the true absolute scale of the framework. The square root of two enters only through the modular square-root mechanism; odd-length transport also carries it. The declaration proves any claim about measured particle masses.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: