Encyclopedia Masses Masses Mass Genesis T10 Run Cone Terminal Wall Two Sqrt Two Mul Intended

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Run Cone Terminal Wall Two Sqrt Two Mul Intended

A single number, the intended gap factor, is shown to be unreachable by the pure arithmetic of run records, forcing a new ingredient into the mass derivation.

Verify this page

The intended gap factor

The intended gap factor is a real number that the Recognition Science framework's mass derivation needs. The declaration two_sqrt_two_mul_intended proves a precise relation: twice the square root of two times this factor equals the golden ratio raised to the twenty-first power. In symbols, 2√2 · f = φ²¹. The factor itself is not named by this declaration; the relation is what it establishes.

The proof is a short chain. The library first shows that φ²¹ equals 12238 + 5473√5, a number in the field Q(√5). It then uses a previously banked identity, f² = φ⁴²/8, together with the fact that f is positive, to take square roots and obtain the relation. The declaration is a theorem in the machine-checked library of formal theorems, meaning the steps are verified by a computer proof checker.

What the declaration does not claim is that f itself is a simple number like √2 or a rational. In fact, the same module proves the opposite: f is not in the field Q(√2). This matters because the run cone, the set of numbers derivable from pure ledger-run data, is built only from rationals, √2, and field operations. Since f is not in that field, no pure run-derived number can equal it. The declaration is the key step in that separation.

In Recognition Science, the framework models a ledger as a discrete record of events, and the run cone is the set of real numbers that can be generated from such records alone. The declaration shows that the intended gap factor lies outside this cone, meaning that the mass derivation cannot proceed from run data alone. It forces the framework to introduce a new ingredient, the J-cost, to reach the target. The declaration is therefore a boundary marker: it defines what the pure run record cannot do, and it sets up the next stage of the derivation.

THEOREM two_sqrt_two_mul_intended · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
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]
THEOREM phi21_eq · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean
phi21_eq · IndisputableMonolith/Masses/MassGenesis/T10RunConeTerminalWall.lean:286 
theorem phi21_eq :
    Constants.phi ^ (21 : ℕ) = 12238 + 5473 * Real.sqrt 5 := by
  have hfib21 : Nat.fib 21 = 10946 := by decide
  have hfib20 : Nat.fib 20 = 6765 := by decide
  have h := phi_pow_succ_eq 20
  rw [hfib21, hfib20] at h
  have h21 : (20 + 1 : ℕ) = 21 := rfl
  rw [h21] at h
  rw [h]
  show (10946 : ℝ) * ((1 + Real.sqrt 5) / 2) + (6765 : ℝ) = _
  ring
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 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)

What this page does not claim

This answer does not claim that the intended gap factor is a measured physical quantity. This answer does not claim that the declaration itself proves the full mass derivation, only a boundary step within it. This answer does not claim that the run cone is the only possible set of run-derived numbers; the declaration concerns the registered cone.

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