LedgerState
plain-language theorem explainer
LedgerState is identified with the eight-component complex signal carrier Signal8. Anyone wiring older ledger APIs (time, Z-patterns, bonds, recognition cost) into the analytic RecognitionOperator cites this alias. The body is a pure type abbreviation, not a proved equivalence.
Claim. By definition, a ledger state is an eight-tick complex signal: $\mathrm{LedgerState} := \mathrm{Signal}_8$, where $\mathrm{Signal}_8$ is the forced eight-component carrier from the complex-structure forcing development.
background
This module hosts the analytic RecognitionOperator on the eight-tick carrier. Several older bridge modules still expect a ledger-shaped API with fields such as time, Z-patterns, active bonds, and recognition cost. The local fix is a compatibility surface: rename the carrier so those modules type-check without restoring a separate ledger datatype.
Signal8 is imported from ComplexStructureForcing and is the canonical 8-tick state space aligned with the forced octave (period $2^3$). Upstream modules define richer ledger structures (N positive ratios with a tick index; lists of recognition events; finite active bonds with positive multipliers). Here those notions are stubbed or projected onto the signal carrier rather than reintroduced as independent state types.
The namespace LedgerState then exposes the legacy field names as definitions on that alias, so call sites can keep writing ledger-style projections while the underlying object remains the eight-component signal.
proof idea
No proof. The declaration is a one-line type abbreviation equating LedgerState with Signal8. Downstream field stubs (active_bonds, bond_multipliers, admissible, etc.) are defined in the opened namespace and ignore or trivialize the signal argument where the old ledger data are not yet reconstructed.
why it matters
Without this alias, the RecognitionOperator file cannot serve both the analytic 8-tick operator and the older ledger bridges that feed Hamiltonian emergence, bond accounting, and admissibility checks. Downstream definitions such as active_bonds, bond_multipliers, bond_pos, bond_agents, channels, global_phase, and admissible all take a LedgerState argument; diagonalHamiltonian sits in the same foundation layer that expects a coherent state type.
In the Recognition framework this sits under the eight-tick octave (T7): the carrier is forced to period $2^3$, and the ledger language is kept only as a compatibility skin. It does not itself force D = 3, J-uniqueness, or the mass ladder; it keeps the operator API stable while those results live elsewhere in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.