Encyclopedia Masses Masses Mass Genesis T10 Run Cone Terminal Wall Cone Pure Organ Fails Interface

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Run Cone Terminal Wall Cone Pure Organ Fails Interface

A machine-checked theorem shows that a certain class of mass-generating rules cannot produce the target mass value, closing a specific gap in a derivation chain.

Verify this page

The pure-cone wall

The declaration conePure_organ_fails_interface is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns organ arrows, which are rules that assign a numerical level to each octave in a settled ledger, a discrete record of accounting events. The theorem states that if an organ arrow's level at every octave is a value drawn from a particular set called the pure run cone, then that arrow necessarily fails to satisfy a specific coupling interface, a required relationship between its filter and its level, at every octave.

The pure run cone is a precisely defined collection of real numbers. It contains the rational numbers, the square root of 2, and everything obtainable from these by the ordinary field operations of addition, subtraction, multiplication, division, and taking natural powers. Importantly, it does not contain the golden ratio φ, and it does not contain the specific target value that the framework is trying to derive for a mass-generation parameter. The theorem's proof works by showing that the target value, which is φ²¹ times (√2/4), cannot be expressed in the form a + b√2 with rational a and b, while every element of the pure run cone can be so expressed.

In Recognition Science, the framework models the genesis of particle masses as a process of recognition events recorded in a ledger. The target value, called intendedGapOneFactorAmplitude, is the specific number that the framework's derivation chain aims to produce for a mass-related quantity. The theorem establishes a negative result: no rule that draws its levels exclusively from the pure run cone can hit this target. This is a wall, not a path; it shows that any successful rule must incorporate something beyond the pure ledger data, such as the J-cost fragment, which is a separate component related to the cost of recognition.

The theorem does not claim that no organ arrow can ever produce the target value. It only rules out those arrows whose levels come from the pure run cone. The framework's successor modules address this by expanding the allowed set of values to include the J-cost fragment, which is transcendental, and then proving that even with this addition, the target value still cannot be reached. The pure-cone theorem is therefore a precise, limited statement: it closes one specific avenue in the derivation, not the entire search.

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 RunCone · runConePure_inQsqrtTwo · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
RunCone · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:226 
/-- The registered run-record derivation cone. Generators: rational
settlement data at any marking, `√2` from the holonomy transport at any
marking, and the per-post J-cost `cosh 1 − 1` at the `true` marking only.
Operations: field operations and natural powers, the only operations the
run-real theorems use. -/
inductive RunCone : Bool → ℝ → Prop
  | rat (j : Bool) (q : ℚ) : RunCone j (q : ℝ)
  | sqrtTwo (j : Bool) : RunCone j (Real.sqrt 2)
  | jcost : RunCone true (Real.cosh 1 - 1)
  | add {j : Bool} {x y : ℝ} : RunCone j x → RunCone j y → RunCone j (x + y)
  | neg {j : Bool} {x : ℝ} : RunCone j x → RunCone j (-x)
  | mul {j : Bool} {x y : ℝ} : RunCone j x → RunCone j y → RunCone j (x * y)
  | inv {j : Bool} {x : ℝ} : RunCone j x → x ≠ 0 → RunCone j x⁻¹
  | pow {j : Bool} {x : ℝ} : RunCone j x → (n : ℕ) → RunCone j (x ^ n)
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 · two_sqrt_two_mul_intended · 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⟩
two_sqrt_two_mul_intended · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:298 
/-- `2√2 f = φ²¹`: both sides are positive and their squares agree by
the banked `f² = φ⁴²/8`. -/
theorem two_sqrt_two_mul_intended :
    2 * Real.sqrt 2 * intendedGapOneFactorAmplitude =
      Constants.phi ^ (21 : ℕ) := by
  have hsq : intendedGapOneFactorAmplitude ^ 2 = Constants.phi ^ (42 : ℕ) / 8 :=
    gapOne_factorAmplitude_sq_eq_phi42_div_eight
  have hsq2 : (2 * Real.sqrt 2 * intendedGapOneFactorAmplitude) ^ 2 =
      (Constants.phi ^ (21 : ℕ)) ^ 2 := by
    rw [mul_pow, mul_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2), hsq, ← pow_mul]
    ring
  have hx : 0 < 2 * Real.sqrt 2 * intendedGapOneFactorAmplitude :=
    mul_pos (mul_pos (by norm_num) (Real.sqrt_pos_of_pos (by norm_num)))
      OrganArrowReduction.intendedGapOneFactorAmplitude_pos
  have hy : 0 < Constants.phi ^ (21 : ℕ) := pow_pos Constants.phi_pos _
  rcases sq_eq_sq_iff_eq_or_eq_neg.mp hsq2 with h | h
  · exact h
  · linarith [h, hx, hy]

What this page does not claim

The theorem does not claim that no organ arrow can ever produce the target value; it only rules out those with levels in the pure run cone. The theorem does not claim that the pure run cone is the only set of values an organ arrow could use. The theorem does not claim that the target value is impossible to derive from the framework; it only closes one specific avenue.

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