RSLedger
plain-language theorem explainer
The RS Ledger packages the three forced parameters of any discrete conservative system into one record: three spatial dimensions, golden-ratio scaling, and an eight-tick cycle. A researcher closing the uniqueness argument in Recognition Science would cite this structure when stating that every such system must be isomorphic to it. The declaration is a plain structure definition that supplies the default values for its three fields.
Claim. The RS Ledger is the structure whose fields are fixed at dimension $=3$, ratio $=φ$, and cycleLength $=8$, where $φ$ is the golden ratio.
background
Module Gap 9 addresses the objection that discreteness permits many conservative systems and asks why the ledger must adopt specifically $φ$, the three-dimensional cube, and the eight-tick cycle. The RS Ledger collects these three forced values into a single abstract record. Upstream results supply the cycle length of eight from mass-to-light derivations and the active-edge count $A=1$ from integration-gap and actualization contexts.
proof idea
The declaration is a structure definition that directly assigns the three fields with their forced defaults. No lemmas or tactics are invoked.
why it matters
This structure supplies the canonical target referenced by the module's main theorem asserting that any discrete conservative system is isomorphic to the RS Ledger. It assembles the unique solutions to the constraints listed in the module doc: cost-function fixed point for $φ$, irreducible linking for $D=3$, and Gray-code compatibility for the eight-tick cycle. The declaration therefore closes the uniqueness step for the parameters arising from T5–T8 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.