hilbert_display_valid_iff
plain-language theorem explainer
Two finite complex amplitudes over the F_RS carrier are validly comparable under the Hilbert-norm display bridge exactly when their total Born weights agree. Cite this when checking that Hilbert-display equality is the native sum-of-weights predicate, not an ambient C-norm. The proof is a one-line application of the generic native-bridge equivalence to the Hilbert bridge.
Claim. For every $N\in\mathbb{N}$ and finite amplitudes $\psi,\varphi:\{0,\ldots,N\}\to F_{RS}[i]$, the pair is a valid comparison under the Hilbert-norm bridge if and only if $\sum_{i=0}^{N}|\psi_i|^2=\sum_{i=0}^{N}|\varphi_i|^2$, where each squared modulus is the native Born weight $\mathrm{Re}(\cdot)^2+\mathrm{Im}(\cdot)^2$ evaluated in $F_{RS}$.
background
In the Primitive Recognition Calculus, a finite complex amplitude is an FRSIAmp N: a map from Fin (N+1) into the F_RS[i] carrier (real and imaginary F_RS components). The native Born weight of component $i$ is $\mathrm{Re}^2+\mathrm{Im}^2$ after evaluation; the total weight is the sum over all alternatives. That is the Hilbert-display observable used here.
Valid comparison is the doctrine that two protocols may be equated only after a named bridge maps them to a common native predicate. The Hilbert-norm bridge is the concrete bridge for finite Hilbert display, parallel to the real-value and finite-probability bridges in the same module.
Upstream, validComparison_iff_native states that validity under a bridge is definitionally the native equality that bridge exposes. Born-weight agreement with ambient complex display is already recorded in the FRS complex-amplitude layer.
proof idea
One-line term proof: apply ValidComparison.validComparison_iff_native at the Hilbert-norm bridge and the two amplitudes. That generic lemma rewrites IsValidComparison bridge x y into the bridge's native equality; for the Hilbert bridge the native side is equality of summed Born weights. No extra algebra is needed.
why it matters
This is the Hilbert leg of the three concrete valid-comparison examples. Downstream, valid_comparison_examples_headline packages the real, probability, and Hilbert bridges into one conjunction: the doctrine is not abstract, it has working displays. The headline's third conjunct is exactly this biconditional (paired with the bridge definition).
In Recognition terms, Born weight is the display of recognition cost on a finite alternative set; equating total weight is the correct sameness test before any continuum Hilbert-space story. The result stays finite-dimensional (register size $N+1$), consistent with the finite 8-tick / matrix-exponential stance elsewhere in Foundation. It does not itself force $D=3$ or the octave; it only certifies the comparison rule used when Hilbert display appears in later forcing or measurement arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.