SigmaLayer/ProjectiveRecord: the record layer on the actual projective Σ (MD-1, migration)

Category: 7-SigmaLayer (the record layer — realised on the corpus's real model).

The record-layer framing of SigmaLayer/FibreRecord.lean was built on an abstract fibre Σ = ℝ. This file migrates it onto the corpus's actual measurement model: the projective space Σ = CPN (M+1) = ℂℙ^M, with the corpus's own outcome regions bornRegion (LF4/BornRegionDisjoint), its per-microstate outcome map bornOutcome, and the Fubini–Study measure fubiniStudyMeasure — the exact objects FiniteQMClosure.born_frequency is stated with. So the record layer is no longer a parallel construction; it is instantiated on the real Σ with the real Born machinery.

What is delivered, foundational-triple, no sorry:

• projRecordSemantics — a genuine postulate-P5 RecordSemantics on CPN (M+1): the record event of "context ⟨ψ,·⟩ recorded outcome i" is bornRegion ψ i, measurable (bornRegion_measurable_uncond) and exclusive within a context (bornRegion_pairwiseDisjoint);
• bornOutcome_eq_record — the corpus's per-microstate outcome map bornOutcome is the record: it reads i exactly on the record event (via bornOutcome_eq_some_iff);
• compatibleSet_proj_single — isolation on one record conditions the ontic state onto the born region (the P6 story on the real Σ);
• fubiniStudy_projRecord — the FS typicality of the record event of outcome i is exactly ‖⟨eᵢ,ψ⟩‖² (bornRegion_fs_measure_uncond): Born as the ontic typicality of the record event;
• projRecord_frequency — Born as the law of large numbers over the unknown microstate, on the real Σ: for i.i.d. FS-typical microstates, the frequency of trials whose microstate lands in the record event of i converges a.s. to ‖⟨eᵢ,ψ⟩‖² (via freq_tendsto_of_iid + bornRegion_fs_measure_uncond). This is the exact FiniteQMClosure.born_frequency conclusion, now carried by the record-layer RecordSemantics rather than the ad-hoc vnPointerOutcome readout.

Honest scope. This connects the record-layer interface to the corpus's real model and its Born machinery — the substantive content of "retiring vnPointerOutcome". It does not rewrite the field wiring of unifiedFiniteQMClosure (that re-plumbing carries no new theorem); the closure's records_time_physical still names vnPointerOutcome, and this file supplies the record-layer realisation the closure's MD-1 docstring points at. The regions bornRegion ψ remain the corpus's preparation-indexed cells; the probabilities are the moment map (see MomentMapRace), and the statistics are LLN over the unknown microstate.

References

SigmaLayer/RecordedFact.lean (RecordSemantics, compatibleSet, P5/P6); LF4/BornRegionDisjoint.lean (bornRegion, bornRegion_pairwiseDisjoint, bornOutcome, bornOutcome_eq_some_iff); LF4/BornRegionUncond.lean (bornRegion_measurable_uncond, bornRegion_fs_measure_uncond); LF1/GeneralFrequency.lean (freq_tendsto_of_iid); SigmaLayer/FibreRecord.lean (the abstract-fibre version this migrates); SigmaLayer/FiniteQMClosure.lean (born_frequency, whose conclusion this matches).

def CSD.RecordLayer.projSignature (M : ℕ) : SigmaLayer.RecordSignature

The projective record signature (P5 data): a context is a nonzero preparation/measurement reference state ψ (fixing the born regions); outcomes are Fin (M+1).

Equations

• CSD.RecordLayer.projSignature M = { Context := { ψ : EuclideanSpace ℂ (Fin (M + 1)) // ψ ≠ 0 }, Outcome := fun (x : { ψ : EuclideanSpace ℂ (Fin (M + 1)) // ψ ≠ 0 }) => Fin (M + 1) }

noncomputable def CSD.RecordLayer.projRecordSemantics (M : ℕ) : SigmaLayer.RecordSemantics (LF4.CPN (M + 1)) (projSignature M)

The record semantics (P5) on the actual projective Σ = CPN (M+1). The ontic event of "context ψ recorded outcome i" is the corpus's own Born region bornRegion ψ i: measurable (bornRegion_measurable_uncond), and exclusive within a context — a microstate cannot lie in two Born cells (bornRegion_pairwiseDisjoint). The corpus's measurement readout as a first-class record.

Equations

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

@[simp]

theorem CSD.RecordLayer.projRecordSemantics_event {M : ℕ} (c : { ψ : EuclideanSpace ℂ (Fin (M + 1)) // ψ ≠ 0 }) (i : Fin (M + 1)) (t : SigmaLayer.OnticTime) : (projRecordSemantics M).event { context := c, outcome := i, time := t } = LF4.bornRegion ↑c ⋯ i

theorem CSD.RecordLayer.bornOutcome_eq_record {M : ℕ} (c : { ψ : EuclideanSpace ℂ (Fin (M + 1)) // ψ ≠ 0 }) (i : Fin (M + 1)) (t : SigmaLayer.OnticTime) (p : LF4.CPN (M + 1)) : LF4.bornOutcome ↑c ⋯ p = some i ↔ p ∈ (projRecordSemantics M).event { context := c, outcome := i, time := t }

The corpus's outcome map is the record. bornOutcome reads outcome i at a microstate exactly when the microstate lies in the record event ⟨c, i, t⟩.

theorem CSD.RecordLayer.compatibleSet_proj_single {M : ℕ} (c : { ψ : EuclideanSpace ℂ (Fin (M + 1)) // ψ ≠ 0 }) (i : Fin (M + 1)) (t : SigmaLayer.OnticTime) : SigmaLayer.compatibleSet (projRecordSemantics M) [{ context := c, outcome := i, time := t }] = LF4.bornRegion ↑c ⋯ i

Isolation on one record conditions the ontic state onto the Born region (P6).

theorem CSD.RecordLayer.fubiniStudy_projRecord {M : ℕ} (p₀ : LF4.CPN (M + 1)) (c : { ψ : EuclideanSpace ℂ (Fin (M + 1)) // ψ ≠ 0 }) (hψ : ‖↑c‖ = 1) (i : Fin (M + 1)) (t : SigmaLayer.OnticTime) : ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ((projRecordSemantics M).event { context := c, outcome := i, time := t })).toReal = ‖inner ℂ (EuclideanSpace.single i 1) ↑c‖ ^ 2

Born meets the record, on the real Σ. For a unit state the Fubini–Study typicality of the record event of outcome i is exactly ‖⟨eᵢ, ψ⟩‖² (bornRegion_fs_measure_uncond).

theorem CSD.RecordLayer.projRecord_frequency {M : ℕ} (p₀ : LF4.CPN (M + 1)) (c : { ψ : EuclideanSpace ℂ (Fin (M + 1)) // ψ ≠ 0 }) (hψ : ‖↑c‖ = 1) (i : Fin (M + 1)) (t : SigmaLayer.OnticTime) {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Ω → LF4.CPN (M + 1)) (hX : ∀ (k : ℕ), Measurable (X k)) (hlaw : ∀ (k : ℕ), MeasureTheory.Measure.map (X k) P = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g P) fun (k : ℕ) => (X k ⁻¹' (projRecordSemantics M).event { context := c, outcome := i, time := t }).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (N : ℕ) => (∑ k ∈ Finset.range N, (X k ⁻¹' (projRecordSemantics M).event { context := c, outcome := i, time := t }).indicator (fun (x : Ω) => 1) ω) / ↑N) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ↑c‖ ^ 2))

Born as the law of large numbers over the unknown microstate, on the actual projective Σ. For i.i.d. FS-typical microstates X k (law fubiniStudyMeasure p₀), the frequency of trials whose microstate lands in the record event of outcome i converges almost surely to ‖⟨eᵢ, ψ⟩‖² — the exact FiniteQMClosure.born_frequency conclusion, carried by the record-layer RecordSemantics. The whole probabilistic content is the strong law over the unknown initial condition.