IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.HilbertDisplayCompletion
Defines the finite Hilbert display carrier: an ambient complex vector on a finite set of distinction alternatives. It packages the display map, squared norm, Born weight, and the equalities that identify those quantities with FRS complex-amplitude data, plus a normalization bridge. Downstream native-delta analysis and valid-comparison examples import the carrier. The module is definition-led, with short equality and iff lemmas rather than deep proofs.
claimA finite Hilbert display is an ambient complex vector on a finite set of distinction alternatives, together with a display map, squared norm $\|\cdot\|^2$, and Born weight, satisfying the equalities that identify display norm-square and Born weight with the underlying FRS complex-amplitude data, and an iff criterion for normalization via the display.
background
Recognition Science treats measurement and comparison through finite distinction alternatives rather than an a priori infinite Hilbert space. The FRS complex-amplitude layer supplies complex amplitudes on those alternatives; ValidComparison supplies the comparison infrastructure that later modules use to judge when two displays are admissible.
This module introduces the finite Hilbert display carrier: an ambient complex vector sitting on that finite alternative set. Sibling objects include the display map itself, squared norm, Born weight, equalities linking display norm-square and Born weight to amplitude data, an iff relating normalization to the display, a norm bridge, and a headline lemma packaging the finite-display story.
The local setting is Primitive Recognition Calculus in the Foundation domain: build just enough Hilbert-like structure to host Born-type weights and normalization without committing to continuum QM axioms.
proof idea
This is a definition module, not a deep proof development. It introduces the finite Hilbert display carrier and the associated maps (display, squared norm, Born weight), then records short equality and iff lemmas (display norm-square and Born-weight identities, normalization via display, a norm bridge) that restate amplitude data in display language. The headline lemma packages those identities for downstream import. No multi-step tactic argument is the point; the content is the carrier and the identification lemmas.
why it matters in Recognition Science
The finite Hilbert display is the bridge from FRS complex amplitudes to a Hilbert-style presentation of finite alternatives, so later calculus can talk about Born weights and normalization without leaving the Recognition stack. It is imported by DeltaNativeAnalysis and DeltaNativeStrongClosure (native delta analysis and its strong closure) and by ValidComparisonExamples (concrete valid-comparison instances).
In the broader framework this sits under Foundation / Primitive Recognition Calculus: enough display structure to support comparison and delta analysis on finite alternatives, consistent with the forcing chain's discrete, self-similar skeleton (eight-tick octave, phi ladder) rather than continuum postulates. It does not itself force dimension or the J-cost; it supplies the carrier those later arguments can quote.
scope and limits
- Does not construct infinite-dimensional Hilbert space or continuum QM postulates.
- Does not prove uniqueness of the display carrier beyond the stated equalities and iff.
- Does not derive Born rule from dynamics; it only packages Born weight on the finite display.
- Does not force spatial dimension, phi, or the eight-tick octave; those live elsewhere in the chain.
- Does not discharge ValidComparison obligations; examples and analysis modules import this carrier.