Bridge
plain-language theorem explainer
A Bridge packages a native type N, a display type D, and an observable type O with maps display : N → D, observeNative : N → O, observeDisplay : D → O, plus a commuting square: observing the display equals observing the native object. Anyone comparing RS-native quantities to laboratory or SI displays cites this interface. It is pure structure: the commuting law is the only content.
Claim. A bridge from native objects $N$ to display objects $D$ with observables $O$ consists of maps $\mathrm{display}: N \to D$, $\mathrm{observe}_{N}: N \to O$, $\mathrm{observe}_{D}: D \to O$ such that for every $n \in N$, $\mathrm{observe}_{D}(\mathrm{display}(n)) = \mathrm{observe}_{N}(n)$.
background
Recognition Science separates native quantities (phi-ladder rungs, RS units with $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$) from the displays used in experiment or SI bookkeeping. A comparison is only legitimate when both sides are read through the same observation protocol.
This module sits in PrimitiveRecognitionCalculus and introduces the minimal interface for that legitimacy. The structure does not encode a particular unit system; it only records that display and native observation commute. Downstream modules (K-display null conditions, RS-native energy coherence, cosmological gap identities) instantiate concrete bridges rather than inventing ad hoc equalities.
Upstream context includes forced $D=3$ (T8), gap and active-edge counts from GapDerivation, and certified analytic registries whose value sets stay countable. Those facts constrain what may appear as $N$ or $D$; they are not part of the Bridge fields themselves.
proof idea
No proof body: this is a structure declaration. The sole mathematical content is the field commutes, a universal equality requiring that observation after display agrees with native observation. Sibling predicates such as valid comparison then quantify over pairs of natives that share one bridge and have agreeing displayed observations.
why it matters
Bridge is the factorization point for every native-to-display comparison in the monolith. Downstream uses include units self-consistency (tau0/Planck relations), K-display null conditions and K-gate falsifiers, equality of RS-native and ordinary coherence energies, fermionic-half-equals-gap in baryon asymmetry, and $g_*$ decimal matches in cosmology.
Without a commuting bridge, displayed equalities could smuggle continuum or unit-dependent artifacts. The structure enforces the doctrine that a display comparison is valid only when both values come from natives through the same bridge and the displayed observations agree. That doctrine feeds the forcing chain's constant derivations and the alpha-band / mass-ladder displays without reopening T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.