display_bornWeight_eq
plain-language theorem explainer
For any finite F_RS[i] amplitude vector, the complex Born weight of its ambient display equals the native Born weight built from the two F_RS components. Anyone bridging native recognition amplitudes to ordinary complex Hilbert data cites this equality. The proof is pure definitional equality (rfl).
Claim. Let $\psi$ be a finite amplitude vector of length $N+1$ with values in $F_{RS}[i]$, and let $i$ index one alternative. Then the complex Born weight $|z_i|^2 = \mathrm{Re}(z_i)^2 + \mathrm{Im}(z_i)^2$ of the displayed complex amplitude equals the native weight obtained by evaluating the two $F_{RS}$ components of $\psi_i$ and summing their squares.
background
This module sits in the Primitive Recognition Calculus layer: native finite amplitudes live over the carrier $F_{RS}[i]$ (pairs of recognition-field expressions), not over $\mathbb{C}$ a priori. An FRSIAmp N is a map from Fin (N+1) into such pairs. The display map sends each pair to an ordinary complex number by evaluating real and imaginary $F_{RS}$ components.
Native Born weight is $\mathrm{eval}(\mathrm{re})^2 + \mathrm{eval}(\mathrm{im})^2$. On the ambient side, complexBornWeight is the usual $|z|^2 = \mathrm{re}^2 + \mathrm{im}^2$ for a finite complex amplitude. The GoldenInt field norm $N(a+b\varphi)=a^2+ab-b^2$ is the algebraic backbone of the carrier, but this lemma only needs the evaluation bridge into $\mathbb{R}$.
The local claim is the componentwise agreement of those two weight formulas after display.
proof idea
One-line rfl. By definition, displayAmp ψ at index $i$ is eval (ψ i), whose real and imaginary parts are exactly the evaluated $F_{RS}$ components. Unfolding complexBornWeight on that complex value therefore matches the native bornWeight definition term-for-term, so the equality is definitional.
why it matters
This is the Born-weight half of the native-to-display bridge for finite amplitudes. Downstream, HilbertDisplayCompletion.display_bornWeight_eq re-exports it under the Hilbert-display API, and finite_hilbert_display_headline packages it with the squared-norm identity: finite Hilbert space is a display of native $F_{RS}[i]$ amplitudes, and the bridge preserves Born weights, squared norm, and normalization.
In the Recognition framework this keeps probability weights honest when moving from the recognition carrier into ordinary complex amplitudes, without inserting an extra physical postulate. It is bookkeeping that makes the finite Hilbert display theorem hold by construction rather than by analytic approximation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.