Encyclopedia Masses Masses Mass Genesis T10 Rung Scalar Halving Wall Scalar Eq Phi21 Iff Mass Expone

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Rung Scalar Halving Wall Scalar Eq Phi21 Iff Mass Expone

A machine-checked proof shows that in the Recognition Science framework, a mass scalar equals φ^21 exactly when the mass exponent is 42, but it does not derive the value 55.

Verify this page

The halving wall

The golden ratio φ, approximately 1.618, appears throughout mathematics and physics. In the Recognition Science framework, particle masses are proposed to follow a ladder of φ-powers. This page examines a specific, machine-checked theorem about that ladder: the declaration scalar_eq_phi21_iff_mass_exponent_eq_42. In plain terms, it proves a conditional equivalence: if a certain positive scalar quantity q, which lives in the field of rational numbers extended by φ, satisfies a particular squaring relation with a deposit norm, then q equals φ^21 precisely when the mass exponent e equals 42.

The proof rests on a chain of formal steps. First, the framework defines a ledger, a discrete record of recognition events, and a cost, the forced price of each recognition. From these, it derives a rung, a step on the mass ladder. The theorem sqConsistent_scalar_eq_half_pow shows that if a positive scalar in Q(φ) squares to φ^e / 8, then e must be even and the scalar must equal φ^(e/2). This is the halving property: the scalar's exponent is forced to be half the mass exponent. The theorem scalar_eq_phi21_iff_mass_exponent_eq_42 applies this to the specific case where the squared scalar is φ^42 / 8, yielding the equivalence q = φ^21 ↔ e = 42.

The proof also establishes a parity constraint. The theorem not_sq_phi_pow_odd shows that no odd power of φ has a square root in Q(φ). This means a rational-φ deposit scalar can exist only at an even mass exponent. Consequently, the electroweak yardstick, a framework-internal integer related to the mass exponent by r0 = e + 13, must be odd. The frozen value 55 passes this test, while 56 is excluded.

However, the theorem does not claim to derive the value 55 itself. The framework's structural apparatus, including the halving wall, is blind to the specific yardstick beyond parity. The theorem structural_apparatus_yardstick_blind shows that the same structural package accepts both e = 42 (yardstick 55) and e = 44 (yardstick 57), an observably different world. The value 55 remains a frozen assumption, measured against the Z boson mass in October 2025, not a consequence of the forcing chain. The precise origin of the yardstick pair (B_pow, r0) is an open problem within the framework.

THEOREM scalar_eq_phi21_iff_mass_exponent_eq_42 · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
scalar_eq_phi21_iff_mass_exponent_eq_42 · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean:383 
/-- **The reduction is exact and lossless (THEOREM).** Under
square-consistency, the scalar is `phi^21` iff the mass exponent is 42:
reading `phi^21` off the amplitude is exactly the information content of the
yardstick value `r0(EW) = 55`, nothing more and nothing less. -/
theorem scalar_eq_phi21_iff_mass_exponent_eq_42 {q : ℝ} (hq : InQPhi q) (hq0 : 0 < q)
    {e : ℕ} (h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ e / 8) :
    q = Constants.phi ^ 21 ↔ e = 42 := by
  obtain ⟨he, hqeq⟩ := sqConsistent_scalar_eq_half_pow hq hq0 h
  rw [hqeq]
  constructor
  · intro hpow
    have h21 : e / 2 = 21 := (pow_right_strictMono₀ one_lt_phi).injective hpow
    obtain ⟨m, hm⟩ := he
    omega
  · intro he42
    rw [he42, show (42 : ℕ) / 2 = 21 from by norm_num]
THEOREM sqConsistent_scalar_eq_half_pow · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
sqConsistent_scalar_eq_half_pow · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean:255 
/-- **The upgrade (THEOREM).** Square-consistency forces the pure rung power:
if a positive rational-phi scalar's full-dimension deposit amplitude squares
to the mass content `phi^e / 8`, then `e` is even and the scalar is exactly
`phi^(e/2)`. The C9 rung-quantum shape is a CONSEQUENCE of the squaring on
`Q(phi)`, not an additional assumption. -/
theorem sqConsistent_scalar_eq_half_pow {q : ℝ} (hq : InQPhi q) (hq0 : 0 < q)
    {e : ℕ} (h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ e / 8) :
    Even e ∧ q = Constants.phi ^ (e / 2) := by
  have hsq : q ^ 2 = Constants.phi ^ e := (depositAmplitude_sq_eq_iff q e).mp h
  have heven : Even e := by
    by_contra hne
    exact not_sq_phi_pow_odd (Nat.not_even_iff_odd.mp hne) ⟨q, hq, hsq⟩
  refine ⟨heven, ?_⟩
  obtain ⟨m, hm⟩ := heven
  have hm2 : e / 2 = m := by omega
  have hm' : e = 2 * m := by omega
  rw [hm2]
  exact scalar_eq_half_pow_of_sq hq0.le (hm' ▸ hsq)
THEOREM not_sq_phi_pow_odd · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
not_sq_phi_pow_odd · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean:190 
/-- **The parity obstruction (THEOREM).** No odd power of `phi` is a square
in the rational-phi field: if `x^2 = phi^e` with `x = p + q phi`, then
reading off coefficients against `phi^e = F_e phi + F_{e-1}` (banked
`phi_pow_fib`) gives `A = F_{e-1}`, `B = F_e`, and the norm identity forces
`N(x)^2 = F_{e-1}^2 + F_{e-1} F_e - F_e^2 = -1` by Cassini's identity
(`Int.fib_succ_mul_fib_pred_sub_fib_sq`) with `e` odd. No rational squares
to `-1`. -/
theorem not_sq_phi_pow_odd {e : ℕ} (he : Odd e) :
    ¬ ∃ x : ℝ, InQPhi x ∧ x ^ 2 = Constants.phi ^ e := by
  rintro ⟨x, ⟨p, q, hpq⟩, hx⟩
  have h1e : 1 ≤ e := by
    obtain ⟨k, hk⟩ := he
    omega
  have hshift : (Nat.fib (e + 1) : ℤ) - (Nat.fib e : ℤ) = (Nat.fib (e - 1) : ℤ) := by
    rcases e with _ | n
    · omega
    · rw [show n + 1 + 1 = n + 2 from rfl, Nat.fib_add_two, Nat.add_sub_cancel]
      push_cast
      ring
  have hfib1 : (Nat.fib (e + 1) : ℤ) = (Nat.fib e : ℤ) + (Nat.fib (e - 1) : ℤ) := by
    rcases e with _ | n
    · omega
    · rw [show n + 1 + 1 = n + 2 from rfl, Nat.fib_add_two, Nat.add_sub_cancel]
      push_cast
      ring
  rw [hpq, sq_rep p q] at hx
  rw [phi_pow_fib e] at hx
  push_cast at hx
  have hx' : ((p ^ 2 + q ^ 2 : ℚ) : ℝ) + ((2 * p * q + q ^ 2 : ℚ) : ℝ) * Constants.phi =
      (((Nat.fib (e + 1) : ℤ) - (Nat.fib e : ℤ) : ℚ) : ℝ) +
        (((Nat.fib e : ℤ) : ℚ) : ℝ) * Constants.phi := by
    push_cast
    linear_combination hx
  obtain ⟨hA, hB⟩ := rat_coeff_unique hx'
  have hn := phiNorm_sq p q
  rw [hA, hB] at hn
  have hshiftQ : ((Nat.fib (e + 1) : ℤ) : ℚ) - ((Nat.fib e : ℤ) : ℚ) =
      ((Nat.fib (e - 1) : ℤ) : ℚ) := by
    exact_mod_cast hshift
  rw [hshiftQ] at hn
  have hcass : (Nat.fib (e - 1) : ℤ) ^ 2 + (Nat.fib (e - 1) : ℤ) * (Nat.fib e : ℤ) -
      (Nat.fib e : ℤ) ^ 2 = (-1 : ℤ) := by
    have h0 := Int.fib_succ_mul_fib_pred_sub_fib_sq (e : ℤ)
    have he1 : (e : ℤ) + 1 = ((e + 1 : ℕ) : ℤ) := by push_cast; ring
    have he2 : (e : ℤ) - 1 = ((e - 1 : ℕ) : ℤ) := by
      rcases e with _ | n
      · omega
      · rw [Nat.add_sub_cancel]
        push_cast
        ring
    rw [he1, he2, Int.fib_natCast, Int.fib_natCast, Int.fib_natCast,
      Int.natAbs_natCast, Odd.neg_one_pow he] at h0
    rw [hfib1] at h0
    linear_combination h0
  have hcassQ : ((Nat.fib (e - 1) : ℤ) : ℚ) ^ 2 +
      ((Nat.fib (e - 1) : ℤ) : ℚ) * ((Nat.fib e : ℤ) : ℚ) -
        ((Nat.fib e : ℤ) : ℚ) ^ 2 = (-1 : ℚ) := by
    exact_mod_cast hcass
  have hnorm : (p ^ 2 + p * q - q ^ 2 : ℚ) ^ 2 = (-1 : ℚ) := by
    rw [hn]
    linear_combination hcassQ
  have hnonneg : (0 : ℚ) ≤ (p ^ 2 + p * q - q ^ 2) ^ 2 := sq_nonneg _
  rw [hnorm] at hnonneg
  norm_num at hnonneg
THEOREM structural_apparatus_yardstick_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
structural_apparatus_yardstick_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean:518 
/-- **WALL 3 (THEOREM): the structural deposit apparatus is yardstick-blind
beyond parity.** The candidate at the witness exponent `e = 44` (yardstick
`r0(EW) = 57`, one step up) satisfies every banked structural test the
candidate at `e = 42` (yardstick 55) satisfies: square-consistency,
rung-quantum acceptance, doubled-decoy rejection; while the two worlds are
observably distinct. The C1-C9 structural apparatus therefore does not
discriminate `r0(EW) = 55` from `r0(EW) = 57`. Deriving 55 requires a
principle outside the structural apparatus: a sector-invariant law of the
yardstick itself. -/
theorem structural_apparatus_yardstick_blind :
    ((Constants.phi ^ 21 * creationDepositNorm) ^ 2 = Constants.phi ^ 42 / 8) ∧
      ((Constants.phi ^ 22 * creationDepositNorm) ^ 2 = Constants.phi ^ 44 / 8) ∧
      (¬ ∃ k : ℕ, 2 * (Constants.phi ^ 21 * creationDepositNorm) =
        Constants.phi ^ k * creationDepositNorm) ∧
      (¬ ∃ k : ℕ, 2 * (Constants.phi ^ 22 * creationDepositNorm) =
        Constants.phi ^ k * creationDepositNorm) ∧
      Constants.phi ^ (57 : ℤ) ≠ Constants.phi ^ (55 : ℤ) := by
  have h42 := structural_package_at_even_exponent (e := 42) ⟨21, by norm_num⟩
  have h44 := structural_package_at_even_exponent (e := 44) ⟨22, by norm_num⟩
  rw [show (42 : ℕ) / 2 = 21 from by norm_num] at h42
  rw [show (44 : ℕ) / 2 = 22 from by norm_num] at h44
  exact ⟨h42.1, h44.1, h42.2.2, h44.2.2, witness_exponent_distinct⟩

What this page does not claim

The theorem does not derive the electroweak yardstick value 55; that value remains a frozen assumption. The theorem does not prove that the framework's mass ladder matches measured particle masses. The theorem does not apply to scalars outside the field Q(φ).

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/T10RungScalarHalvingWall.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