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

IndisputableMonolith.Masses.StepValueEnumeration

show as:
view Lean formalization →

The StepValueEnumeration module enumerates the natural invariants from D=3 cubic lattice geometry for use in mass step calculations. These include cell counts V=8, E=12, F=6, C=1 and combinations such as 17 and 13 that carry direct Q3 combinatorial meaning. Researchers deriving mass spectra on the phi-ladder cite it to fix allowed rung increments. The module consists of definitions for the invariant collection followed by lemmas that verify summation relations and chain uniqueness via direct case analysis.

claimAt $D=3$ the natural invariants are the cell counts $V=8$, $E=12$, $F=6$, $C=1$ together with the combinations $V+F=14$, $2V+1=17$, $V+F-C=13$, $V+E=20$, $E+F=18$, $V+E+F=26$, and $E-C=11$.

background

Recognition Science obtains all physics from the geometry of the cubic ledger Q3. At spatial dimension D=3 the ledger possesses eight vertices, twelve edges, six faces and one cell. The module enumerates the natural invariants: the integers possessing direct Q3-combinatorial interpretation, namely the cell counts and their simple linear combinations. The supplied documentation states that these are precisely the integers with a direct Q3-combinatorial interpretation at D=3.

proof idea

The module is enumerative and definitional. It first introduces natural_invariants_D3 as the explicit list of the D=3 cell counts and combinations. Subsequent declarations prove concrete relations: middle pairs sum to 17, endpoint pairs sum to 21, the current chain partitions 55, and the chain is unique modulo edge-pair filters. All proofs proceed by exhaustive verification on the small finite sets of integers.

why it matters in Recognition Science

This module supplies the combinatorial foundation for step values on the phi-ladder that enter the mass formula. It feeds downstream mass enumeration by identifying the allowed rung increments fixed by the D=3 invariants. The work connects directly to the T8 forcing of D=3 and to the sector-dependent torsion results that establish the core counts {13,11,6,8} and their cyclic-chain partition of 55.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)