Encyclopedia Masses Masses Mass Genesis T10 Sqrt2 Source Closed8 Holonomy Trace Ne Sqrt2

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Sqrt2 Source Closed8 Holonomy Trace Ne Sqrt2

A machine-checked theorem proves that a certain eight-step closed path can never have a trace equal to the square root of two, and explains why that matters for the framework's account of mass.

Verify this page

The closed eight-beat spectrum

The square root of two, about 1.414, is a number that appears throughout mathematics and physics. In the Recognition Science framework, a ledger, a discrete record of recognition events, gives rise to walks: sequences of steps along three axes. A closed walk returns to its starting point after a fixed number of beats. The framework's library of machine-checked formal theorems proves a sharp fact about closed walks of eight beats: none of them has a holonomy trace equal to the square root of two, and none has a trace equal to its negative.

The theorem, named closed8_holonomyTrace_ne_sqrt2, states this exclusion precisely. For any admissible closed walk of length eight, the holonomy trace, a number that records how a vector is rotated and scaled after the walk, is never the square root of two and never its negative. The proof is short. The framework's earlier work shows that the closed eight-beat spectrum, the set of all possible traces, is exactly the five integers minus two, minus one, zero, one, and two. Since the square root of two lies strictly between 1.4 and 1.5, it cannot be any of those five integers. The same argument rules out its negative.

This exclusion is one piece of a larger result about where the square root of two can enter the framework's account of particle masses. A candidate value for a mass-scale amplitude, called the tainted candidate, is the number phi to the 21st power times the square root of two, divided by four. The theorem shows that this candidate's square root of two cannot come from any closed eight-beat walk, because the closed spectrum simply does not contain it. Instead, the framework proves that the candidate's square root of two enters through a different mechanism: a modular square root operator whose forced eigenvalue is exactly the square root of two. The closed-walk exclusion is what rules out one possible source, leaving the modular operator as the only proved carrier of this particular amplitude's square root of two.

What the theorem does not claim is equally important. It does not say that the tainted candidate is the true absolute mass scale of the framework. That question remains open at the conjecture layer. It does not say that the square root of two never appears in any walk; odd-length open walks, which do not return to their start, provably do carry the square root of two in their traces. The theorem only draws a clean boundary around the closed eight-beat sector, and that boundary is what lets the framework name the modular operator as the source of the candidate's square root of two.

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)
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)
THEOREM sqrt2_source_verdict · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean
sqrt2_source_verdict · IndisputableMonolith/Masses/MassGenesis/T10Sqrt2Source.lean:224 
/-- **The C8 Task-2 verdict (THEOREM).** Two mechanisms carry `sqrt2`:

(i) **the C1 modular square root** — the tainted candidate's value is the
banked intended gap-one factor amplitude, its off-field factor `sqrt2/4`
is `(1/4)` times the modular square root's forced posted-rung eigenvalue
(`sqrt(eigenvalue 2)`), that eigenvalue is realized by an eigen-operator,
and both the factor and the full amplitude are certified off the
rational-phi field;

(ii) **odd-length / open transport** — odd traces are dyadic multiples of
`sqrt2` with `±sqrt2` realized at beat counts 1 and 3;

while the closed 8-beat spectrum provably excludes `±sqrt2`, and the odd
sector provably cannot carry the tainted candidate itself
(`tainted_ne_odd_trace`: odd traces are `sqrt2` times DYADIC rationals, but
the candidate's prefactor `phi^21/4` is irrational).

The candidate's value is a SCALAR with an irrational prefactor, so mechanism
(i) is THE source of its `sqrt2`; mechanism (ii) is a second, independent
carrier of `sqrt2` in the transport sector, but not of this amplitude.
Whether the tainted candidate is the true absolute scale is NOT decided
here (CONJECTURE-layer); this theorem names where `sqrt2` enters. -/
theorem sqrt2_source_verdict {a : ℝ} (ha : a ≠ 0) :
    (intendedGapOneFactorAmplitude = (Constants.phi ^ 21 / 4) * sqrtEigenvalue a 0 0 ∧
      (∃ X : M4, X ≠ 0 ∧ relativeModularSqrt a X = ((Real.sqrt 2 : ℝ) : ℂ) • X) ∧
      ¬ InQPhi (Real.sqrt 2 / 4) ∧ ¬ InQPhi taintedAmplitude) ∧
    (holonomyTrace [0] = Real.sqrt 2 ∧ holonomyTrace [0, 2, 1] = Real.sqrt 2 ∧
      holonomyTrace [0, 0, 0] = -Real.sqrt 2 ∧
      (∀ (k : ℕ) (w : Walk), w.length = 2 * k + 1 →
        (2 : ℝ) ^ k * holonomyTrace w = ((qProd w).w : ℝ) * Real.sqrt 2)) ∧
    (∀ w ∈ closedWalks8, holonomyTrace w ≠ Real.sqrt 2 ∧
      holonomyTrace w ≠ -Real.sqrt 2) ∧
    ¬ ∃ (k : ℕ) (m : ℤ), taintedAmplitude = (m : ℝ) * Real.sqrt 2 / 2 ^ k :=
  ⟨⟨intended_eq_phi21_div4_mul_sqrtEigen ha, sqrt_two_mem_sqrt_spectrum ha,
      sqrt2_div_four_not_inQPhi, tainted_not_inQPhi⟩,
    ⟨holonomyTrace_single 0, holonomyTrace_xzy, holonomyTrace_xxx,
      fun k w hw => holonomyTrace_odd k w hw⟩,
    (fun _w hw => closed8_holonomyTrace_ne_sqrt2 hw),
    tainted_ne_odd_trace⟩

What this page does not claim

The tainted candidate is the true absolute mass scale; that question remains open at the conjecture layer. The square root of two never appears in any walk; odd-length open walks provably carry it in their traces. The theorem explains why the square root of two appears in the tainted candidate; that explanation is a separate result.

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