Encyclopedia Masses Masses Mass Genesis T10 Run Cone Terminal Wall

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Run Cone Terminal Wall

A machine-checked proof shows that the mass ladder's target value cannot be built from the ledger's own run data, closing a gap in the framework's derivation.

Verify this page

The run-cone wall

The golden ratio φ appears throughout the Recognition Science framework, most importantly as the ratio between rungs on the mass ladder. A particle's mass is tied to a specific power of φ, and the framework's goal is to derive that power from the ledger, a discrete record of recognition events. The module called T10RunConeTerminalWall addresses a precise question: can the target value, φ²¹·(√2/4), be constructed from the run data alone, using only the operations the ledger's own theorems employ?

The answer is no. The module defines a run cone, the set of all real numbers reachable from the ledger's raw data (rational constants like 1, 2, and 16, plus √2 from the holonomy transport) using only field operations and natural powers. It then proves a theorem: no element of this pure run cone equals the target value. The proof works by showing every pure-cone element lives in the field ℚ(√2), while the target value does not. The target contains √5, and a separate calculation shows φ²¹ = 12238 + 5473√5, which cannot be expressed as a + b√2 with rational a and b.

This result has a direct consequence for the framework's structure. An organ arrow is a proposed rule that assigns a level to each octave of the ledger, and the framework requires such rules to satisfy a coupling interface. The module proves that any organ arrow whose levels all lie in the pure run cone fails this interface at every octave. In plain terms, the ledger's own run data cannot generate the missing piece of the mass derivation; the target must come from elsewhere, specifically from the modular operator's spectrum where φ already resides as the cross-rung transport ratio.

The module also handles the J-cost fragment, the term cosh 1 − 1 that represents the per-post recognition cost. It proves that any integer multiple of this term lies in the J-cone, but the full closure of that cone is left to successor modules. The bundled theorem, run_cone_terminal_wall, combines the pure-cone exclusion, the organ-arrow failure, and the J-cost registration into one statement. A separate census script, an instrument rather than a theorem, guards the sweep of run-derived declarations to ensure no new generator slips in unnoticed.

What this establishes is a boundary. The framework's derivation of the mass ladder cannot be completed from the ledger's run data alone; the missing organ must draw on the modular spectrum, which is anchor-family data. This is not a failure but a clarification of where the derivation must look. The wall is terminal for the run cone, and the path forward is already marked by the successor modules that close the J-cost fragment and the full cone.

THEOREM runConePure_ne_intended · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
runConePure_ne_intended · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:405 
/-- No element of the pure run-record cone equals the factor amplitude. -/
theorem runConePure_ne_intended {x : ℝ} (h : RunCone false x) :
    x ≠ intendedGapOneFactorAmplitude :=
  fun hx => intended_not_in_QsqrtTwo (hx ▸ runConePure_inQsqrtTwo h)
THEOREM runConePure_inQsqrtTwo · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
runConePure_inQsqrtTwo · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:244 
theorem runConePure_inQsqrtTwo {x : ℝ} (h : RunCone false x) : InQsqrtTwo x := by
  have hr : ∀ {j : Bool} {x : ℝ}, RunCone j x → j = false → InQsqrtTwo x := by
    intro j x h
    induction h with
    | rat _ q => intro _; exact inQsqrtTwo_rat q
    | sqrtTwo _ => intro _; exact inQsqrtTwo_sqrtTwo
    | jcost => intro hj; simp at hj
    | add _ _ ihx ihy => intro hj; exact inQsqrtTwo_add (ihx hj) (ihy hj)
    | neg _ ihx => intro hj; exact inQsqrtTwo_neg (ihx hj)
    | mul _ _ ihx ihy => intro hj; exact inQsqrtTwo_mul (ihx hj) (ihy hj)
    | inv _ hx0 ihx => intro hj; exact inQsqrtTwo_inv (ihx hj) hx0
    | pow _ n ihx => intro hj; exact inQsqrtTwo_pow n (ihx hj)
  exact hr h rfl
THEOREM intended_not_in_QsqrtTwo · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
intended_not_in_QsqrtTwo · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:319 
theorem intended_not_in_QsqrtTwo : ¬ InQsqrtTwo intendedGapOneFactorAmplitude := by
  rintro ⟨a, b, hf⟩
  have hmul := two_sqrt_two_mul_intended
  rw [hf, phi21_eq] at hmul
  have hsq2 : Real.sqrt 2 * Real.sqrt 2 = 2 := Real.mul_self_sqrt (by norm_num)
  have hexp : 2 * Real.sqrt 2 * ((a : ℝ) + (b : ℝ) * Real.sqrt 2) =
      4 * (b : ℝ) + 2 * (a : ℝ) * Real.sqrt 2 := by
    calc 2 * Real.sqrt 2 * ((a : ℝ) + (b : ℝ) * Real.sqrt 2)
        = 2 * (a : ℝ) * Real.sqrt 2 +
            2 * (b : ℝ) * (Real.sqrt 2 * Real.sqrt 2) := by ring
      _ = 4 * (b : ℝ) + 2 * (a : ℝ) * Real.sqrt 2 := by rw [hsq2]; ring
  rw [hexp] at hmul
  have hsqrt5_irr : Irrational (Real.sqrt 5) :=
    Nat.Prime.irrational_sqrt (by norm_num : Nat.Prime 5)
  by_cases ha : a = 0
  · subst ha
    simp only [Rat.cast_zero, zero_mul, mul_zero, add_zero] at hmul
    have h5 : Real.sqrt 5 = (((4 * b - 12238 : ℚ) / 5473 : ℚ) : ℝ) := by
      push_cast
      rw [eq_div_iff (by norm_num : (5473 : ℝ) ≠ 0)]
      linarith [hmul]
    exact hsqrt5_irr ⟨_, h5.symm⟩
  · have ha0 : (a : ℝ) ≠ 0 := by exact_mod_cast ha
    have hd0 : (5473 / (2 * a) : ℚ) ≠ 0 :=
      div_ne_zero (by norm_num) (mul_ne_zero (by norm_num) ha)
    have hmul' : 2 * (a : ℝ) * Real.sqrt 2 =
        (12238 - 4 * (b : ℝ)) + 5473 * Real.sqrt 5 := by
      linarith [hmul]
    have hsqrt2 : Real.sqrt 2 =
        (((12238 - 4 * b) / (2 * a) : ℚ) : ℝ) +
        ((5473 / (2 * a) : ℚ) : ℝ) * Real.sqrt 5 := by
      have h2 : Real.sqrt 2 =
          ((12238 - 4 * (b : ℝ)) + 5473 * Real.sqrt 5) / (2 * (a : ℝ)) := by
        rw [eq_div_iff (mul_ne_zero (by norm_num : (2 : ℝ) ≠ 0) ha0)]
        linarith [hmul']
      rw [h2]
      push_cast
      rw [div_mul_eq_mul_div, div_add_div_same]
    have hsq5 : (Real.sqrt 5) ^ 2 = 5 := Real.sq_sqrt (by norm_num)
    have hsq : (2 : ℝ) = (((12238 - 4 * b) / (2 * a) : ℚ) : ℝ) ^ 2 +
        5 * (((5473 / (2 * a) : ℚ) : ℝ) ^ 2) +
        2 * (((12238 - 4 * b) / (2 * a) : ℚ) : ℝ) *
          (((5473 / (2 * a)) : ℚ) : ℝ) * Real.sqrt 5 := by
      have h1 : (Real.sqrt 2) ^ 2 =
          ((((12238 - 4 * b) / (2 * a) : ℚ) : ℝ) +
          ((5473 / (2 * a) : ℚ) : ℝ) * Real.sqrt 5) ^ 2 := by rw [hsqrt2]
      rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)] at h1
      refine h1.trans ?_
      rw [add_sq, mul_pow, hsq5]
      ring
    by_cases hc : ((12238 - 4 * b) / (2 * a) : ℚ) = 0
    · have h2d : (2 : ℝ) = 5 * (((5473 / (2 * a)) : ℚ) : ℝ) ^ 2 := by
        rw [hc] at hsq
        simpa using hsq
      have h10 : ((5 * (5473 / (2 * a)) : ℚ) : ℝ) ^ 2 = (10 : ℝ) := by
        push_cast at h2d ⊢
        have h25 : (5 * (5473 / (2 * (a : ℝ)))) ^ 2 =
            25 * ((5473 / (2 * (a : ℝ))) ^ 2) := by ring
        rw [h25]
        linarith [h2d]
      exact rat_sq_ne_nat not_isSquare_ten h10
    · have hCD : (2 : ℝ) * ((((12238 - 4 * b) / (2 * a) : ℚ) : ℝ) *
          (((5473 / (2 * a)) : ℚ) : ℝ)) ≠ 0 :=
        mul_ne_zero (by norm_num : (2 : ℝ) ≠ 0)
          (mul_ne_zero (by exact_mod_cast hc) (by exact_mod_cast hd0))
      have h5r : Real.sqrt 5 =
          (((2 - ((12238 - 4 * b) / (2 * a) : ℚ) ^ 2 -
            5 * ((5473 / (2 * a) : ℚ)) ^ 2) /
            (2 * ((12238 - 4 * b) / (2 * a) : ℚ) * ((5473 / (2 * a) : ℚ))) :
            ℚ) : ℝ) := by
        have h1 : (((2 - ((12238 - 4 * b) / (2 * a) : ℚ) ^ 2 -
              5 * ((5473 / (2 * a) : ℚ)) ^ 2) /
              (2 * ((12238 - 4 * b) / (2 * a) : ℚ) * ((5473 / (2 * a) : ℚ))) :
              ℚ) : ℝ) =
            (2 - (((12238 - 4 * b) / (2 * a) : ℚ) : ℝ) ^ 2 -
              5 * (((5473 / (2 * a)) : ℚ) : ℝ) ^ 2) /
              ((2 : ℝ) * ((((12238 - 4 * b) / (2 * a) : ℚ) : ℝ) *
                (((5473 / (2 * a)) : ℚ) : ℝ))) := by
          push_cast
          ring
        rw [h1, eq_div_iff hCD]
        linarith [hsq]
      exact hsqrt5_irr ⟨_, h5r.symm⟩
THEOREM conePure_organ_fails_interface · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
conePure_organ_fails_interface · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:410 
/-- Any organ arrow whose level is pure-cone valued at every octave
fails the four-witness interface at every octave. -/
theorem conePure_organ_fails_interface
    (A : OrganArrowReduction.OrganArrow)
    (hA : ∀ o : Q3SettledLedgerOctave, RunCone false (A.level (A.W o)))
    (o : Q3SettledLedgerOctave) :
    ¬ RunPatternScaleCouplingInterface A.filter o := by
  intro hiface
  have hlevel := ((OrganArrowReduction.organArrow_interface_iff A o).1 hiface).1
  exact runConePure_ne_intended (hA o) hlevel
THEOREM coneJ_atomic · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
coneJ_atomic · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:445 
theorem coneJ_atomic (K : ℕ) : RunCone true ((K : ℝ) * (Real.cosh 1 - 1)) := by
  exact_mod_cast RunCone.mul (RunCone.rat true (K : ℚ)) RunCone.jcost

What this page does not claim

This module does not prove the J-cost fragment is closed; that is left to successor modules. This module does not derive the target value φ²¹·(√2/4) from the run cone. This module does not introduce a new provenance predicate beyond the cone 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/T10RunConeTerminalWall.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