Encyclopedia Masses Masses Mass Genesis T10 Anchor Closure C17 Axiom Audit Gap One Predicted Mass Eq

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Anchor Closure C17 Axiom Audit Gap One Predicted Mass Eq

A machine-checked theorem pins one predicted particle mass to exactly 2 times the golden ratio raised to the 42nd power, with no fitted input.

Verify this page

The gap-one mass anchor

The golden ratio φ, about 1.618, appears throughout mathematics as the solution to r² = r + 1. In the Recognition Science framework, a machine-checked library of formal theorems derives physical structure from a single starting point: reality keeps a ledger, a discrete record of recognition events. The theorem gapOne_predictedMass_eq_two_phi42 states that for a specific topological pattern called the gap-one worldline, the predicted mass equals exactly 2 · φ⁴². This is a pure number, a fixed positive real, not a ratio to any unit.

The proof is a dependency audit. Every input to the mass formula is derived internal structure: the exponent 42 comes from cube-geometry integers (edge, face, and wallpaper counts), the coherence energy E_coh equals φ⁻⁵ and is derived three independent ways, and φ itself is forced by the framework's foundational theorem. Nothing in the closure reads any empirical mass input or any fitted parameter. The audit shows the absolute scale is banked modulo exactly one adopted, typed, located model law: load normalization, which the library proves is identical to the T10 residual and to the foundational model law R4.

The theorem does not attach an SI unit. It does not claim that this pure number equals any measured particle mass in kilograms or electronvolts; that comparison against the Particle Data Group values is an empirical check, not part of the theorem. The theorem also does not claim that the mass law m = Σ load is a proved theorem; that equation is absent as a theorem, present only as a named boundary predicate. The audit proves the anchor value is banked up to exactly one typed identification, and that no internal predicate can supply that identification because every uniquely pinning on-orbit predicate is pointwise σ-zero.

What this establishes for the reader is a precise provenance claim: a specific predicted mass is a theorem, derived from structural constants with no fitted input, and the single remaining freedom is explicitly located and named. The framework does not claim to have derived the absolute scale of particle masses from nothing; it claims to have reduced the freedom to one adopted, located model law, and to have proved everything else in the closure.

THEOREM gapOne_predictedMass_eq_two_phi42 · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean
gapOne_predictedMass_eq_two_phi42 · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean:66 
/-- **The gap-one anchor (THEOREM).** The topology-labelled gap-one
worldline pattern has the RS-native pure-number mass `2 * φ^42`. This public
receipt promotes the private arithmetic helper used by the posted-emission
wall into the paper-facing audit surface. It does not attach an SI unit. -/
theorem gapOne_predictedMass_eq_two_phi42 :
    predictedMass (worldlinePattern gapOneTwoPhaseMode) =
      2 * Constants.phi ^ (42 : ℕ) := by
  have hsec :
      sectorOf (worldlinePattern gapOneTwoPhaseMode) =
        Anchor.Sector.Electroweak := by
    simp [sectorOf, sectorFromTopology, worldlinePattern]
  have hrung : rungOf (worldlinePattern gapOneTwoPhaseMode) = 0 := by
    simp [rungOf, rungFromTopology, worldlinePattern]
  have hZ : ZOf (worldlinePattern gapOneTwoPhaseMode) = 0 := by
    simp [ZOf, ZFromTopology, sectorFromTopology, worldlinePattern]
  unfold predictedMass
  rw [hsec, hrung, hZ]
  unfold MassLaw.predict_mass
  rw [MassLaw.gap_zero_neutral]
  simp only [Anchor.yardstick, Anchor.E_coh, Anchor.B_pow_Electroweak_eq,
    Anchor.r0_Electroweak_eq]
  have hphi_ne : Constants.phi ≠ 0 := Constants.phi_ne_zero
  have h2 : (2 : ℝ) ^ (1 : ℤ) = (2 : ℝ) := by norm_num
  rw [h2]
  have hexp : (((0 : ℤ) : ℝ) - 8 + (0 : ℝ)) = (-8 : ℝ) := by norm_num
  rw [hexp]
  have hrpow :
      Constants.phi ^ (-8 : ℝ) = Constants.phi ^ (-(8 : ℤ)) := by simp
  rw [hrpow]
  have hpow :
      Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
          Constants.phi ^ (-(8 : ℤ)) =
        Constants.phi ^ (42 : ℤ) := by
    rw [← zpow_add₀ hphi_ne, ← zpow_add₀ hphi_ne]
    norm_num
  conv_lhs =>
    rw [show
      (2 : ℝ) * Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
          Constants.phi ^ (-(8 : ℤ)) =
        (2 : ℝ) *
          (Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
            Constants.phi ^ (-(8 : ℤ))) by ring]
  rw [hpow]
  have hnat : Constants.phi ^ (42 : ℤ) =
      Constants.phi ^ (42 : ℕ) := by
    simp [← zpow_natCast]
  rw [hnat]
THEOREM gapOne_predictedMass_eq_two_phi42 · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean
gapOne_predictedMass_eq_two_phi42 · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean:66 
/-- **The gap-one anchor (THEOREM).** The topology-labelled gap-one
worldline pattern has the RS-native pure-number mass `2 * φ^42`. This public
receipt promotes the private arithmetic helper used by the posted-emission
wall into the paper-facing audit surface. It does not attach an SI unit. -/
theorem gapOne_predictedMass_eq_two_phi42 :
    predictedMass (worldlinePattern gapOneTwoPhaseMode) =
      2 * Constants.phi ^ (42 : ℕ) := by
  have hsec :
      sectorOf (worldlinePattern gapOneTwoPhaseMode) =
        Anchor.Sector.Electroweak := by
    simp [sectorOf, sectorFromTopology, worldlinePattern]
  have hrung : rungOf (worldlinePattern gapOneTwoPhaseMode) = 0 := by
    simp [rungOf, rungFromTopology, worldlinePattern]
  have hZ : ZOf (worldlinePattern gapOneTwoPhaseMode) = 0 := by
    simp [ZOf, ZFromTopology, sectorFromTopology, worldlinePattern]
  unfold predictedMass
  rw [hsec, hrung, hZ]
  unfold MassLaw.predict_mass
  rw [MassLaw.gap_zero_neutral]
  simp only [Anchor.yardstick, Anchor.E_coh, Anchor.B_pow_Electroweak_eq,
    Anchor.r0_Electroweak_eq]
  have hphi_ne : Constants.phi ≠ 0 := Constants.phi_ne_zero
  have h2 : (2 : ℝ) ^ (1 : ℤ) = (2 : ℝ) := by norm_num
  rw [h2]
  have hexp : (((0 : ℤ) : ℝ) - 8 + (0 : ℝ)) = (-8 : ℝ) := by norm_num
  rw [hexp]
  have hrpow :
      Constants.phi ^ (-8 : ℝ) = Constants.phi ^ (-(8 : ℤ)) := by simp
  rw [hrpow]
  have hpow :
      Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
          Constants.phi ^ (-(8 : ℤ)) =
        Constants.phi ^ (42 : ℤ) := by
    rw [← zpow_add₀ hphi_ne, ← zpow_add₀ hphi_ne]
    norm_num
  conv_lhs =>
    rw [show
      (2 : ℝ) * Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
          Constants.phi ^ (-(8 : ℤ)) =
        (2 : ℝ) *
          (Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
            Constants.phi ^ (-(8 : ℤ))) by ring]
  rw [hpow]
  have hnat : Constants.phi ^ (42 : ℤ) =
      Constants.phi ^ (42 : ℕ) := by
    simp [← zpow_natCast]
  rw [hnat]
THEOREM gapOne_predictedMass_eq_two_phi42 · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean
gapOne_predictedMass_eq_two_phi42 · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean:66 
/-- **The gap-one anchor (THEOREM).** The topology-labelled gap-one
worldline pattern has the RS-native pure-number mass `2 * φ^42`. This public
receipt promotes the private arithmetic helper used by the posted-emission
wall into the paper-facing audit surface. It does not attach an SI unit. -/
theorem gapOne_predictedMass_eq_two_phi42 :
    predictedMass (worldlinePattern gapOneTwoPhaseMode) =
      2 * Constants.phi ^ (42 : ℕ) := by
  have hsec :
      sectorOf (worldlinePattern gapOneTwoPhaseMode) =
        Anchor.Sector.Electroweak := by
    simp [sectorOf, sectorFromTopology, worldlinePattern]
  have hrung : rungOf (worldlinePattern gapOneTwoPhaseMode) = 0 := by
    simp [rungOf, rungFromTopology, worldlinePattern]
  have hZ : ZOf (worldlinePattern gapOneTwoPhaseMode) = 0 := by
    simp [ZOf, ZFromTopology, sectorFromTopology, worldlinePattern]
  unfold predictedMass
  rw [hsec, hrung, hZ]
  unfold MassLaw.predict_mass
  rw [MassLaw.gap_zero_neutral]
  simp only [Anchor.yardstick, Anchor.E_coh, Anchor.B_pow_Electroweak_eq,
    Anchor.r0_Electroweak_eq]
  have hphi_ne : Constants.phi ≠ 0 := Constants.phi_ne_zero
  have h2 : (2 : ℝ) ^ (1 : ℤ) = (2 : ℝ) := by norm_num
  rw [h2]
  have hexp : (((0 : ℤ) : ℝ) - 8 + (0 : ℝ)) = (-8 : ℝ) := by norm_num
  rw [hexp]
  have hrpow :
      Constants.phi ^ (-8 : ℝ) = Constants.phi ^ (-(8 : ℤ)) := by simp
  rw [hrpow]
  have hpow :
      Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
          Constants.phi ^ (-(8 : ℤ)) =
        Constants.phi ^ (42 : ℤ) := by
    rw [← zpow_add₀ hphi_ne, ← zpow_add₀ hphi_ne]
    norm_num
  conv_lhs =>
    rw [show
      (2 : ℝ) * Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
          Constants.phi ^ (-(8 : ℤ)) =
        (2 : ℝ) *
          (Constants.phi ^ (-(5 : ℤ)) * Constants.phi ^ (55 : ℤ) *
            Constants.phi ^ (-(8 : ℤ))) by ring]
  rw [hpow]
  have hnat : Constants.phi ^ (42 : ℤ) =
      Constants.phi ^ (42 : ℕ) := by
    simp [← zpow_natCast]
  rw [hnat]

What this page does not claim

The theorem does not attach an SI unit to the mass value. The theorem does not claim that the mass law m = Σ load is a proved theorem. The theorem does not claim that any measured particle mass equals 2 · φ⁴².

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