SigmaLayer/UnifiedMeasurement: dynamics and measurement on ONE many-to-one ontic model (SL-T5)

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

The primary structural closure item. The forward capstone (product_projectiveSector_forward_capstone) lives on Σ = ℂℙ^{M} × T² with the exp(-itH) Hamiltonian flow; the measurement capstone (lifted_projectiveSector_measurement_born_capstone) lived on the dilated ℂℙ^{M} with trivialDynamics. They used DIFFERENT ontic models. This module puts BOTH on the SAME (Σ, μL, Φ, π):

• Σ = KSigma (M+1) = ℂℙ^{M} × T², μL = kMuL = μFS ⊗ vol, π = Prod.fst (productSector);
• the ISOLATED dynamics is the genuine Hamiltonian flow productDynamics H hH p₀ (Φ_t(p,θ) = (exp(-itH)•p, θ)), NOT trivialDynamics;
• the DE-ISOLATION measurement is a DeisolationModel over that same productDynamics whose interaction is the LF5 von Neumann flow lifted to the fibre, Φ_meas(p,θ) = (measurementFlow p, θ), with the pointer readout vnPointerOutcome ∘ π.

unified_projectiveSector_capstone then delivers, on the ONE model productDynamics H hH p₀:

1. the isolated flow is measure-preserving (flow_preserves);
2. it projects through π = Prod.fst to exp(-itH) • · — the Schrödinger pillar (productDynamicsBridge);
3. π_* μL = μFS — the Fubini-Study bridge (B1);
4. the de-isolation interaction (on the SAME Σ, μL) is measure-preserving;
5. the contextual pointer readout is defined almost everywhere (target T6, lifted through the fibre);
6. the readout records the established outcome (bridge B5).

So one (Σ, μL, Φ, π) carries isolated Hamiltonian evolution AND de-isolating measurement AND records AND the Fubini-Study/Born content — removing the forward-vs-measurement model split. The Born outcome FREQUENCIES are the base-space statement vnDeisolationModel_born_frequency (the readout factors through π, so its i.i.d. law lives on the base ℂℙ^{M}). Follow-on residue (see specs/future-work.md SL-T5): physical record persistence, nonzero post-outcome preparation, the conditional→Lüders link.

Consistency witness, not derivation (scope discipline). This is ONE concrete model with μL = μFS ⊗ vol and Φ_t = (e^{-itH}·[p], θ) built in; the capstone is a compatibility statement about the witness, not a derivation of the projective geometry / FS measure / unitary evolution from a primitive ontology. Two frontiers sit outside it: SO-1 (the sector origin) and MD-1 (the Paper C A7 mismatch — the readout cells bornRegion ψ' are preparation-indexed, not the context-fixed Ωᵢ(M) of A7, so readout_ae_total is a preparation-indexed operational witness). See specs/reconstruction-status.md §7.

noncomputable def CSD.SigmaLayer.vnRecordSemanticsProd {N M : ℕ} (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) : RecordSemantics (LF4.KSigma (M + 1)) (vnRecordSignature N)

The record semantics on the product ontic space: the event of pointer outcome i is the fibred pointer preimage {(p,θ) | vnPointerOutcome p = some i} (the base pointer fibre pulled back through π = Prod.fst).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.SigmaLayer.unifiedDeisolationModel {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) : DeisolationModel (productDynamics H hH p₀) (vnRecordSignature N) (vnRecordSemanticsProd e ψ' hψ'0) Unit

The unified de-isolation model. A DeisolationModel over the NONTRIVIAL isolated dynamics productDynamics H hH p₀ (the exp(-itH) Hamiltonian flow), on the same Σ = ℂℙ^{M} × T². The interaction is the LF5 measurement flow on the base fibre (p,θ) ↦ (measurementFlow p, θ); the readout is the base pointer outcome; the outcome regions are the fibred pointer fibres. Every field is discharged by an LF4/LF5 lemma.

Equations

• One or more equations did not get rendered due to their size.

Why the record persists: the register is frozen, and that is a theorem, not a reading

records_time_physical (SigmaLayer/FiniteQMClosure.lean) says the record probability is conserved and the record is flow-covariant. It is easy to read that as apparatus memory — a pointer latching and holding. It is not. The two lemmas below say exactly what the model does: the de-isolation interaction leaves the register coordinate untouched, and the readout never looks at it. So persistence here is register-freezing by construction, and naming it as a theorem keeps the stronger reading from being taken for free (SigmaLayer/TimeIndexedRecord.lean, "Honest scope").

@[simp]

theorem CSD.SigmaLayer.unifiedDeisolationModel_interaction_register {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) (t : OnticTime) (c : (vnRecordSignature N).Context) (x : LF4.KSigma (M + 1)) : ((unifiedDeisolationModel H hH p₀ e ψ' hψ'0).interaction t c x).2 = x.2

★ The interaction freezes the register. The de-isolation interaction acts only on the base coordinate; the KTorus register is carried through unchanged. This is what "persistence by construction" means, stated so it can be checked rather than believed.

theorem CSD.SigmaLayer.unifiedDeisolationModel_readout_register_irrelevant {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) (c : (vnRecordSignature N).Context) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin (M + 1)))) (r r' : LF4.KTorus) : (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).readout () c (p, r) = (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).readout () c (p, r')

★ The readout ignores the register. Two ontic states sharing a base coordinate read out the same outcome whatever their register values. Together with the lemma above: nothing in this model writes to the register, and nothing reads from it. A latching-memory model would have to do both.

theorem CSD.SigmaLayer.unifiedDeisolationModel_records {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) : (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).RecordsEstablishedOutcome

The readout records the established outcome (B5) on the unified model.

theorem CSD.SigmaLayer.unifiedDeisolationModel_ae_total {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) (hψ' : ‖ψ'‖ = 1) : (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).AETotalReadout () () 0 (LF4.kMuL p₀)

Almost-everywhere defined readout (T6) on the unified model. For almost every ontic state (p,θ) under the product Liouville measure μFS ⊗ vol, the pointer readout after the de-isolation interaction is defined. The predicate depends only on the base p, so it lifts the base statement vnDeisolationModel_ae_total through Prod.fst (whose pushforward of kMuL is μFS).

theorem CSD.SigmaLayer.unified_projectiveSector_capstone {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) (hψ' : ‖ψ'‖ = 1) : (∀ (t : OnticTime), MeasureTheory.MeasurePreserving ((productDynamics H hH p₀).flow t) (LF4.kMuL p₀) (LF4.kMuL p₀)) ∧ (∀ (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)) ∧ HasFubiniStudyPushforward (productSector H hH p₀) p₀ ∧ (∀ (t : OnticTime) (c : (vnRecordSignature N).Context), MeasureTheory.MeasurePreserving ((unifiedDeisolationModel H hH p₀ e ψ' hψ'0).interaction t c) (LF4.kMuL p₀) (LF4.kMuL p₀)) ∧ (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).AETotalReadout () () 0 (LF4.kMuL p₀) ∧ (unifiedDeisolationModel H hH p₀ e ψ' hψ'0).RecordsEstablishedOutcome

SL-T5: dynamics and measurement on one many-to-one ontic model. For Σ = ℂℙ^{M} × T², the Liouville measure μFS ⊗ vol and π = Prod.fst, the SAME productDynamics H hH p₀ carries:

1. a measure-preserving isolated Hamiltonian flow;
2. projectable through π to the Schrödinger flow exp(-itH) • ·;
3. π_* μL = μFS (Fubini-Study bridge);
4. a measure-preserving de-isolation measurement interaction (on the same Σ, μL);
5. an almost-everywhere defined contextual pointer readout;
6. record establishment.

One ontic model behind isolated evolution, measurement, records and the Born/Fubini-Study content.