pith. sign in
module module moderate

IndisputableMonolith.Masses.AnchorDerivation

show as:
view Lean formalization →

AnchorDerivation supplies alternative expressions for B_pow and related mass constants such as r0. Researchers deriving masses from the phi-ladder and cubic ledger geometry would cite it to cross-check canonical anchors. The module consists of definitions for Wz, Etz, Epz, Az together with equality statements that link directly to the imported Anchor and AlphaDerivation modules.

claimAlternative expression for $B_{pow}$ (denoted $B_{pow}^{alt}$) together with $r_0^{alt}$, $W_z$, $E_{tz}$, $E_{pz}$, $A_z$ and their canonical equalities.

background

This module sits in the Masses domain and imports the canonical anchors from IndisputableMonolith.Masses.Anchor together with the alpha derivation from IndisputableMonolith.Constants.AlphaDerivation. The Anchor module centralises parameter-free constants described in the mass manuscripts; everything lives in the Model layer with no proofs claiming experimental agreement. AlphaDerivation supplies a complete constructive derivation of the fine-structure constant alpha^{-1} from the geometry of the cubic ledger, including 4 pi from Gauss-Bonnet via vertex deficits of Q_3.

proof idea

This is a definition module, no proofs. It introduces the alternative forms B_pow_alt and r0_alt plus the auxiliary quantities Wz, Etz, Epz, Az and records their equalities to the canonical versions by direct definition.

why it matters in Recognition Science

The module supports the mass derivation chain by furnishing alternative formulations that can be used to verify the canonical constants. It feeds the broader Recognition Science results on mass spectra that rely on the phi-ladder and the eight-tick octave. It touches the derivation of alpha^{-1} inside the interval (137.030, 137.039) supplied by the upstream AlphaDerivation module.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)