pith. sign in
module module high

IndisputableMonolith.Masses.Anchor

show as:
view Lean formalization →

Masses.Anchor supplies the foundational definitions for sector yardsticks B_pow and r0, plus passive edge counts, that anchor all subsequent mass derivations on the phi-ladder. RS mass-spectrum workers cite it to trace electron and proton ratios back to Q3 combinatorics rather than literals. The module is built as a collection of abbrevs and eq lemmas that expose the cube-derived structure without new theorems.

claimThe module defines sector anchors including the passive edge count $E_0=11$, coherence energy $E_0$, total energy $E$, and yardsticks $B_0$, $r_0$ together with the sector decomposition and the equalities $B_0$ (lepton) = $B_0$ (up) = $B_0$ (down) = $B_0$ (electroweak).

background

Recognition Science constructs particle masses via the phi-ladder formula yardstick times phi to the power (rung minus 8 plus gap(Z)). The yardsticks themselves must be derived from the geometry of the 3-cube Q3 rather than postulated. This module imports the RS time quantum tau_0 = 1 tick from Constants and the Gauss-Bonnet derivation of 4 pi from AlphaDerivation to ground those yardsticks. It introduces the auxiliary notions of passive edges, coherence sectors, and B_pow as the combinatorial scale factor for each sector.

proof idea

This is a definition module, no proofs. It consists of a sequence of abbrevs and eq lemmas that compute E_passive as 12 minus 1, introduce the four sector cases, and state the four B_pow equalities that follow directly from the shared cube combinatorics.

why it matters in Recognition Science

The module is the common source for the mass derivations in ElectronMass (C-007) and ProtonElectronMassRatio (C-009). AnchorDerivation explicitly credits it with upgrading sector yardsticks from boundary assumptions to derived objects. It thereby supplies the concrete link between the T5-T8 forcing chain and the numerical mass ladder.

scope and limits

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (25)