SigmaLayer/GlobalRecordClosure: the record-layer capstone, on the context-fixed basins

Category: 7-SigmaLayer (the record layer — MD-1, the closure).

The successor to SigmaLayer/RecordLayerClosure.lean. That bundle certifies the record layer on the fibre Σ = ℝ with fibreTypicality, for the context bornContext ψ — built from the preparation. This one certifies the same five facts on the corpus's actual compact sector Σ = ℂℙⁿ⁻¹ × T², for a ContextField — built from the apparatus alone.

What changes, and what does not

The five closure fields are the same five, and that is the point: nothing about the record layer's content depended on the preparation-indexing. What changes is the arena and the context type.

	RecordLayerClosure	GlobalRecordClosure
arena	ℝ (non-compact, odd-dim'l product)	KSigma = ℂℙⁿ⁻¹ × T² (compact, even)
context	bornContext ψ — the preparation	ContextField — the apparatus
measure	fibreTypicality (Lebesgue on [0,1))	epistemicMeasure p = δ_p ⊗ Haar
ae_total	on Ico 0 1 (⚠️ not forced — fibreTypicality_uncovered_univ)	on univ; mass one is Haar, not a restriction

★ The record event is now a function of (context, outcome, time) and of nothing else. That is visible in the type of globalRecordSemantics and needs no theorem to state: the same set globalBasin c i serves every preparation, and only the epistemic measure moves. Under fibreRecordSemantics the event itself was cdfCell (bornRate ψ), so it moved with ψ. This is the defect A7 objected to, and it is what the migration removes.

★ globalOutcome is literally circleOutcome read at the point's own base, so the ontic selection needs no new machinery — globalOutcome_eq_some_iff is circleOutcome_eq_some_iff composed with the definitional unfolding of globalBasin.

Scope — unchanged from GlobalBasin.lean, and repeated because this is the capstone

⚠️ epistemicMeasure p = δ_p ⊗ Haar is the epistemic measure, taken as a definition rather than obtained by disintegration (conditioning on p conditions on a μ_FS-null set). It is not the Liouville measure; kMuL = μ_FS ⊗ vol remains that.

⚠️ KINEMATIC. No H_int(M) generating these basins is constructed. The Paper D obligation (SigmaLayer/DeIsolationFlow.lean) is untouched, and a certified readout is not a dynamical account of measurement.

⚠️ This closes the preparation-indexing defect, not general-N A7 outright ANSWERED 2026-08-02 (author decision): the fibred reading of A7 is canonical, so with v0.7.0's dynamical layer this line of work discharges A7 at every N. The parked base-only chain is now the qubit-special-case question. See reconstruction-status.md §2.

⚠️ RecordLayerClosure is superseded, not deleted. It remains true, and FiniteQMClosure still carries the older vnPointerOutcome readout — swapping that is a separate migration on the productDynamics engine, and is not done here.

References

SigmaLayer/RecordLayerClosure.lean (the ℝ bundle this succeeds); SigmaLayer/GlobalBasin.lean (ContextField, globalBasin, epistemicMeasure, globalBasin_born); SigmaLayer/RecordedFact.lean (RecordSemantics, compatibleSet, and the warning that the structure is trivially inhabited — the non-vacuity here is ae_total and born_typicality); SigmaLayer/CircleRecord.lean (circleOutcome); specs/record-layer-plan.md §4 (MD-1); specs/BACKLOG.md (the ★★ row).

The record semantics on the compact sector

def CSD.RecordLayer.globalSignature (N : ℕ) : SigmaLayer.RecordSignature

The global record signature (P5 data): contexts are ContextFields — rate fields on the ontic base — and outcomes are Fin N. Contrast fibreSignature, whose contexts are bare rate vectors and so had to be manufactured from a preparation.

Equations

• CSD.RecordLayer.globalSignature N = { Context := CSD.RecordLayer.ContextField N, Outcome := fun (x : CSD.RecordLayer.ContextField N) => Fin N }

noncomputable def CSD.RecordLayer.globalRecordSemantics (N : ℕ) : SigmaLayer.RecordSemantics (LF4.KSigma N) (globalSignature N)

The global record semantics (P5) on Σ = ℂℙⁿ⁻¹ × T². The ontic event of "context c recorded outcome i" is the context-fixed basin globalBasin c i: measurable (measurableSet_globalBasin), and within one context at one time distinct outcomes are mutually exclusive (globalBasin_pairwiseDisjoint).

⚠️ RecordSemantics is trivially inhabited (RecordedFact.lean), so exhibiting this instance proves nothing on its own. The content is in globalRecordClosure's born_typicality and ae_total.

Equations

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

@[simp]

theorem CSD.RecordLayer.globalRecordSemantics_event {N : ℕ} (c : ContextField N) (i : Fin N) (t : SigmaLayer.OnticTime) : (globalRecordSemantics N).event { context := c, outcome := i, time := t } = globalBasin c i

theorem CSD.RecordLayer.compatibleSet_global_single {N : ℕ} (c : ContextField N) (i : Fin N) (t : SigmaLayer.OnticTime) : SigmaLayer.compatibleSet (globalRecordSemantics N) [{ context := c, outcome := i, time := t }] = globalBasin c i

The compatible region of the single-record history [⟨c, i, t⟩] is exactly the basin: isolation on this record conditions the ontic state onto the outcome basin (P6).

The ontic selection

noncomputable def CSD.RecordLayer.globalOutcome {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) : Option (Fin N)

The ontic selection on Σ: read which basin the point occupies. It is circleOutcome applied to the point's own fibre coordinate, with the rates the context assigns at the point's own base — so no new selection machinery is needed.

Equations

• CSD.RecordLayer.globalOutcome c x = CSD.RecordLayer.circleOutcome (c.rate x.1) x.2.1

theorem CSD.RecordLayer.globalOutcome_eq_some_iff {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) (i : Fin N) : globalOutcome c x = some i ↔ x ∈ globalBasin c i

Reading the outcome and testing the record event agree: the ontic selection is the record.

The closure bundle

structure CSD.RecordLayer.GlobalRecordClosure (N : ℕ) (c : ContextField N) (p : LF4.CPN N) : Prop

The global record-layer closure (MD-1). The five record-layer facts, certified on the corpus's compact sector for a context fixed by the apparatus and a preparation p.

Field-for-field the same bundle as RecordLayerClosure; what moved is the arena (ℝ → KSigma), the context type (bornContext ψ → ContextField), and the measure (fibreTypicality → epistemicMeasure p).

• exclusive (i j : Fin N) (t : SigmaLayer.OnticTime) (x : LF4.KSigma N) : x ∈ (globalRecordSemantics N).event { context := c, outcome := i, time := t } → x ∈ (globalRecordSemantics N).event { context := c, outcome := j, time := t } → i = j

  Within the context, distinct outcomes have mutually exclusive record events (P5).

• selection_is_record (i : Fin N) (t : SigmaLayer.OnticTime) (x : LF4.KSigma N) : globalOutcome c x = some i ↔ x ∈ (globalRecordSemantics N).event { context := c, outcome := i, time := t }

  The ontic selection globalOutcome is the record.

• isolation_is_conditioning (i : Fin N) (t : SigmaLayer.OnticTime) : SigmaLayer.compatibleSet (globalRecordSemantics N) [{ context := c, outcome := i, time := t }] = (globalRecordSemantics N).event { context := c, outcome := i, time := t }

  Isolation on one record conditions the ontic state onto the outcome basin (P6).

• born_typicality (i : Fin N) (t : SigmaLayer.OnticTime) : (epistemicMeasure p) ((globalRecordSemantics N).event { context := c, outcome := i, time := t }) = ENNReal.ofReal (c.rate p i)

  Born meets the record: the epistemic probability of the record event of outcome i is the rate the context assigns at p.

• ae_total (t : SigmaLayer.OnticTime) : (epistemicMeasure p) (Set.univ \ ⋃ (i : (globalSignature N).Outcome c), (globalRecordSemantics N).event { context := c, outcome := i, time := t }) = 0

  The record events cover Σ up to a null set. ★ On ℝ this was stated relative to Ico 0 1 — ⚠️ not because it had to be (fibreTypicality_uncovered_univ gives the univ form there too), but because the mass one was imposed by restricting Lebesgue. Here the whole space carries mass one intrinsically.

theorem CSD.RecordLayer.globalRecordClosure {N : ℕ} (c : ContextField N) (p : LF4.CPN N) : GlobalRecordClosure N c p

The global record-layer closure holds for every context and every preparation. Each field is discharged by its source lemma in GlobalBasin.lean.

The Born rule at the capstone

theorem CSD.RecordLayer.globalRecordClosure_born {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) (t : SigmaLayer.OnticTime) : (epistemicMeasure (Projectivization.mk ℂ ψ hψ0)) ((globalRecordSemantics N).event { context := momentContext N, outcome := i, time := t }) = ENNReal.ofReal (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2)

★★ The record-layer Born rule, from a context the preparation did not build.

For the canonical moment-map context, the epistemic probability of the record event of outcome i at preparation ψ is exactly ‖⟨eᵢ, ψ⟩‖². The record event globalBasin (momentContext N) i is the same set for every ψ; only the epistemic measure moves.

This is RecordLayerClosure.born_typicality's successor, with the preparation-indexing removed. ⚠️ Still kinematic: no H_int(M) produces these basins.