RecordLayer/Measurement: context, fibre outcome and recorded fact

Category: 7-SigmaLayer (measurement on the real fibre).

A Measurement pairs a nonnegative rate vector with a time label. Its disjoint CDF cells select an optional outcome from a real fibre point and package that outcome as a RecordedFact. The event semantics does not depend on the time label. Rates need not sum to one, so an arbitrary context can leave a set of positive fibreTypicality measure without a record.

• prob_eq_rate identifies basin probabilities with rates when the rates sum to one.
• ae_record_of_sum_eq_one proves almost-sure record production under that normalization.
• bornMeasurement_prob specializes the probability identity to a unit vector's squared component norms, and bornMeasurement_prob_momentMap identifies these with the moment map.
• bornMeasurement_frequency proves the frequency limit for measurable trials with the specified fibre law and pairwise independent outcome indicators.

The Born constructor supplies the rate vector from the state. Identifying it with the moment map does not by itself force an arbitrary context to have those rates; the separate generation hypothesis and theorem are in RecordLayer/CellLawForced.lean. Likewise, a deterministic selector does not establish independence between preparations: the frequency theorem takes that assumption explicitly.

This file packages a readout and its law. An interaction that changes an apparatus register is constructed separately in RecordLayer/SwapWitness.lean; sequential register laws are in RecordLayer/DrivenTwoTime.lean. The CDF packaging here does not prove those interaction laws.

References

RecordLayer/FibreRecord.lean (record semantics and Born context); RecordLayer/DeIsolationFlow.lean (restricted Lebesgue typicality); RecordLayer/MomentMapRace.lean (moment-map identification); LF1/GeneralFrequency.lean (strong law for the outcome indicators).

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

A measurement: a context (measurement type) awaiting an unknown microstate. The context fixes disjoint fibre cells and their probabilities; a microstate ξ selects an outcome when it lies in a cell, and that outcome is packaged as the record.

• context : FibreContext n

  The measurement context; fixes the disjoint cells and their probabilities.

• time : SigmaLayer.OnticTime

  The ontic time at which the record is established.

def CSD.RecordLayer.Measurement.basin {n : ℕ} (m : Measurement n) (i : Fin n) : Set ℝ

The basin of outcome i: the fibre region (record event) the context assigns to i. The basins are disjoint CDF cells. Normalized rates give full typicality coverage.

Equations

• m.basin i = (CSD.RecordLayer.fibreRecordSemantics n).event { context := m.context, outcome := i, time := m.time }

noncomputable def CSD.RecordLayer.Measurement.outcome {n : ℕ} (m : Measurement n) (ξ : ℝ) : Option (Fin n)

The outcome the unknown microstate ξ selects: the basin it occupies (none off the basins, which need not be a fibreTypicality-null set for an unnormalized context).

Equations

• m.outcome ξ = CSD.RecordLayer.fibreOutcome m.context.rate ξ

noncomputable def CSD.RecordLayer.Measurement.record {n : ℕ} (m : Measurement n) (ξ : ℝ) : Option (SigmaLayer.RecordedFact (fibreSignature n))

The record: the combined result the microstate ξ produces — the recorded fact ⟨context, outcome, time⟩, when the outcome is determined.

Equations

• m.record ξ = Option.map (fun (i : (CSD.RecordLayer.fibreSignature n).Outcome m.context) => { context := m.context, outcome := i, time := m.time }) (m.outcome ξ)

noncomputable def CSD.RecordLayer.Measurement.prob {n : ℕ} (m : Measurement n) (i : Fin n) : ENNReal

The probability of outcome i: the fibre typicality of its basin. The basins set the probabilities.

Equations

• m.prob i = CSD.RecordLayer.fibreTypicality (m.basin i)

theorem CSD.RecordLayer.Measurement.basin_eq {n : ℕ} (m : Measurement n) (i : Fin n) : m.basin i = cdfCell m.context.rate i

The basin is the context's CDF cell.

theorem CSD.RecordLayer.Measurement.outcome_eq_some_iff {n : ℕ} (m : Measurement n) (i : Fin n) (ξ : ℝ) : m.outcome ξ = some i ↔ ξ ∈ m.basin i

The microstate selects the basin it occupies: the outcome is i exactly when ξ lies in basin i.

theorem CSD.RecordLayer.Measurement.record_of_mem_basin {n : ℕ} (m : Measurement n) (i : Fin n) (ξ : ℝ) (h : ξ ∈ m.basin i) : m.record ξ = some { context := m.context, outcome := i, time := m.time }

The combined result is the record: a microstate in basin i produces the record ⟨context, i, time⟩.

theorem CSD.RecordLayer.Measurement.prob_eq_rate {n : ℕ} (m : Measurement n) (hsum : ∑ i : Fin n, m.context.rate i = 1) (i : Fin n) : m.prob i = ENNReal.ofReal (m.context.rate i)

For normalized context rates, each basin probability equals its rate.

theorem CSD.RecordLayer.Measurement.ae_record_of_sum_eq_one {n : ℕ} (m : Measurement n) (hsum : ∑ i : Fin n, m.context.rate i = 1) : ∀ᵐ (ξ : ℝ) ∂fibreTypicality, ∃ (i : (fibreSignature n).Outcome m.context), m.record ξ = some { context := m.context, outcome := i, time := m.time }

Normalized contexts produce a record almost surely under fibreTypicality. Nonnegativity alone, the requirement in FibreContext, does not imply this.

noncomputable def CSD.RecordLayer.Measurement.bornMeasurement {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (t : SigmaLayer.OnticTime) : Measurement n

The Born measurement of a state ψ: the context whose rates are the Born weights ‖ψ i‖² (= the Kähler moment map), established at time t.

Equations

• CSD.RecordLayer.Measurement.bornMeasurement ψ t = { context := CSD.RecordLayer.bornContext ψ, time := t }

theorem CSD.RecordLayer.Measurement.bornMeasurement_prob {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (i : Fin n) (t : SigmaLayer.OnticTime) : (bornMeasurement ψ t).prob i = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)

The basins set the probabilities = Born. For a unit state the probability of outcome i of the Born measurement is exactly ‖ψ i‖².

theorem CSD.RecordLayer.Measurement.bornMeasurement_prob_momentMap {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin n) (t : SigmaLayer.OnticTime) : (bornMeasurement ψ t).prob i = ENNReal.ofReal ((Projectivization.mk ℂ ψ hψ0).momentMap i)

The probability is the Kähler moment map. The Born measurement's outcome-i probability is the i-th torus moment-map coordinate at [ψ] — read off the context, not injected. That the moment map is the right rate field is pinned by torus generation (torusGenerated_eq_momentMap, RecordLayer/CellLawForced.lean): a context field whose rates generate the coordinate phase rotations is exactly the moment map. What remains posited is that the rates are generators (specs/POSITS.md Posit 1, restated).

theorem CSD.RecordLayer.Measurement.bornMeasurement_ae_total {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (t : SigmaLayer.OnticTime) : fibreTypicality (Set.Ico 0 1 \ ⋃ (i : Fin n), (bornMeasurement ψ t).basin i) = 0

The unknown microstate almost surely produces a record. For a unit state the Born measurement's basins cover the fibre up to a fibreTypicality-null set: a.e. microstate lands in some basin, so a.e. microstate yields a record.

theorem CSD.RecordLayer.Measurement.bornMeasurement_frequency {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (t : SigmaLayer.OnticTime) (i : Fin n) {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Ω → ℝ) (hX : ∀ (k : ℕ), Measurable (X k)) (hlaw : ∀ (k : ℕ), MeasureTheory.Measure.map (X k) P = fibreTypicality) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g P) fun (k : ℕ) => (X k ⁻¹' (bornMeasurement ψ t).basin i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (N : ℕ) => (∑ k ∈ Finset.range N, (X k ⁻¹' (bornMeasurement ψ t).basin i).indicator (fun (x : Ω) => 1) ω) / ↑N) Filter.atTop (nhds (‖ψ.ofLp i‖ ^ 2))

For measurable trials with law fibreTypicality and pairwise independent outcome-i indicators, the outcome-i frequency converges almost surely to the unit state's Born weight. The common law and indicator independence are hypotheses on the repeated preparations.