DiscreteConservativeSystem
plain-language theorem explainer
A discrete conservative system consists of a countable state space together with a placeholder conservation law. Recognition Science researchers addressing ledger uniqueness cite this structure as the input class for proving that any such system must match the RS ledger. The definition is introduced as a direct structure with three fields and no further axioms.
Claim. A discrete conservative system consists of a countable type $S$ together with a proposition asserting the existence of a conservation law (currently instantiated as the trivial proposition).
background
The module Meta.LedgerUniqueness addresses the objection that discreteness alone permits many possible ledgers. It shows that the specific choices of golden ratio, three dimensions, and eight-tick cycle are forced once a discrete conservative system is assumed. The local setting is Gap 9 of the Recognition Science program, which closes the uniqueness argument after the forcing chain (T5–T8) has already fixed J-uniqueness, the phi fixed point, the eight-tick octave, and spatial dimension three.
proof idea
Direct structure definition. The three fields are stated explicitly with no computational content or tactic steps.
why it matters
The definition supplies the hypothesis type for the downstream theorem ledger_structure_unique, which asserts that every discrete conservative system is isomorphic to the RS ledger with dimension 3, ratio phi, and cycle length 8. It therefore completes the uniqueness step that follows the Recognition Composition Law and the eight-tick minimality results already established upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.