normBridge
plain-language theorem explainer
Packages the native-to-Hilbert comparison as a valid-comparison bridge with squared norm as the shared real observable. Anyone treating finite Hilbert space as a display of native F_RS[i] amplitudes cites this construction. The commuting square is a one-line appeal to the already-proved equality of displayed complex norm with the native Born-weight sum.
Claim. For each natural number $N$, there is a valid-comparison bridge from native $F_{RS}[i]$ amplitudes on $N+1$ alternatives to the finite Hilbert carrier $\mathrm{Fin}(N+1)\to\mathbb{C}$, with real observable given by squared norm: native observation is the sum of Born weights, display observation is the squared Hilbert norm, and these commute with the display map.
background
In the primitive recognition calculus, a native finite amplitude is an $F_{RS}[i]$-valued assignment on $N+1$ distinction alternatives. Each component carries real and imaginary $F_{RS}$ data; the native Born weight at site $i$ is the sum of squares of the evaluated real and imaginary parts. The finite Hilbert display is the ordinary complex vector space $\mathrm{Fin}(N+1)\to\mathbb{C}$ obtained by evaluating those components.
A valid-comparison bridge is a structure with a display map, a native observable, a display observable, and a commuting square: observing after display equals observing natively. Here the shared observable is squared norm (sum of Born weights on the native side; complex squared norm on the display side).
Upstream, display_normSq_eq already records that the displayed complex norm equals the native Born-weight sum, by definitional unfolding of the display map.
proof idea
Structure-instance definition, not a deep proof. The display field is the existing native-to-complex display map. Native observation is the finite sum of native Born weights over $\mathrm{Fin}(N+1)$. Display observation is the in-module squared-norm functional on Hilbert vectors. The commuting obligation is discharged in one tactic step by applying the upstream theorem that displayed complex norm equals the native Born-weight sum.
why it matters
This is the bridge object that lets finite Hilbert space sit inside the valid-comparison layer rather than as an ad-hoc rewrite. Downstream, the finite Hilbert display headline packages the preservation of Born weights, squared norm, and normalization, and states that comparison by norm is valid through this native/display/observable bridge. The examples module re-exports the same bridge under a shorter name for use as a worked valid-comparison instance.
In the broader Recognition stack this is display infrastructure, not a forcing-chain step: it shows that ordinary finite-dimensional Born-rule Hilbert data is a faithful readout of native $F_{RS}[i]$ amplitudes, so later claims about measurement and normalization can be stated once on the native side and transported.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.