LedgerSector
plain-language theorem explainer
LedgerSector is a record type that tags ledger entries with an 8-tick phase index, a photon-coupling flag, and a gravitational flag defaulting to true. Cosmologists working on the ledger-shadow account of dark matter would cite it to separate electromagnetically active and inactive sectors within the same J-cost geometry. The declaration is a plain structure definition with one default field.
Claim. A ledger sector is a triple $(k, c, g)$ where $k$ is an element of the finite set of eight phases, $c$ is a boolean indicating whether the sector couples to photons, and $g$ is a boolean indicating gravitational participation (default true).
background
Recognition Science obtains the eight-tick cycle from the self-similar fixed point phi and the octave period $2^3$ (T7). The upstream phase definition maps each element of Fin 8 to the real angle $k pi/4$, supplying the temporal label for every ledger entry; the companion complex-phase definition supplies the unimodular factor $e^{i w}$ used in wave representations. Both visible and dark sectors therefore share the same J-cost coupling to geometry while differing only in the photon-coupling bit.
proof idea
The declaration is a direct structure definition that introduces the three fields and supplies the default value true for gravitates. No lemmas or tactics are invoked; the constructor is used verbatim by sibling definitions such as visibleSector and darkSector.
why it matters
LedgerSector supplies the minimal classification required to implement the ledger-shadow model of dark matter inside the eight-tick framework (T7). It directly supports the module-level statements that compute omega_dm, the dm_baryon_ratio, and the phase-mismatch suppression mechanism. The structure therefore realizes the claim that dark matter arises as non-luminous ledger configurations without new particles, while leaving open the quantitative match to the observed 5.4 ratio and the 1.79 GeV WIMP projection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.