Bridge
plain-language theorem explainer
Bridge supplies a minimal type wrapper around any Ledger instance to parameterize recognition states for downstream constant derivations and complexity separations. Researchers deriving units or proving circuit properties cite this to instantiate ledger-specific bridges without extra data. The definition is a direct structure with a single defaulted dummy unit field and no proof obligations.
Claim. Let $L$ be a ledger with carrier type, optional state, and optional tick function. Then Bridge$(L)$ denotes the structure type whose sole field is a dummy element of type Unit.
background
Ledger is the basic carrier structure with a Carrier type plus optional state and tick bookkeeping, allowing downstream modules to project canonical states. The Recognition module supplies a default L with debit and credit both constantly 1. Cycle3 supplies an L with debit and credit both 0 together with a Conserves instance. The Bridge definition lives in RecogSpec.Core to serve as a neutral interface for ledger-dependent constructions.
proof idea
Direct structure definition. The body introduces Bridge as a Type parameterized by Ledger and populates it with a single dummy field of type Unit defaulted to (). No lemmas, tactics, or reductions are invoked.
why it matters
Bridge feeds the alpha_not_tunable theorem that derives the fine-structure constant from cube geometry, voxel topology, and the phi fixed point; the units_self_consistent theorem relating tau0 to Planck time over pi; and circuitSeparation that assembles recognition-time bounds with moat and decoder results. It supplies the ledger interface required by the Recognition Science constant derivations and falsifier constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.