Encyclopedia Masses Masses Mass Genesis T10 Run Cone Terminal Wall Intended Not In Qsqrt Two

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Run Cone Terminal Wall Intended Not In Qsqrt Two

A machine-checked proof shows that a candidate mass value cannot be built from the simple numbers a ledger of events would supply, ruling out an entire family of explanations.

Verify this page

The number outside the field

The declaration intended_not_in_QsqrtTwo concerns a specific real number, written intendedGapOneFactorAmplitude, which the framework's mass-genesis work identifies as a candidate for a physical amplitude. The proof shows this number does not belong to the field ℚ(√2), the set of all numbers that can be written as a + b√2 where a and b are rational numbers. In plain terms, no amount of adding, subtracting, multiplying, dividing, or raising to whole-number powers of ordinary fractions and the square root of two can produce this candidate value.

The argument runs through a chain of equalities. The framework's library proves that 2√2 times the candidate equals φ²¹, where φ is the golden ratio. It also proves φ²¹ equals 12238 + 5473√5. If the candidate were in ℚ(√2), then φ²¹ would have to be expressible as 4b + 2a√2 for rational a and b. That would force either √5 to be rational, or √2 to be a rational combination of √5 and 1, or a rational square root of 10. Each of these is impossible, since 2, 5, and 10 are not perfect squares. The contradiction completes the proof.

This result matters because it closes a specific door. The framework builds a run cone, a formal collection of numbers that can be derived purely from a discrete record of posting events, using only rational constants, √2 from a holonomy trace, and field operations. The theorem runConePure_ne_intended states that no number in this pure cone equals the candidate. Consequently, any attempt to construct the candidate amplitude from ledger-run data alone, without invoking the framework's recognition cost, fails. The proof also implies that any organ arrow whose level takes values only in the pure cone cannot satisfy a required four-witness interface at any octave.

In Recognition Science, this is a terminal wall for a specific reduction path. The declaration does not claim the candidate is impossible or unphysical; it claims the candidate is not reachable from the pure run data. The framework's broader account includes a J-cost fragment, based on the recognition cost function, which is handled by successor modules. Those modules prove that the full cone, including the J-cost term, still excludes the candidate, but that is a separate theorem. This declaration also does not claim that no run-derived real number outside the registered cone could exist; it only covers the cone as defined.

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 two_sqrt_two_mul_intended · phi21_eq · 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]
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 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 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

What this page does not claim

The declaration does not claim the candidate amplitude is impossible or unphysical, only that it is not in the pure run cone. The declaration does not claim that no run-derived real number outside the registered cone could exist. The declaration does not itself close the J-cost fragment, which is handled by successor modules.

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