SigmaLayer/FibreRecord: the record layer as a RecordSemantics instance (MD-1, step 3)

Category: 7-SigmaLayer (the record layer — the ontic record of the fibre outcome).

This wires the record-layer fibre partition into the corpus's postulate-P5 record infrastructure (SigmaLayer/RecordedFact.lean): the de-isolation outcome becomes a genuine RecordedFact, and its ontic event is the fibre cell cdfCell. This is step 3 of specs/record-layer-plan.md — the record half — and it makes the record-layer readout a first-class RecordSemantics, the intended replacement for the ad-hoc, preparation-indexed LF5/PointerOutcome.lean (vnPointerOutcome) readout.

Concretely, on the fibre Σ = ℝ:

• a context is a nonnegative rate vector FibreContext (the measurement M applied to the prepared state — the moment-map/Born rates over the outcomes);
• the record event of "context c recorded outcome i" is the CDF cell cdfCell c.rate i (fibreRecordSemantics), measurable, and exclusive within a context — distinct outcomes have disjoint cells (from cdfCell_pairwiseDisjoint);
• the ontic selection fibreOutcome records i at a fibre point exactly when the point lies in the record event (fibreOutcome_eq_some_iff) — the selection is the record;
• the compatible region of a single record is that cell (compatibleSet_fibre_single), so isolation on this record is conditioning on the outcome cell (the P6 story of RecordedFact.lean);
• Born meets the record: for the Born context, the fibre typicality of the record event is exactly ‖ψ i‖² (fibreTypicality_bornRecord) — the ontic typicality of recording outcome i is the Born weight.

The rate vector is part of the context and is only required to be nonnegative. Normalization and almost-sure record production are additional properties, proved for unit-state Born contexts. The time field is a label: these events do not change with time, and this file defines no register interaction. The preparation-independent context fields and their basins are in RecordLayer/GlobalBasin.lean; register-changing protocols are in RecordLayer/SwapWitness.lean.

References

specs/record-layer-plan.md (record layer, MD-1; step 3 = the record); SigmaLayer/RecordedFact.lean (RecordSignature, RecordSemantics, compatibleSet, postulates P5/P6); RecordLayer/DeIsolationFlow.lean (fibreTypicality, fibreTypicality_bornCell); RecordLayer/BornFibrePartition.lean (cdfCell, cdfCell_pairwiseDisjoint, fibreOutcome, bornRate); LF5/PointerOutcome.lean (vnPointerOutcome, the prep-indexed readout this replaces).

structure CSD.RecordLayer.FibreContext (n : ℕ) : Type

A measurement context on the fibre: a nonnegative rate vector over the n outcomes. In the Born constructor it is the context applied to a state. General contexts need not be normalized.

• rate : Fin n → ℝ

  Nonnegative outcome rates; no normalization or moment-map identity is assumed.

• rate_nonneg (i : Fin n) : 0 ≤ self.rate i

  The rates are nonnegative.

def CSD.RecordLayer.fibreSignature (n : ℕ) : SigmaLayer.RecordSignature

The fibre record signature (P5 data): contexts are rate vectors, outcomes are Fin n.

Equations

• CSD.RecordLayer.fibreSignature n = { Context := CSD.RecordLayer.FibreContext n, Outcome := fun (x : CSD.RecordLayer.FibreContext n) => Fin n }

noncomputable def CSD.RecordLayer.fibreRecordSemantics (n : ℕ) : SigmaLayer.RecordSemantics ℝ (fibreSignature n)

The fibre record semantics (P5) on Σ = ℝ. The ontic event of "context c recorded outcome i" is the CDF cell cdfCell c.rate i: measurable (measurableSet_cdfCell), and within one context at one time distinct outcomes are mutually exclusive — a fibre point cannot lie in two different outcome cells (from cdfCell_pairwiseDisjoint). This is the record-layer readout as a first-class RecordSemantics.

Equations

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

@[simp]

theorem CSD.RecordLayer.fibreRecordSemantics_event {n : ℕ} (c : FibreContext n) (i : Fin n) (t : SigmaLayer.OnticTime) : (fibreRecordSemantics n).event { context := c, outcome := i, time := t } = cdfCell c.rate i

theorem CSD.RecordLayer.compatibleSet_fibre_single {n : ℕ} (c : FibreContext n) (i : Fin n) (t : SigmaLayer.OnticTime) : SigmaLayer.compatibleSet (fibreRecordSemantics n) [{ context := c, outcome := i, time := t }] = cdfCell c.rate i

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

theorem CSD.RecordLayer.fibreOutcome_eq_record {n : ℕ} (c : FibreContext n) (i : Fin n) (t : SigmaLayer.OnticTime) (ξ : ℝ) : fibreOutcome c.rate ξ = some i ↔ ξ ∈ (fibreRecordSemantics n).event { context := c, outcome := i, time := t }

The ontic selection is the record. The outcome map records i at a fibre point exactly when that point lies in the record event ⟨c, i, t⟩ — reading the de-isolation outcome and testing membership in the record event agree.

noncomputable def CSD.RecordLayer.bornContext {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) : FibreContext n

The Born context of a state: the rate vector is the Born rates ‖ψ i‖².

Equations

• CSD.RecordLayer.bornContext ψ = { rate := CSD.RecordLayer.bornRate ψ, rate_nonneg := ⋯ }

@[simp]

theorem CSD.RecordLayer.bornContext_rate {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) : (bornContext ψ).rate = bornRate ψ

theorem CSD.RecordLayer.fibreTypicality_bornRecord {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (i : Fin n) (t : SigmaLayer.OnticTime) : fibreTypicality ((fibreRecordSemantics n).event { context := bornContext ψ, outcome := i, time := t }) = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)

Born meets the record. For the Born context the fibre-typicality measure of the record event of outcome i is exactly ‖ψ i‖² = |⟨eᵢ, ψ⟩|²: the ontic typicality of recording outcome i is the Born weight. This is the record-layer form of the Born rule — the outcome probability is the typicality of the ontic record event.