UnitsEqv
plain-language theorem explainer
UnitsEqv equips bridges over a ledger with an equivalence relation. Researchers extracting dimensionless predictions from recognition specifications cite this structure to group equivalent bridge states. The declaration is a direct structure definition that encodes reflexivity, symmetry, and transitivity on the bridge carrier.
Claim. Let $L$ be a ledger. An equivalence relation $R$ on the bridges over $L$ satisfies $R(B,B)$ for every bridge $B$, symmetry, and transitivity.
background
Ledger is a carrier type augmented with optional state and tick bookkeeping fields. Bridge over a ledger is a minimal wrapper containing a unit dummy. The definition sits in RecogSpec.Core, which handles recognition specifications and observable payloads extracted from bridges.
proof idea
Direct structure definition. It declares the relation field together with the three equivalence axioms; no lemmas or tactics are applied.
why it matters
The structure supports extraction of dimensionless predictions from bridges. It supplies the equivalence needed for units in ledger-based models within the Recognition framework. No downstream theorems are recorded, leaving integration with the phi-ladder and forcing chain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.