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. ⚠️ Frontier statement corrected 2026-09-05 — both labels below are retired or closed. SO-1 was retired as a non-question (2026-07-24: Σ is the floor, there is nothing beneath it to derive it from; what survives is constraint work such as fsMeasure_unique). MD-1 was closed (2026-08-31), its residuals being the permanent boundary R-015 and the open-mathematics item R-016. The A7 mismatch recorded below is real but is a property of this witness: the cells here are preparation-indexed bornRegion ψ', whereas RecordLayer/GlobalBasin.lean gives a context-fixed partition at every N. What sits outside this closure and is genuinely open is Posit 1's discharge condition — deriving the rate field from the de-isolation dynamics (specs/POSITS.md, "What 'frontier' means here"). The original wording, kept for the A7 point it makes: the measurement cells bornRegion ψ' are preparation-indexed, not the context-fixed Ωᵢ(M) of A7; the readout here is an honest preparation-indexed operational witness.

Which trilemma horn this closure pays

Records, exact Born and continuity are jointly impossible, so every witness in the record layer pays exactly one price: seams (piecewise witness), ε-Born (smooth witness), or Dirac calibration (null-seam witness). This closure pays seams, and it is worth naming because a reader can otherwise take the closure for a free lunch.

The interaction here is unitary — measurementFlow N e p = vnUnitaryReindexed N e • p (LF5/MeasurementFlow.lean), so it is continuous and measure-preserving — and the Born weights are exact. What gives is totality of the readout: the closure's field is readout_ae_total, i.e. AETotalReadout, records defined almost everywhere rather than everywhere. That is forced, not chosen: no_everywhere_correlation (RecordLayer/MeasurementConstraints.lean) proves an everywhere-defined correlation is impossible for any continuous Φ at n ≥ 2, and its exceptional set is necessarily non-empty — it contains the seams between selector sectors.

⚠️ no_everywhere_correlation prices the everywhere case only. It does not bound the exceptional set's measure and does not rule out an a.e. correlation whose exceptional set has positive measure. The theorem that forces positive measure is posMeasure_noRecord_pointer (RecordLayer/NoRecordGeometry.lean), and it is about the pointer's own geometry, not this model. So "a.e., with a null seam" is a coherent position here and is the one this closure occupies.

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). ⚠️ Read this as register-freezing, not as apparatus memory. The interaction carries the register coordinate through unchanged and the readout never inspects it — both are theorems, not readings (unifiedDeisolationModel_interaction_register, unifiedDeisolationModel_readout_register_irrelevant). So the record persists here because nothing in the model can disturb it; a pointer that physically latches and holds would have to write to the register and read from it, and this model does neither (SigmaLayer/TimeIndexedRecord.lean, "Honest scope"). ⚠️ Generic recurrence is deferred. A measure-preserving flow on a finite-measure space returns (Poincaré, and quantitatively Kac — Mathlib/Dynamics/Kac.lean, tsum_measure_lt_returnTime), so indefinite persistence is not available from conservation alone. What would break recurrence is record proliferation, and that tier is not built;
• 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, RecordLayer/RecordLayerClosure.lean (recordLayerClosure, built on RecordLayer/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 RecordLayer/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 (RecordLayer/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.