SigmaLayer/Measurement: the measurement architecture in one object (MD-1)

Category: 7-SigmaLayer (the record layer — the measurement as context + microstate → record).

The record-layer architecture assembled into a single object Measurement, exactly the intended shape:

• the context m.context is the measurement type — it fixes the basin partition of the fibre, and therefore the outcome probabilities (the moment-map/Born weights);
• the microstate ξ : ℝ is the unknown ontic fibre point (typical under fibreTypicality);
• the microstate selects an outcome m.outcome ξ — the basin it occupies (outcome_eq_some_iff);
• the basins set the probabilities: m.prob i = fibreTypicality (m.basin i), which for the Born measurement is ‖ψ i‖² = the Kähler moment map (bornMeasurement_prob, bornMeasurement_prob_momentMap);
• the combined result is the record m.record ξ = ⟨context, outcome, time⟩ (record_of_mem_basin).

So one microstate + one context deterministically yields one record. The probabilistic content is nothing special — it is the law of large numbers over the unknown initial microstate: each run is deterministic given its microstate, and across repeated preparations the microstate is typical (fibreTypicality), so the outcome-i frequency converges a.s. to the basin measure ‖ψ i‖² (bornMeasurement_frequency, via the strong law freq_tendsto_of_iid). Randomness = ignorance of the initial condition; Born = the LLN limit = the basin measure = the Kähler moment map.

Honest scope. Every fact here is grounded in the proven pieces (BornFibrePartition, DeIsolationFlow, FibreRecord, MomentMapRace, LF1/GeneralFrequency); the probabilities are the typicality of the basins, the basins carry the moment map, and the frequencies are the strong law — no injected probability vector and no extra dynamical postulate. The de-isolation flow is just the deterministic map from microstate to basin (which is what a measurement context is); there is no separate "derive the flow" problem, only the standard typicality+LLN story of Papers A/D. Foundational-triple, no sorry.

References

specs/record-layer-plan.md (record layer, MD-1); SigmaLayer/FibreRecord.lean (the P5 RecordSemantics, bornContext); SigmaLayer/MomentMapRace.lean (bornRate_eq_momentMap, the rates = the Kähler moment map); SigmaLayer/DeIsolationFlow.lean (fibreTypicality).

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

A measurement: a context (measurement type) awaiting an unknown microstate. The context fixes the fibre's basin partition (hence the outcome probabilities); a microstate ξ then selects the basin it occupies, and the combined result is the record.

• context : FibreContext n

  The measurement context — the measurement type; fixes the basins and the 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 the measurement type's partition of the fibre.

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, a fibreTypicality-null set).

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⟩.

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 (LF4.momentMap (Projectivization.mk ℂ ψ hψ0) 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 [ψ] — the probabilities are forced by the Kähler geometry, not injected.

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))

The Born rule as the law of large numbers over the unknown microstate. This is the whole probabilistic content, and it is nothing special: the microstate is unknown, each run is deterministic given it, and across repeated preparations the microstate is typical (fibreTypicality), so the outcome-i frequency converges almost surely to the basin measure ‖ψ i‖² — the Born weight. Randomness = ignorance of the initial condition; the limit is the strong law (freq_tendsto_of_iid).

For i.i.d. trials X k with law fibreTypicality, the frequency of trials whose microstate lands in basin i converges a.s. to ‖ψ i‖².