Encyclopedia Masses Masses Mass Genesis T10 Rung Scalar Halving Wall Structural Apparatus Yardstick

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Rung Scalar Halving Wall Structural Apparatus Yardstick

A machine-checked proof shows that the framework's own structural tests cannot tell the difference between the observed mass scale and a neighboring one, so the final number must come from a principle outside the current apparatus.

Verify this page

The limits of the structural apparatus

The golden ratio φ, about 1.618, appears throughout the framework's account of particle masses. The declaration structural_apparatus_yardstick_blind is a theorem in the framework's machine-checked library of formal theorems. It establishes a precise limit: the framework's structural tests, the ones that check consistency and reject decoys, accept two different mass scales equally well. One scale corresponds to the observed world; the other, with a different yardstick value, would be observably different. The theorem proves the apparatus cannot select between them.

In the framework, a ledger, a discrete record of events, tracks a scalar quantity that squares to a mass content. The structural tests include square-consistency, which forces a scalar's exponent to be half the mass exponent, and rejection of doubled decoys. The theorem shows that at every even mass exponent, these tests pass. It instantiates this at exponent 42, which corresponds to the electroweak yardstick value 55, and at exponent 44, which would correspond to a yardstick of 57. Both pass. The two worlds are genuinely different, as the theorem also proves that φ^57 ≠ φ^55.

This result is a consequence of two other theorems in the same module. One, modularFlow_predicate_scale_blind, proves that the tower's modular data, its eigenvalues and predicates, are identical at any two nonzero amplitudes. No modular-flow law can distinguish φ^21 from φ^20 in the deposit prefactor. The other, r0_electroweak_formula_nonunique, shows that two distinct combinations of derived counts both reach the yardstick value 55, so no small-integer dressing of banked counts can force it. The structural apparatus is therefore blind to the yardstick beyond a parity condition: it can prove the yardstick is odd, but not that it is 55.

What the declaration does not claim is important. It does not prove that the yardstick value 55 is wrong or unobservable; it proves the opposite, that the two worlds are observably different. It does not claim that no principle can force the yardstick; it names the class that cannot: modular-flow predicates and the structural tests. The framework's own account states that deriving 55 requires a sector-invariant law of the yardstick itself, a principle outside the structural apparatus. That principle remains open.

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⟩
THEOREM witness_exponent_distinct · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
witness_exponent_distinct · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean:508 
/-- The witness yardstick is an observably different world: `phi^57 ≠ phi^55`
since `phi > 1`. -/
theorem witness_exponent_distinct :
    Constants.phi ^ (57 : ℤ) ≠ Constants.phi ^ (55 : ℤ) := by
  intro h
  have hlt : Constants.phi ^ (55 : ℤ) < Constants.phi ^ (57 : ℤ) :=
    zpow_lt_zpow_right₀ one_lt_phi (by norm_num)
  rw [h] at hlt
  exact lt_irrefl _ hlt
THEOREM modularFlow_predicate_scale_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
modularFlow_predicate_scale_blind · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean:439 
/-- **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 r0_electroweak_formula_nonunique · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean
r0_electroweak_formula_nonunique · IndisputableMonolith/Masses/MassGenesis/T10RungScalarHalvingWall.lean:455 
/-- **WALL 2 (THEOREM).** The electroweak rung offset is `3W + 4` by
definition, and the same value is `5 * E_passive` (the passive-field edge
count): two distinct small-integer combinations of derived counts reach 55,
so no cube-dressing formula of this family can force the value. A formula
family that reaches a value twice conveys nothing by reaching it (the banked
selective-content measurement; same shape as
`b_pow_lepton_formula_nonunique` for the powers of two). -/
theorem r0_electroweak_formula_nonunique :
    Anchor.r0 Anchor.Sector.Electroweak = 3 * (Anchor.W : ℤ) + 4 ∧
      Anchor.r0 Anchor.Sector.Electroweak = 5 * (Anchor.E_passive : ℤ) := by
  refine ⟨?_, ?_⟩
  · simp only [Anchor.r0, Anchor.W, AlphaDerivation.wallpaper_groups]
  · simp only [Anchor.r0, Anchor.W, Anchor.E_passive,
      AlphaDerivation.wallpaper_groups, AlphaDerivation.passive_field_edges,
      AlphaDerivation.cube_edges, AlphaDerivation.active_edges_per_tick,
      AlphaDerivation.D]
    norm_num

What this page does not claim

The declaration does not claim that the yardstick value 55 is wrong or unobservable. It does not claim that no principle can force the yardstick value. It does not claim that the framework's structural tests are the only possible tests.

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