DiscreteLedger
plain-language theorem explainer
DiscreteLedger packages a LedgerForcing ledger with a DiscretenessForcing discrete configuration space to model finite-step self-similar structures. Researchers deriving the golden ratio from ledger self-similarity cite it as the base object for the phi-forcing argument. The definition is a direct structure pairing the two imported components with no extra axioms or proofs.
Claim. A discrete ledger is a pair $(L, S)$ where $L$ is a ledger from the LedgerForcing framework and $S$ is a discrete configuration space whose configurations form a finite positive subset of the reals with a positive minimum gap in J-cost between adjacent elements.
background
The PhiForcing module shows that self-similarity plus J-cost on a discrete ledger forces the scale ratio to be the golden ratio. DiscreteConfigSpace supplies a finite set of positive real configurations together with a minimum J-cost gap that traps states at local minima. LedgerForcing.Ledger supplies the underlying ledger operations. Upstream, the CellularAutomata step applies a local rule to produce the successor tape, while A denotes the active edge count per fundamental tick (equal to 1 in both Masses.Anchor and Modal.Actualization).
proof idea
The structure is defined directly by bundling the ledger field from LedgerForcing with the discrete_space field from DiscretenessForcing; no tactics or lemmas are applied.
why it matters
DiscreteLedger is the input type for is_self_similar and the phi_forced theorem, which conclude that any self-similar discrete ledger must have scale ratio exactly phi. It therefore occupies the position of T6 in the forcing chain (phi forced as the self-similar fixed point) and supplies the concrete object needed for the eight-tick octave and D=3 spatial dimensions. The same structure appears in the IC-003 certificate establishing that RS dynamics remain approximable by rational arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.