DiscreteConservativeSystem
plain-language theorem explainer
DiscreteConservativeSystem defines a countable state space equipped with a conservation placeholder. It supplies the hypothesis type for the uniqueness theorem showing any such system matches the RS ledger with golden ratio, three dimensions, and eight-tick cycle. The structure is a direct declaration with no internal proof steps.
Claim. A discrete conservative system consists of a countable type $S$ (state space) together with a conservation property instantiated as the trivial proposition True.
background
The module Gap 9: Ledger Uniqueness formalizes the objection that discreteness and conservation alone do not force the specific RS ledger parameters. It resolves the objection by showing each component (phi, Q3, eight-tick) is the unique solution to its constraint: phi from the J-cost fixed point, Q3 from irreducible linking in three dimensions, and eight-tick from Gray-code cycle minimality. Upstream results include phi_unique_fixed_point for the fixed-point constraint and eight_tick_minimal for cycle length.
proof idea
This is a structure definition with zero proof lines. It directly encodes the state space and conservation fields as the input type for the downstream uniqueness theorem.
why it matters
The definition supplies the hypothesis for ledger_structure_unique, which concludes existence of an RS Ledger with dimension 3, ratio phi, and cycle length 8. It closes the meta gap on why the ledger must take this specific form rather than another discrete conservative structure. The result sits inside the forcing chain that derives T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, and T8 D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.