pith. sign in
module module high

IndisputableMonolith.Masses.StepValueEnumeration

show as:
view Lean formalization →

The module enumerates the natural invariants consisting of Q₃ cell counts and their linear combinations at D=3. These integers receive direct combinatorial meaning and supply the concrete values required by the alpha derivation and sector-dependent torsion constraints. The module consists of definitions together with short lemmas that verify summation, uniqueness, and partitioning properties of the listed pairs.

claimAt dimension 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$, $F+C=7$, $E+C=13$, $E-C=11$ and the relation $E-A=11$.

background

Recognition Science works at D=3 with the cubic ledger Q₃ whose cell counts are fixed by the geometry. The module records these counts and the integer combinations that arise as wallpaper-group orders or Euler characteristics. Upstream AlphaDerivation derives 4π from vertex deficits of Q₃. SectorDependentTorsion proves that the set {13,11,6,8} satisfies the cyclic-chain and 2D^D+1=55 partition constraints.

proof idea

The module proceeds by direct enumeration of the cell counts followed by algebraic verification of each listed summation and uniqueness property. Sibling lemmas check middle-pair and endpoint-pair relations that partition the relevant totals and confirm distinctness modulo the edge-pair filter.

why it matters in Recognition Science

The enumerated invariants close the combinatorial side of the D=3 forcing chain and supply the integer inputs required by the alpha derivation from the cubic ledger and by the sector-dependent torsion constraints. They therefore stand immediately before any mass-formula application that uses the phi-ladder.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)