Encyclopedia Masses Masses Mass Genesis T10 Rung Scalar Halving Wall Odd Yardstick Of Sq Consistent
ARTICLE 4 claims 4 theorems
Masses Mass Genesis T10 Rung Scalar Halving Wall Odd Yardstick Of Sq Consistent
A machine-checked proof shows that if particle masses follow a golden-ratio ladder, the electroweak yardstick must be an odd number, but it cannot say which odd number.
The odd yardstick
The golden ratio φ, about 1.618, is the number whose square is itself plus one. In the Recognition Science framework, particle masses are proposed to sit on a ladder of powers of φ: the mass of a particle is proportional to φ raised to some whole-number exponent. The declaration odd_yardstick_of_sqConsistent_genesis (a theorem in the framework's machine-checked library of formal theorems) establishes a constraint on that exponent for the electroweak sector, the part of physics governing the weak nuclear force and electromagnetism.
The proof works by squaring. The framework models a particle's mass content as the square of a "deposit amplitude," a number that includes a scalar factor q. If q is a rational combination of 1 and φ, and its square equals φ^e divided by 8, then the exponent e must be even. This is because no odd power of φ has a square root in the field Q(φ), the set of numbers of the form a + bφ with a and b rational. The theorem not_sq_phi_pow_odd proves this using Cassini's identity for Fibonacci numbers. Since the electroweak yardstick r0(EW) relates to the mass exponent by r0(EW) = e + 13, an even e forces r0(EW) to be odd. The declaration odd_yardstick_of_sqConsistent_genesis packages this chain: square-consistency implies the yardstick is odd.
This is the first theorem-tier constraint on the yardstick beyond a gauge sum. The framework's frozen value for r0(EW) is 55, which is odd and passes. The nearby even value 56 is excluded by the theorem. But the theorem does not derive 55 itself. The framework's structural apparatus, including modular-flow data and cube-dressing formulas, is provably blind to the specific yardstick value beyond parity. The theorem structural_apparatus_yardstick_blind shows that both e = 42 (yardstick 55) and e = 44 (yardstick 57) pass every structural test. Deriving the exact value 55 requires a principle outside this apparatus, a sector-invariant law of the yardstick itself, which remains open.
The honest verdict is therefore narrow: the declaration proves an oddness constraint, not a specific number. It also proves the reduction is exact and lossless: the amplitude's squared scalar is φ^e with e = r0(EW) - 13, and under square-consistency q = φ^21 if and only if e = 42. The remaining taint, the yardstick value 55, is frozen against the measured Z boson mass from October 2025, not derived. This is a measurement-free theorem: no measured constants appear in its dependency cone.
THEOREM odd_yardstick_of_sqConsistent_genesis · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **Parity constraint on the yardstick (THEOREM).** If the genesis deposit
has a rational-phi scalar at mass exponent `e = r0(EW) - 13`, the
electroweak yardstick is ODD. The frozen 55 passes; an even yardstick such
as 56 is excluded. The first theorem-tier constraint on the yardstick beyond
the gauge sum. -/
theorem odd_yardstick_of_sqConsistent_genesis {q : ℝ} (hq : InQPhi q) {e : ℕ}
(hr : Anchor.r0 Anchor.Sector.Electroweak = (e : ℤ) + 13)
(h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ e / 8) :
Odd (Anchor.r0 Anchor.Sector.Electroweak) := by
have he := even_mass_exponent_of_sqConsistent hq h
rw [hr]
obtain ⟨m, hm⟩ := he
use (m : ℤ) + 6
omega
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 structural_apparatus_yardstick_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **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⟩
THEOREM scalar_eq_phi21_iff_mass_exponent_eq_42 · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **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]
What this page does not claim
The declaration does not derive the specific yardstick value 55; it only proves the yardstick must be odd. The declaration does not prove that masses actually follow the φ ladder; that is a framework model, not a theorem. The declaration does not claim that the framework's structural apparatus can distinguish between different even mass exponents.
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 yardstick value 55 without using a measured mass?
- Does the oddness constraint apply to other sectors, such as the lepton sector, in the same way?
- How does the yardstick value 55 relate to the measured Z boson mass, and what precision does that comparison achieve?
- What would it mean for the framework if a future measurement excluded the yardstick value 55?
- Can the square-consistency condition be derived from the more fundamental cost function J, or is it an independent assumption?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM odd_yardstick_of_sqConsistent_genesis · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **Parity constraint on the yardstick (THEOREM).** If the genesis deposit has a rational-phi scalar at mass exponent `e = r0(EW) - 13`, the electroweak yardstick is ODD. The frozen 55 passes; an even yardstick such as 56 is excluded. The first theorem-tier constraint on the yardstick beyond the gauge sum. -/ theorem odd_yardstick_of_sqConsistent_genesis {q : ℝ} (hq : InQPhi q) {e : ℕ} (hr : Anchor.r0 Anchor.Sector.Electroweak = (e : ℤ) + 13) (h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ e / 8) : Odd (Anchor.r0 Anchor.Sector.Electroweak) := by have he := even_mass_exponent_of_sqConsistent hq h rw [hr] obtain ⟨m, hm⟩ := he use (m : ℤ) + 6 omegaThe declaration odd_yardstick_of_sqConsistent_genesis establishes that if a positive scalar q in Q(φ) squares to φ^e / 8, then the electroweak yardstick r0(EW) must be odd. odd_yardstick_of_sqConsistent_genesis · 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 φ has a square root in Q(φ). not_sq_phi_pow_odd · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.leanTHEOREM structural_apparatus_yardstick_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **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⟩The structural apparatus is yardstick-blind beyond parity: both e = 42 (yardstick 55) and e = 44 (yardstick 57) pass every structural test. structural_apparatus_yardstick_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.leanTHEOREM scalar_eq_phi21_iff_mass_exponent_eq_42 · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
/-- **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]Under square-consistency, q = φ^21 if and only if the mass exponent e = 42. scalar_eq_phi21_iff_mass_exponent_eq_42 · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean