Encyclopedia Masses Masses Mass Genesis T10 Sqrt2 Source

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Sqrt2 Source

A machine-checked proof identifies where the square root of two enters a candidate mass scale, and proves it cannot come from the transport sector.

Verify this page

The source of the square root of two

The square root of two is a number that appears in many geometric and algebraic settings, from the diagonal of a square to the solutions of x² = 2. In Recognition Science, a candidate absolute mass scale, called the tainted candidate, contains this number explicitly: its value is φ²¹·√2/4, where φ is the golden ratio. The question addressed by the mass genesis framework (the account of how particle masses arise from recognition events) is simple: where does that √2 come from, and can it be traced to a specific mechanism within the framework's formal structure?

The framework proves, with machine-checked theorems, that the tainted candidate is not a new number at all. It equals the already-banked intended gap-one factor amplitude, which satisfies f² = φ⁴²/8 and is positive. The proof shows that f = √(φ⁴²/8) = φ²¹·√2/4, exactly. So the tainted value is just the intended amplitude written in a form that exposes the √2 factor. The framework then identifies two mechanisms that could carry √2 into the framework: the modular square root of a certain operator eigenvalue, and odd-length transport traces. It proves that the first mechanism is the actual source for the tainted candidate, and that the second provably cannot be, because odd traces are always √2 times a dyadic rational, while the candidate's prefactor φ²¹/4 is irrational.

The key theorem, sqrt2_source_verdict, bundles the full result: the intended amplitude factors as (φ²¹/4) times the modular square root's eigenvalue (which is √2), that eigenvalue is realized by a nonzero operator, both √2/4 and the full amplitude are outside the rational-phi field, and the closed 8-beat spectrum excludes ±√2 entirely. The proof also shows that the odd-length transport sector does carry ±√2, but only as traces, not as the scalar amplitude. The distinction is sharp: the tainted candidate is a scalar with an irrational prefactor, so only the modular square root can supply its √2.

In Recognition Science, this framework establishes a precise provenance for a specific irrational number. It does not decide whether the tainted candidate is the true absolute scale; that remains an open conjecture. What it proves is that if √2 appears in the mass scale, it enters through the modular square root, not through transport. This is a step toward understanding why the framework's mass ladder involves the golden ratio and its powers, and where other irrationalities might enter. The result is a theorem in the framework's machine-checked library, with no unproved assumptions.

THEOREM taintedAmplitude · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
taintedAmplitude · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean:66 
/-- The tainted candidate's value: `a = phi^21 * sqrt2 / 4`. -/
noncomputable def taintedAmplitude : ℝ := Constants.phi ^ 21 * Real.sqrt 2 / 4
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 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 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 tainted candidate is the true absolute scale. The square root of two appears in any closed 8-beat holonomy trace. The odd-length transport sector carries the tainted amplitude itself.

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