pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.MassTopology

show as:
view Lean formalization →

Physics.MassTopology defines the topological ledger quantities on Q3 required for mass derivations in Recognition Science. It supplies total edges, energy partitions E_total and E_passive, weights W, and ledger fractions that feed electron mass and lepton generation calculations. The module is purely definitional, importing alpha and constant derivations to establish the cubic geometry base for T9 and T10.

claimThe module defines the total edge count of the cubic ledger $Q_3$ together with the partitioned energies $E_ {total}$, $E_{passive}$, weight $W$, ledger fraction, base shift, and radiative corrections up to order 3.

background

This module sits inside the Recognition Science derivation chain after the cubic ledger geometry of AlphaDerivation, which states: 'This module provides a complete, constructive derivation of the fine-structure constant α⁻¹ from the geometry of the cubic ledger' and derives 4π from Gauss-Bonnet via vertex deficits of Q3. It introduces ledger-based energy partitions and correction terms that rest on the RS time quantum τ₀ = 1 tick from Constants and the Recognition Composition Law. The setting prepares the topological inputs for mass formulas on the phi-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions are imported by ElectronMass.Defs and Necessity, which prove the electron mass formula is forced from T8 ledger quantization and cubic geometry, and by LeptonGenerations.Defs for higher generations. The module supplies the missing topological layer between alpha derivation and the T9 mass chain, closing the gap from first-principles constants to lepton sector values.

scope and limits

used by (5)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (9)