SigmaLayer/FiniteQMClosure: the tiered finite-dimensional QM closure (#6)

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

The capstone bundle. Every earlier module proves ONE reconstructed fact on the single many-to-one ontic model productDynamics H hH p₀ (isolated Hamiltonian flow exp(-itH) on Σ = ℂℙ^M × T², Liouville measure μL = μFS ⊗ vol, projection π = Prod.fst). This module collects the ones that are GENUINELY PROVED on that model into a single record FiniteQMClosure, discharged by unifiedFiniteQMClosure, and — crucially — states honestly, tier by tier, what is a theorem here, what is a projective-sector posit, what is a textbook-QM adapter, and what is still open. No field is sorry; the structure carries only real theorems, and the non-theorem tiers live in this docstring, not in fabricated fields.

This is a concrete consistency witness, not a derivation of the Paper C architecture. The model productDynamics H hH p₀ has μL = μFS ⊗ vol and Φ_t = (e^{-itH}·[p], θ) built IN, so the pushforward-to-μFS (fubini_study_bridge) and the Schrödinger projection (schrodinger_projection) are compatibility facts about the witness — NOT derivations of projective geometry, the Fubini–Study measure, or unitary evolution from a more primitive ontic model. The precise claim unifiedFiniteQMClosure earns is: operational finite-QM closure holds on a concrete projective product witness satisfying the exact formalised subset of the Paper C assumptions (specs/reconstruction-status.md §2, the A1–A7 map). It does NOT claim the witness derives that architecture. The two genuinely open frontiers sit OUTSIDE this closure: SO-1 (the sector-origin problem — the origin of (Σ, π, μL); the trials SAMPLE μL) and MD-1 (the Paper C A7 mismatch — the measurement cells bornRegion ψ' are preparation-indexed, not the context-fixed Ωᵢ(M) of A7; the readout here is an honest preparation-indexed operational witness). See specs/BACKLOG.md (SO-1, MD-1).

Tier 1 — PROVED on the unified model (the fields of FiniteQMClosure)

All eleven on the ONE model productDynamics H hH p₀:

• isolated_flow_measure_preserving — the isolated flow preserves μL (ConstraintDynamics.flow_preserves);
• schrodinger_projection — π ∘ Φ_t = exp(-itH) • · (productDynamicsBridge.projectable);
• fubini_study_bridge — π_* μL = μFS, i.e. B1 (productSector_hasFubiniStudyPushforward);
• measurement_preserving — the de-isolation interaction preserves μL (measurementFlow_measurePreserving);
• readout_ae_total — the contextual pointer readout is a.e. defined (T6, unifiedDeisolationModel_ae_total);
• records_established — the readout records the established outcome, B5 (unifiedDeisolationModel_records);
• records_time_physical — the time-indexed record probability is conserved and flow-covariant, #5 (unified_records_persistence);
• born_frequency — i.i.d. trials of μL have outcome-region frequency → ‖⟨eᵢ,ψ⟩‖², #2, for EVERY unit ψ (no genericity hypothesis — the hpos full-support requirement is retired via the _uncond engine, unified_born_frequency / born_frequency_convergence_N_uncond; vanishing amplitudes give FS-null regions whose frequencies converge to 0 = their Born weight);
• conditioning_is_luders — record conditioning = Lüders update as predictions, #3/#4 (conditioning_luders_effect_equivalence);
• mixed_born — mixed states on the model (#8 C, weight level): for every density operator ρ, the classical mixture over ρ's spectral ensemble of ontic Born-region measures reproduces Tr(ρ Eᵢ) (mixed_ontic_born_weight) — so the model carries mixed-state Born content, not only the pure ψ;
• mixed_born_frequency — the same mixed content as an a.s. FREQUENCY (#8 C, LLN): i.i.d. two-stage trials (spectral component ~ λ, then microstate ~ μL) have outcome-i frequency → Tr(ρ Eᵢ) (unified_mixed_born_frequency) — mixed-state Born as certified frequencies, not only weights.

Tier 2 — ASSUMED under projective sector

The interpretive commitment that makes the above a reconstruction of QM rather than a study of a measure space: taking the Fubini-Study/Liouville measure on ℂℙ^M × T² to BE the ontic probability law (projective sector; see specs/future-work.md). This is a stance, not a Lean proposition, and is deliberately NOT a field. The structural sub-posits that a bare Choice-A reconstruction would ALSO assume are, on this concrete model, already DISCHARGED (hence they appear as tier-1 fubini_study_bridge etc., not here) — with one honest exception recorded separately:

• B6 (composite tensor structure) — that a joint system's algebra is M_m ⊗ M_n. Posited per instance in CompositeSector, OR derived: CSD.SigmaLayer.CompositeSector.ofReconstruction (SigmaLayer/TensorReconstruction.lean, composite_dim_eq) builds a CompositeSector whose tensor_dimension is PROVED from the composite algebra being simple — so B6 is "assumed OR dischargeable", not a gap. This is single-system closure; B6 belongs to the composite track and is intentionally outside FiniteQMClosure.

Tier 3 — QM ADAPTERS (restatements into textbook QM, elsewhere)

SigmaLayer/Adapters.lean, SigmaLayer/CompositeAdapters.lean: the maps taking these ontic facts to their standard Hilbert-space QM statements (density operators, Lüders channel, Born rule). They translate; they do not add reconstruction content.

Open residue (outside the closure)

The mixed-state / ensemble representation (#8) that was once "Tier 4 open" is now fully closed and lives in the closure as fields: the statistical side (#8 A+B, SigmaLayer/MixedEnsemble.lean), the ontic-side WEIGHT-level representation (mixed_born / mixed_ontic_born_weight), AND the a.s. FREQUENCY LLN (mixed_born_frequency / unified_mixed_born_frequency, SigmaLayer/MixedFrequency.lean). So the closure's QM content is complete on the witness. What remains open is NOT a QM item but the two architecture frontiers already named above:

• SO-1 — the sector-origin problem RETIRED as a non-question (2026-07-24; Corrected 2026-08-04 (codebase audit).): Σ is the floor — there is nothing beneath it to derive it from. What is legitimate, and ongoing, is constraining Σ from above. Formerly: derive (Σ, π, μL) + FS typicality from a primitive ontology (specs/BACKLOG.md, SigmaLayer/SectorPostulateNoGo.lean proves the single-flow no-go);
• MD-1 — the Paper C A7 measurement-partition mismatch: the outcome cells bornRegion ψ' are preparation-indexed, not the context-fixed Ωᵢ(M) of A7 (specs/BACKLOG.md). Progress: the record-layer readout now has a first-class successor, SigmaLayer/RecordLayerClosure.lean (recordLayerClosure, built on SigmaLayer/FibreRecord.lean), whose outcome probabilities are measurement-noncontextual (‖ψ i‖² from the fibre typicality of a genuine P5 RecordSemantics event). It is realised on this very model in SigmaLayer/ProjectiveRecord.lean: a P5 RecordSemantics on Σ = CPN (M+1) whose events are these bornRegions, whose outcome map is bornOutcome, and whose FS-typicality frequency is Born (projRecord_frequency, the same born_frequency conclusion carried by the record semantics rather than by vnPointerOutcome). The probabilities are the Kähler moment map (SigmaLayer/MomentMapRace.lean) and the statistics are the law of large numbers over the unknown microstate (Measurement.bornMeasurement_frequency) — no dynamical postulate. What is not done is re-plumbing the field wiring of unifiedFiniteQMClosure itself onto the record semantics (a mechanical restatement carrying no new theorem); the regions remain preparation-indexed. See specs/record-layer-plan.md.

References

specs/future-work.md (SL-T5, SL-T6, projective sector); specs/reconstruction-status.md; specs/connectivity-manifest.md (L9). Source theorems: unified_projectiveSector_capstone (SigmaLayer/UnifiedMeasurement.lean), unified_records_persistence, unified_born_frequency (SigmaLayer/UnifiedFlowedRecords.lean), conditioning_luders_effect_equivalence (SigmaLayer/ConditioningLuders.lean), CompositeSector.ofReconstruction (SigmaLayer/TensorReconstruction.lean).

structure CSD.SigmaLayer.FiniteQMClosure {N M : ℕ} [NeZero N] (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) : Prop

The tiered finite-dimensional QM closure (Tier 1). A record of exactly the reconstructed QM facts that are GENUINELY PROVED on the single ontic model productDynamics H hH p₀ (measurement reference state ψ', Born state ψ). Every field is a theorem discharged by unifiedFiniteQMClosure; the projective-sector posit, QM adapters, and open residue are documented in the module header, not encoded as fields.

• isolated_flow_measure_preserving (t : OnticTime) : MeasureTheory.MeasurePreserving ((productDynamics H hH p₀).flow t) (LF4.kMuL p₀) (LF4.kMuL p₀)

  The isolated Hamiltonian flow preserves the Liouville measure.

• schrodinger_projection (t : OnticTime) (x : LF4.KSigma (M + 1)) : (productSector H hH p₀).pi ((productDynamics H hH p₀).flow t x) = productProjectedFlow H hH t ((productSector H hH p₀).pi x)

  The isolated flow projects through π to the Schrödinger flow exp(-itH) • · (Schrödinger pillar).

• fubini_study_bridge : HasFubiniStudyPushforward (productSector H hH p₀) p₀

  π_* μL = μFS: the Fubini-Study bridge (B1).

• measurement_preserving (t : OnticTime) (c : (vnRecordSignature N).Context) : MeasureTheory.MeasurePreserving ((unifiedDeisolationModel H hH p₀ e ψ' hψ'0).interaction t c) (LF4.kMuL p₀) (LF4.kMuL p₀)

  The de-isolation measurement interaction preserves μL (on the same Σ, μL).

• readout_ae_total : (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).AETotalReadout () () 0 (LF4.kMuL p₀)

  The contextual pointer readout is defined almost everywhere (T6).

• records_established : (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).RecordsEstablishedOutcome

  The readout records the established outcome (B5).

• records_time_physical (c : (vnRecordSignature N).Context) (i : (vnRecordSignature N).Outcome c) : (∀ (t : OnticTime), ↑(productDynamics H hH p₀).muL ((unifiedFlowedSemantics H hH p₀ e ψ' hψ'0).event { context := c, outcome := i, time := t }) = ↑(productDynamics H hH p₀).muL ((fun (x : LF4.KSigma (M + 1)) => LF5.vnPointerOutcome ψ' hψ'0 e x.1) ⁻¹' {some i})) ∧ ∀ (s t : OnticTime), (unifiedFlowedSemantics H hH p₀ e ψ' hψ'0).event { context := c, outcome := i, time := t + s } = (productDynamics H hH p₀).flow s ⁻¹' (unifiedFlowedSemantics H hH p₀ e ψ' hψ'0).event { context := c, outcome := i, time := t }

  Time-indexed records are physical: probability is conserved and the record is flow-covariant (#5).

• born_frequency {Ω : Type} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.KSigma (M + 1)) : (∀ (n : ℕ), Measurable (X n)) → (∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = ↑(productDynamics H hH p₀).muL) → (∀ (i : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' (productSector H hH p₀).pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator fun (x : Ω) => 1)) → ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' (productSector H hH p₀).pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

  Born frequency on the model: i.i.d. trials of μL land in π⁻¹(bornRegion i) with frequency → ‖⟨eᵢ,ψ⟩‖² (#2).

• conditioning_is_luders (S T : Finset (Fin (M + 1))) : ‖ψ‖ = 1 → bayesianConditional (fun (U : Finset (Fin (M + 1))) => (↑(productDynamics H hH p₀).muL ((productSector H hH p₀).pi ⁻¹' ⋃ k ∈ U, LF4.bornRegion ψ hψ0 k)).toReal) T S = bayesianConditional (fun (U : Finset (Fin (M + 1))) => ∑ k ∈ U, ‖inner ℂ (EuclideanSpace.single k 1) ψ‖ ^ 2) T S

  Record conditioning = Lüders update as predictions, for every pointer-basis effect (#3/#4).

• mixed_born (ρ : LF2.DensityOperator (M + 1)) (i : Fin (M + 1)) : ∑ j : Fin (M + 1), ⋯.eigenvalues j * (↑(productDynamics H hH p₀).muL ((productSector H hH p₀).pi ⁻¹' LF4.bornRegion (⋯.eigenvectorBasis j) ⋯ i)).toReal = LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)

  Mixed states on the model (#8 C, weight level): for every density operator ρ and pointer outcome i, the classical mixture — over ρ's spectral ensemble — of ontic Born-region measures reproduces the density-operator Born rule Tr(ρ Eᵢ). The model represents mixed states, not only the pure ψ.

• mixed_born_frequency (ρ : LF2.DensityOperator (M + 1)) {Ω : Type} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (Y : ℕ → Ω → Fin (M + 1) × LF4.KSigma (M + 1)) : (∀ (n : ℕ), Measurable (Y n)) → (∀ (n : ℕ), MeasureTheory.Measure.map (Y n) Pr = mixtureMeasure H hH p₀ ρ) → (∀ (i : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (Y n ⁻¹' mixtureRegion H hH p₀ ρ i).indicator fun (x : Ω) => 1)) → ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (Y k ⁻¹' mixtureRegion H hH p₀ ρ i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)))

  Mixed-state Born FREQUENCY on the model (#8 C, a.s. limit): for i.i.d. two-stage trials of any ρ (draw a spectral component ~ λ, then an ontic microstate ~ μL), the frequency of outcome i converges a.s. to Tr(ρ Eᵢ). So the model carries mixed-state Born statistics as certified frequencies, not only weights — the last open QM item in the closure.

theorem CSD.SigmaLayer.unifiedFiniteQMClosure {N M : ℕ} [NeZero N] (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ' : ‖ψ'‖ = 1) (hψ : ‖ψ‖ = 1) : FiniteQMClosure H hH p₀ e ψ' hψ'0 ψ hψ0

The finite-dimensional QM closure holds on the unified model. Every tier-1 field is discharged by its source lemma on the single ontic model productDynamics H hH p₀. Requires only the normalisations of the measurement reference state ψ' and the Born state ψ — the whole reconstruction (dynamics, measurement, records, Born frequency, conditioning=Lüders) is a theorem on one model, with the projective-sector posit and open residue (SO-1, MD-1) as documented (module header), not as hidden gaps.