Bridge
plain-language theorem explainer
Bridge is a structure that pairs any ledger instance with a trivial unit marker. Researchers deriving gauge parameters or circuit properties cite it to enforce uniform ledger handling across modules. The definition is a direct structure declaration supplying a single dummy field of unit type.
Claim. For a ledger $L$ (a carrier type equipped with optional state and tick bookkeeping), the bridge is the type containing exactly one element of the unit type.
background
A ledger is the basic carrier structure with a Carrier type, optional state, and optional tick map, introduced so downstream modules can project canonical states without extra structure. The RecogSpec.Core module supplies Bridge as the uniform wrapper over any such ledger. Upstream, the Recognition module defines an L instance whose debit and credit maps both return 1, while Cycle3 defines an L instance whose maps return 0 together with a Conserves instance.
proof idea
The declaration is a direct structure definition whose sole field is a default unit value; no lemmas or tactics are applied.
why it matters
Bridge supplies the ledger interface required by forty downstream results, including alpha_not_tunable (which derives the fine-structure constant from geometry, phi, and voxel topology) and units_self_consistent (which relates tau0 to Planck time). It therefore anchors the Recognition Science derivation chain that produces alpha inverse inside (137.030, 137.039) and the phi-ladder mass formula without introducing tunable parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.