Encyclopedia Masses Masses Mass Genesis T10 Anchor Closure C17 Axiom Audit

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Anchor Closure C17 Axiom Audit

A machine-checked audit shows that the predicted mass of one particle is a fixed number, not a ratio, and that only one adopted law stands between it and the framework's axioms.

Verify this page

What the audit closes

In Recognition Science, a framework that derives physical structure from a forced cost of recognition, the mass of a particle is not measured or fitted. It is computed from a formula. The formula for the gap-one worldline anchor, a specific topology-labelled pattern, is predictedMass = 2 * φ^42, where φ is the golden ratio. The audit module reports three things: that every input to this formula is derived from internal structure, that the result is an absolute number rather than a ratio, and that the equation m = Σ load is not a theorem but a named boundary predicate.

The dependency closure is the first result. The formula reads predict_mass s r Z = Anchor.yardstick s * φ^((r:ℝ) − 8 + gap_correction Z), with yardstick s = 2^(B_pow s) · E_coh · φ^(r0 s). Every symbol is derived: B_pow and r0 are cube-geometry integers, E_coh = φ^(−5) is derived three independent ways, and φ is forced by the framework's own theorems. Nothing in the closure reads an empirical mass input or the anchor amplitude. The scale weight is the second result: predict_mass is a fixed positive real number once sector, rung, and charge are fixed, not a ratio to an internal unit. This refutes the priced risk that ratios alone cannot produce an absolute.

The third result concerns the equation m = Σ load. It is absent as a theorem. It exists as the named boundary predicate MassLawLoadRealized, and a theorem proves it is the same equation as the T10 residual: on a settled anchor, posting amplitude matches the topology factor amplitude iff the predicate holds. The factor amplitude squared is predictedMass / 16, and the positive root form is proved as gapOne_factorAmplitude_eq_sqrt_predictedMass_div_sixteen.

In Recognition Science, the audit's verdict is that the freedom was never at the amplitude. The anchor value is banked up to exactly one typed identification: load normalization, proved identical to the T10 residual and to R4, the foundational model law adopted 2026-07-24. The genesis-orbit wall proves no internal predicate can supply that identification, because every uniquely pinning on-orbit predicate is pointwise σ-zero. The absolute scale is therefore banked modulo exactly one adopted, typed, located model law. The machine-checked library of formal theorems, where these proofs live, confirms the audit with no RS-specific axioms.

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_factorAmplitude_eq_sqrt_predictedMass_div_sixteen · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean
gapOne_factorAmplitude_eq_sqrt_predictedMass_div_sixteen · IndisputableMonolith/Masses/MassGenesis/T10AnchorClosureC17AxiomAudit.lean:114 
/-- **Positive-root form (THEOREM).** The intended gap-one factor amplitude
is the positive square root of one sixteenth of the predicted mass. -/
theorem gapOne_factorAmplitude_eq_sqrt_predictedMass_div_sixteen :
    primitivePositiveStationaryFactorAmplitude
        (worldlinePattern gapOneTwoPhaseMode) =
      Real.sqrt
        (predictedMass (worldlinePattern gapOneTwoPhaseMode) / 16) := by
  rw [← factorAmplitude_sq_eq_predictedMass_div_sixteen,
    Real.sqrt_sq
      (primitivePositiveStationaryFactorAmplitude_nonneg
        (worldlinePattern gapOneTwoPhaseMode))]
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 audit does not attach an SI unit to the mass value. The audit does not prove that the boundary predicate MassLawLoadRealized is a theorem; it proves it is identical to the T10 residual and to R4. The audit does not claim that the mass formula is derived from empirical inputs; it explicitly shows the closure reads none.

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