pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Bridge

show as:
view Lean formalization →

Bridge supplies a minimal wrapper type over any Ledger instance, enabling uniform reference to ledger states in downstream modules without adding structure. Researchers deriving constants or circuit separations cite it to maintain ledger coherence across recognition cycles. The definition is a direct structure with a single dummy unit field.

claimFor any ledger $L$, the bridge $Bridge(L)$ is the type containing exactly one element of type $Unit$.

background

A Ledger is a structure with a Carrier type, optional state, and optional tick function for bookkeeping, as defined in the same module. The Bridge structure attaches to any such Ledger to allow projection of canonical states. Upstream, the Recognition module defines an L instance with unit debit and credit, while Cycle3 supplies a zero-valued L that satisfies the Conserves instance.

proof idea

The declaration is a direct structure definition with a default unit field, requiring no lemmas or tactics.

why it matters in Recognition Science

This structure appears in forty downstream uses, 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 closes the ledger-to-constants bridge in the Recognition framework, supporting the path from J-uniqueness through the eight-tick octave to observable parameters.

scope and limits

formal statement (Lean)

  17structure Bridge (L : Ledger) : Type where
  18  dummy : Unit := ()

proof body

Definition body.

  19
  20/-- Units equivalence relation over bridges. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.