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

ARTICLE 5 claims 5 theorems

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

A suspicious number in a particle mass formula turns out to be the intended amplitude, with its irrational factor traced to a forced eigenvalue.

Verify this page

The source of sqrt2

In the Recognition Science framework, particle masses are built from a ladder of powers of the golden ratio phi, roughly 1.618. A candidate absolute scale appeared that looked out of place: it contained the square root of 2, an irrational number that does not belong to the field generated by phi. The declaration tainted_eq_phi21_div4_mul_sqrtEigen is a machine-checked theorem that identifies where that sqrt2 comes from. It establishes that the candidate amplitude equals (phi^21 / 4) times the square root of 2, and that this factor is exactly the eigenvalue of a certain modular operator forced by the framework's shared event functional.

The result is a factorization, not a new discovery of a number. The tainted candidate, written as phi^21 * sqrt2 / 4, is shown to be identical to the framework's banked intended gap-one factor amplitude, which satisfies f^2 = phi^42 / 8 and is positive. The theorem intended_eq_tainted establishes this equality. So the candidate is not a foreign intruder; it is the intended amplitude written in a form that exposes its irrational component. The off-field factor sqrt2 / 4 is certified to lie outside the rational-phi field, meaning it cannot be expressed as p + q*phi with rational p and q, a fact established in sqrt2_div_four_not_inQPhi.

The framework then discriminates between two possible carriers of sqrt2. The first is the modular square root, whose eigenvalue sqrt2 is forced by the posted rung's eigenvalue 2. The second is odd-length transport, where traces of walks of odd length are dyadic multiples of sqrt2. The theorem tainted_ne_odd_trace establishes that the candidate cannot be an odd trace, because its prefactor phi^21/4 is irrational while odd traces are sqrt2 times dyadic rationals. This leaves the modular square root as the unique source of the candidate's sqrt2, a conclusion bundled in the theorem sqrt2_source_verdict.

What this does not claim is equally important. The theorem does not decide whether the tainted candidate is the true absolute scale of particle masses; that question remains open, flagged as a conjecture layer. The framework only names where sqrt2 can enter, with proofs, and does not strengthen any wall. The closed 8-beat spectrum, meanwhile, provably excludes sqrt2, so the mechanism is specific to open or odd-length structures. This is a precise provenance result, not a physical prediction.

THEOREM tainted_eq_phi21_div4_mul_sqrtEigen · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
tainted_eq_phi21_div4_mul_sqrtEigen · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean:109 
/-- **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
THEOREM intended_eq_tainted · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
intended_eq_tainted · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean:89 
/-- **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
THEOREM sqrt2_div_four_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
sqrt2_div_four_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean:125 
/-- The off-field factor `sqrt2/4` is outside the rational-phi field:
a representation would give `sqrt2 = 4p + 4q*phi ∈ Q(phi)`, against the
banked C1 escape clause. -/
theorem sqrt2_div_four_not_inQPhi : ¬ InQPhi (Real.sqrt 2 / 4) := by
  rintro ⟨p, q, hpq⟩
  apply sqrt_two_not_inQPhi
  refine ⟨4 * p, 4 * q, ?_⟩
  push_cast
  linear_combination 4 * hpq
THEOREM tainted_ne_odd_trace · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
tainted_ne_odd_trace · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean:169 
/-- **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⟩
THEOREM closed8_holonomyTrace_ne_sqrt2 · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
closed8_holonomyTrace_ne_sqrt2 · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean:207 
/-- **Closed-open contrast (THEOREM).** No admissible closed 8-beat cascade
has holonomy trace `sqrt2` or `-sqrt2`: the closed spectrum is
`{-2, -1, 0, 1, 2}` (Task 1) while `1.4 < sqrt2 < 1.5`. This is the
kernel-checked form of C7's "sqrt2 occurs zero times". -/
theorem closed8_holonomyTrace_ne_sqrt2 {w : Walk} (hw : w ∈ closedWalks8) :
    holonomyTrace w ≠ Real.sqrt 2 ∧ holonomyTrace w ≠ -Real.sqrt 2 := by
  have h14 : (1.4 : ℝ) < Real.sqrt 2 := by
    rw [Real.lt_sqrt (by norm_num : (0 : ℝ) ≤ 1.4)]
    norm_num
  have h15 : Real.sqrt 2 < (1.5 : ℝ) := by
    rw [Real.sqrt_lt' (by norm_num : (0 : ℝ) < 1.5)]
    norm_num
  rcases holonomyTrace_mem_closed hw with h | h | h | h | h <;>
    (rw [h]; constructor <;> intro heq <;> linarith)

What this page does not claim

The theorem does not establish that the tainted candidate is the true absolute scale of particle masses. The theorem does not claim that odd-length transport traces are irrelevant to the framework; it only excludes them as the source of this particular amplitude's sqrt2. The theorem does not derive the value of the fine-structure constant or any other coupling constant.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND