FiniteHilbertDisplay
plain-language theorem explainer
Finite Hilbert display is the ambient carrier for finite-dimensional complex amplitudes on N+1 distinction alternatives: maps from Fin(N+1) into ℂ. Anyone wiring F_RS[i] amplitudes into Born weights, squared norms, or valid-comparison bridges cites this type. The body is a one-line type abbreviation, not a proved statement.
Claim. For each natural number $N$, the finite Hilbert display of rank $N$ is the space of complex-valued functions on the finite index set $\{0,\ldots,N\}$, i.e. maps $\mathrm{Fin}(N+1)\to\mathbb{C}$.
background
In the Primitive Recognition Calculus, native F_RS[i] amplitudes live on a finite set of distinction alternatives. To compare them with ordinary quantum language one needs an ambient Hilbert-style carrier: a complex vector whose coordinates are those alternatives.
This module builds that carrier and the display maps that send F_RS amplitudes into it. Downstream objects (squared norm, Born weight, and the valid-comparison bridge) all take vectors of this type. The double-slit amplitude in the quantum layer is the motivating pattern: a sum of complex path phases, here discretized to N+1 slots rather than a continuum screen.
The continuum bridge material in the simplicial ledger is only an upstream dependency edge in the graph; the mathematical content of this abbreviation is purely the finite complex function space.
proof idea
Definitional abbreviation only. The right-hand side is the Mathlib function type Fin (N + 1) → ℂ. No tactics, no lemmas, no proof obligations.
why it matters
This carrier is the display side of the finite Hilbert valid-comparison story. display embeds an F_RS[i] amplitude into it; normSq and bornWeight read squared modulus and per-slot Born weight off the displayed vector; normBridge packages those into a ValidComparison.Bridge whose observable is the squared norm, proving native and display observations commute. The example layer re-exports that bridge as hilbertNormBridge.
In Recognition Science terms this is scaffolding for the quantum display layer: finite complex amplitudes on distinction alternatives, with Born weights recovered from the displayed vector, not a claim about continuum Hilbert space or the full forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.