Encyclopedia Masses Masses Mass Genesis T10 Rung Scalar Halving Wall
ARTICLE 5 claims 5 theorems
Masses Mass Genesis T10 Rung Scalar Halving Wall
A theorem about particle masses forces a number to be exactly half of another, and then proves that no known rule can pick which half.
The halving wall
In the Recognition Science framework, particle masses are not free parameters but values that must fit a strict pattern. The pattern is built from powers of the golden ratio, phi, the number roughly equal to 1.618. A central quantity in this pattern is the rung scalar, a positive number that sits on one rung of a ladder of possible mass values. The module called T10 Rung Scalar Halving Wall proves a sharp constraint on this scalar: if its square equals phi raised to an even power, then the scalar itself must equal phi raised to exactly half that power. In symbols, if q squared equals phi to the power 2m, then q equals phi to the power m. This is a proved theorem in the machine-checked library of formal theorems, not a guess.
The theorem has a direct consequence for the electroweak sector. The mass content there is phi to the power 42 divided by 8. Squaring the rung scalar removes a factor and leaves this clean power, and the halving rule then forces the scalar to be phi to the power 21. The number 42 itself is not arbitrary: it decomposes as 55 minus 5 minus 8, where the minus 5 is a documented modeling choice and the minus 8 is a proved structural offset. The remaining number, 55, is the electroweak yardstick, a value frozen against the measured Z boson mass in October 2025. The theorem also shows a parity constraint: no odd power of phi has a square root in the field of rational combinations of phi, so a consistent scalar can only exist at an even mass exponent, which forces the yardstick to be odd. The frozen value 55 passes this test; 56 would fail.
What the module calls the wall is the boundary of what this structural apparatus can prove. Three theorems show that the yardstick value 55 cannot be derived from the existing framework. First, the modular flow data, the full spectrum of eigenvalues, is scale blind: any predicate on that data accepts the intended amplitude if and only if it accepts every rescale, so no such law can distinguish phi to the 21 from phi to the 20. Second, the yardstick has two distinct small-integer decompositions, 3 times W plus 4 and 5 times E_passive, so no simple dressing of derived counts can force it. Third, at every even mass exponent, the complete structural package accepts the candidate, so the apparatus cannot tell the world with yardstick 55 from a world with yardstick 57, which would be observably different. Deriving 55 requires a principle outside the structural apparatus, a sector-invariant law of the yardstick itself. That principle remains open.
The consequence is precise: the framework proves the halving relation and the parity constraint, and it proves exactly which class of rules cannot force the remaining number. The reader can now see that the value 55 is not a loose end but a sharply identified boundary, a target for a future law that the current theorems show is needed.
THEOREM scalar_eq_half_pow_of_sq · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **Halving (THEOREM).** A positive scalar squaring to an even phi power
IS the half power: the square is injective on the nonnegatives, so the rung
scalar's exponent is forced to half the mass exponent with no freedom. -/
theorem scalar_eq_half_pow_of_sq {q : ℝ} {m : ℕ} (hq : 0 ≤ q)
(h : q ^ 2 = Constants.phi ^ (2 * m)) :
q = Constants.phi ^ m := by
have hpow : Constants.phi ^ (2 * m) = (Constants.phi ^ m) ^ 2 := by
rw [← pow_mul, mul_comm 2 m]
rw [hpow] at h
exact (sq_eq_sq₀ hq (pow_pos Constants.phi_pos m).le).mp h
THEOREM scalar_forced_eq_phi21_of_banked_mass · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **DERIVED: the rung scalar is `phi^21` (THEOREM, conditional on the banked
mass content).** Any positive rational-phi scalar whose deposit amplitude
squares to the banked `phi^42/8` is exactly `phi^21`; C9's rung-quantum
membership at `k = 21` is its instance. The exponent 21 is forced as half of
42. -/
theorem scalar_forced_eq_phi21_of_banked_mass {q : ℝ} (hq : InQPhi q) (hq0 : 0 < q)
(h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ 42 / 8) :
q = Constants.phi ^ 21 := by
have h2 := (sqConsistent_scalar_eq_half_pow hq hq0 h).2
rwa [show (42 : ℕ) / 2 = 21 from by norm_num] at h2
THEOREM not_sq_phi_pow_odd · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **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 modularFlow_predicate_scale_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **No modular-flow predicate can fix the absolute scale (THEOREM).** Any
predicate of the modular eigenvalue function accepts an amplitude iff it
accepts every nonzero rescale, so the class of modular-flow scalar laws
cannot distinguish `phi^21` from `phi^20` (or any other rescaling) in the
deposit prefactor. This closes the C10 lead (ii) route through the tower's
modular spectrum. -/
theorem modularFlow_predicate_scale_blind {N : ℕ} (k : Fin N)
(P : (SectorN N → SectorN N → ℝ) → Prop) {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) :
P (modularEigenvalueN a k) ↔ P (modularEigenvalueN b k) := by
have hfun : modularEigenvalueN a k = modularEigenvalueN b k := by
funext i j
exact modularEigenvalueN_amplitude_blind ha hb k i j
rw [hfun]
THEOREM structural_package_at_even_exponent · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **The structural package holds at every even mass exponent (THEOREM).**
For every even `e`, the candidate `a_e = phi^(e/2) * cN` (i) squares to the
mass content `phi^e / 8` (square-consistency), (ii) passes the rung-quantum
deposit law at `k = e/2`, and (iii) rejects the doubled decoy `2 a_e` (the
diagonal ratio 2 is no integer power of `phi`, banked `two_not_zpow_phi`,
independent of `e`). The complete structural test the deposit apparatus runs
is satisfied at every even exponent. -/
theorem structural_package_at_even_exponent {e : ℕ} (he : Even e) :
((Constants.phi ^ (e / 2) * creationDepositNorm) ^ 2 =
Constants.phi ^ e / 8) ∧
(∃ k : ℕ, Constants.phi ^ (e / 2) * creationDepositNorm =
Constants.phi ^ k * creationDepositNorm) ∧
(¬ ∃ k : ℕ, 2 * (Constants.phi ^ (e / 2) * creationDepositNorm) =
Constants.phi ^ k * creationDepositNorm) := by
obtain ⟨m, hm⟩ := he
have hm2 : e / 2 = m := by omega
have hm' : e = 2 * m := by omega
refine ⟨?_, ⟨m, by rw [hm2]⟩, ?_⟩
· rw [hm2, depositAmplitude_sq_eq_iff, hm', ← pow_mul, mul_comm 2 m]
· rintro ⟨k, hk⟩
rw [hm2, creationDepositNorm_eq_pow] at hk
have hpn : postingNorm ≠ 0 := ne_of_gt postingNorm_pos
have hk2 : (2 * Constants.phi ^ m) * postingNorm ^ 3 =
Constants.phi ^ k * postingNorm ^ 3 := by
linear_combination hk
have h1 : 2 * Constants.phi ^ m = Constants.phi ^ k :=
mul_right_cancel₀ (pow_ne_zero 3 hpn) hk2
have hφ : Constants.phi ≠ 0 := Constants.phi_ne_zero
have hz : Constants.phi ^ ((k : ℤ) - (m : ℕ)) = 2 := by
rw [zpow_sub₀ hφ, zpow_natCast, zpow_natCast, ← h1]
rw [div_eq_iff (pow_ne_zero m hφ)]
exact two_not_zpow_phi ⟨(k : ℤ) - (m : ℕ), hz⟩
What this page does not claim
The module does not derive the value 55 from the structural apparatus. The halving rule does not apply to odd powers of phi. The framework does not claim the yardstick value is the only possible one.
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:
- What sector-invariant principle could force the electroweak yardstick to be 55?
- How does the halving rule generalize to other sectors beyond electroweak?
- What observable distinguishes a world with yardstick 55 from one with yardstick 57?
- Does the minus 5 modeling choice have a derivation within the framework?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM scalar_eq_half_pow_of_sq · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **Halving (THEOREM).** A positive scalar squaring to an even phi power IS the half power: the square is injective on the nonnegatives, so the rung scalar's exponent is forced to half the mass exponent with no freedom. -/ theorem scalar_eq_half_pow_of_sq {q : ℝ} {m : ℕ} (hq : 0 ≤ q) (h : q ^ 2 = Constants.phi ^ (2 * m)) : q = Constants.phi ^ m := by have hpow : Constants.phi ^ (2 * m) = (Constants.phi ^ m) ^ 2 := by rw [← pow_mul, mul_comm 2 m] rw [hpow] at h exact (sq_eq_sq₀ hq (pow_pos Constants.phi_pos m).le).mp hif q squared equals phi to the power 2m, then q equals phi to the power m. scalar_eq_half_pow_of_sq · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.leanTHEOREM scalar_forced_eq_phi21_of_banked_mass · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **DERIVED: the rung scalar is `phi^21` (THEOREM, conditional on the banked mass content).** Any positive rational-phi scalar whose deposit amplitude squares to the banked `phi^42/8` is exactly `phi^21`; C9's rung-quantum membership at `k = 21` is its instance. The exponent 21 is forced as half of 42. -/ theorem scalar_forced_eq_phi21_of_banked_mass {q : ℝ} (hq : InQPhi q) (hq0 : 0 < q) (h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ 42 / 8) : q = Constants.phi ^ 21 := by have h2 := (sqConsistent_scalar_eq_half_pow hq hq0 h).2 rwa [show (42 : ℕ) / 2 = 21 from by norm_num] at h2the scalar is forced to be phi to the power 21. scalar_forced_eq_phi21_of_banked_mass · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.leanTHEOREM not_sq_phi_pow_odd · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **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 hnonnegno odd power of phi has a square root in the field of rational combinations of phi not_sq_phi_pow_odd · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.leanTHEOREM modularFlow_predicate_scale_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **No modular-flow predicate can fix the absolute scale (THEOREM).** Any predicate of the modular eigenvalue function accepts an amplitude iff it accepts every nonzero rescale, so the class of modular-flow scalar laws cannot distinguish `phi^21` from `phi^20` (or any other rescaling) in the deposit prefactor. This closes the C10 lead (ii) route through the tower's modular spectrum. -/ theorem modularFlow_predicate_scale_blind {N : ℕ} (k : Fin N) (P : (SectorN N → SectorN N → ℝ) → Prop) {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) : P (modularEigenvalueN a k) ↔ P (modularEigenvalueN b k) := by have hfun : modularEigenvalueN a k = modularEigenvalueN b k := by funext i j exact modularEigenvalueN_amplitude_blind ha hb k i j rw [hfun]any predicate on that data accepts the intended amplitude if and only if it accepts every rescale modularFlow_predicate_scale_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.leanTHEOREM structural_package_at_even_exponent · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **The structural package holds at every even mass exponent (THEOREM).** For every even `e`, the candidate `a_e = phi^(e/2) * cN` (i) squares to the mass content `phi^e / 8` (square-consistency), (ii) passes the rung-quantum deposit law at `k = e/2`, and (iii) rejects the doubled decoy `2 a_e` (the diagonal ratio 2 is no integer power of `phi`, banked `two_not_zpow_phi`, independent of `e`). The complete structural test the deposit apparatus runs is satisfied at every even exponent. -/ theorem structural_package_at_even_exponent {e : ℕ} (he : Even e) : ((Constants.phi ^ (e / 2) * creationDepositNorm) ^ 2 = Constants.phi ^ e / 8) ∧ (∃ k : ℕ, Constants.phi ^ (e / 2) * creationDepositNorm = Constants.phi ^ k * creationDepositNorm) ∧ (¬ ∃ k : ℕ, 2 * (Constants.phi ^ (e / 2) * creationDepositNorm) = Constants.phi ^ k * creationDepositNorm) := by obtain ⟨m, hm⟩ := he have hm2 : e / 2 = m := by omega have hm' : e = 2 * m := by omega refine ⟨?_, ⟨m, by rw [hm2]⟩, ?_⟩ · rw [hm2, depositAmplitude_sq_eq_iff, hm', ← pow_mul, mul_comm 2 m] · rintro ⟨k, hk⟩ rw [hm2, creationDepositNorm_eq_pow] at hk have hpn : postingNorm ≠ 0 := ne_of_gt postingNorm_pos have hk2 : (2 * Constants.phi ^ m) * postingNorm ^ 3 = Constants.phi ^ k * postingNorm ^ 3 := by linear_combination hk have h1 : 2 * Constants.phi ^ m = Constants.phi ^ k := mul_right_cancel₀ (pow_ne_zero 3 hpn) hk2 have hφ : Constants.phi ≠ 0 := Constants.phi_ne_zero have hz : Constants.phi ^ ((k : ℤ) - (m : ℕ)) = 2 := by rw [zpow_sub₀ hφ, zpow_natCast, zpow_natCast, ← h1] rw [div_eq_iff (pow_ne_zero m hφ)] exact two_not_zpow_phi ⟨(k : ℤ) - (m : ℕ), hz⟩at every even mass exponent, the complete structural package accepts the candidate structural_package_at_even_exponent · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean