SigmaLayer/CircleRecord: the record layer, re-plumbed onto the compact fibre

Category: 7-SigmaLayer (the record layer — A1 compactness).

CircleFibre.lean moved the Born partition onto a compact fibre. This moves the rest of the record layer with it: the postulate-P5 record semantics, the isolation-is-conditioning reading, measurement-as-context + unknown microstate → record, the Born probabilities, and the almost-everywhere totality of the readout — all on CircleFibre = AddCircle 1 instead of ℝ.

The point is that nothing physical changes. The record signature is reused verbatim (fibreSignature: contexts are non-negative rate vectors, outcomes are Fin n) — it never mentioned the fibre — so only the semantics, the assignment of ontic events, is different. Every Born weight comes out identical (volume_circleCell), which is the content of the swap.

What this gives

• circleRecordSemantics — a postulate-P5 RecordSemantics on the compact CircleFibre: events are the circle Born arcs, measurable and mutually exclusive within a context.
• compatibleSet_circle_single — isolation is conditioning: the states compatible with one record are exactly that record's arc (the P6 reading).
• circleOutcome_eq_record — the ontic selection is the record: reading which arc the microstate occupies agrees with testing membership of the record event.
• CircleMeasurement / prob / circleBornMeasurement — measurement as context-plus-microstate, with circleBornMeasurement_prob : prob i = ‖ψ i‖².
• circleBornMeasurement_ae_total — the arcs cover the circle up to a null set, so a.e. microstate yields a record. On ℝ this was stated on [0,1); on the circle it is about the whole space. ⚠️ The ℝ restriction was not forced — see fibreTypicality_uncovered_univ. What compactness buys is stated precisely at circleBornMeasurement_ae_total.

What is still not claimed

Compactness and a genuine Haar probability measure, yes. A1 in full, no — and ⚠️ not for the reason an earlier version of this docstring gave. It said dω = 0 was blocked on Mathlib's absent manifold exterior calculus. The real obstruction is dimension parity: ℂℙⁿ⁻¹ × AddCircle 1 has real dimension 2n-1, which is odd, and no odd-dimensional manifold admits a symplectic — hence a Kähler — structure. More tooling would not fix it. The successor construction moves to KSigma = ℂℙⁿ⁻¹ × T² (real dimension 2n, even), putting the Born arcs on one torus coordinate; see CircleFibre.lean's scope note and the ★★ BACKLOG.md row. The fibre measure is also exhibited as Haar, not shown to be a Liouville measure.

⚠️ AND THIS IS A PARALLEL CONSTRUCTION, NOT A MIGRATION (corrected 2026-07-30). The commit that landed this file was headlined "the record layer now runs on the compact fibre", and the ★★ BACKLOG row recorded the re-plumbing as DONE. Both overstated it. What exists is a compact counterpart of the record semantics, proved in full. The corpus's actual capstones — Measurement.lean, RecordLayerClosure.lean, FiniteQMClosure.lean, KSigmaRecord.lean — still run on the ℝ fibre with fibreTypicality, and nothing outside AxiomAudit.lean imports this module. Retiring the ℝ closure is future work.

And this is the fibre half: the general-N A7 question of whether context-fixed regions exist at all is ⏸ parked, not settled (specs/sigma-fibre-contextuality.md).

References

SigmaLayer/CircleFibre.lean (the compact fibre and its Born arcs); SigmaLayer/FibreRecord.lean, SigmaLayer/Measurement.lean (the ℝ originals this mirrors); SigmaLayer/RecordedFact.lean (RecordSemantics, and the warning that it is trivially inhabited — the content is in the non-vacuity results, of which circleBornMeasurement_ae_total is one); specs/BACKLOG.md (the ★★ fibre/A1 row).

The P5 record semantics on the compact fibre

noncomputable def CSD.RecordLayer.circleRecordSemantics (n : ℕ) : SigmaLayer.RecordSemantics CircleFibre (fibreSignature n)

The circle record semantics (P5) on the compact Σ-fibre. The ontic event of "context c recorded outcome i" is the Born arc circleCell c.rate i — measurable, and within one context at one time distinct outcomes are mutually exclusive.

The signature is fibreSignature, reused unchanged: it only ever mentioned rate vectors and outcome indices, never the fibre. Swapping ℝ for the circle touches the semantics alone.

Equations

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

@[simp]

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

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

Isolation is conditioning (P6). The ontic states compatible with the single record "context c recorded i at t" are exactly that record's arc.

The ontic selection is the record

noncomputable def CSD.RecordLayer.circleOutcome {n : ℕ} (r : Fin n → ℝ) (x : CircleFibre) : Option (Fin n)

The outcome the unknown microstate selects on the circle: the arc it occupies.

Equations

• CSD.RecordLayer.circleOutcome r x = if h : ∃ (i : Fin n), x ∈ CSD.RecordLayer.circleCell r i then some h.choose else none

theorem CSD.RecordLayer.circleOutcome_eq_some_iff {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) (x : CircleFibre) (i : Fin n) : circleOutcome r x = some i ↔ x ∈ circleCell r i

Reading the outcome and testing the record event agree. For non-negative rates the arcs are disjoint, so "the microstate occupies arc i" and "the record says i" are the same statement.

theorem CSD.RecordLayer.circleOutcome_eq_record {n : ℕ} (c : FibreContext n) (i : Fin n) (t : SigmaLayer.OnticTime) (x : CircleFibre) : circleOutcome c.rate x = some i ↔ x ∈ (circleRecordSemantics n).event { context := c, outcome := i, time := t }

The ontic selection is the record, at the record-layer level.

Measurement on the compact fibre

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

A measurement on the compact fibre: a context awaiting an unknown microstate.

• context : FibreContext n

  The measurement context — fixes the arcs, hence the probabilities.

• time : SigmaLayer.OnticTime

  The ontic time at which the record is established.

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

The basin of outcome i: the arc the context assigns to it.

Equations

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

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

The probability of outcome i: the Haar measure of its basin.

Equations

• m.prob i = MeasureTheory.volume (m.basin i)

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

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

The Born measurement on the compact fibre for a prepared state ψ.

Equations

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

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

★ The Born rule on the compact fibre. The outcome-i probability of the Born measurement is ‖ψ i‖² — the same weight the ℝ fibre gave. Compactifying changed nothing.

theorem CSD.RecordLayer.circleBornMeasurement_ae_total {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (t : SigmaLayer.OnticTime) : MeasureTheory.volume (Set.univ \ ⋃ (i : Fin n), (circleBornMeasurement ψ t).basin i) = 0

A.e. every microstate yields a record. The arcs cover the circle up to a null set, so there is no positive-measure "no outcome" set.

On the comparison with ℝ — CORRECTED 2026-08-11. This module previously said the ℝ statement "had to be restricted to [0,1) by hand, because Lebesgue measure on the line is infinite". Both halves were wrong. fibreTypicality is not Lebesgue measure on the line but volume.restrict (Ico 0 1), a probability measure; and the restriction was not forced — fibreTypicality_uncovered_univ proves the identical univ-form statement on ℝ.

The real difference is not which sets the statement ranges over but where the mass one comes from. On ℝ it is imposed by fiat: fibreTypicality_Ici_one shows the fibre's complement, of infinite Lebesgue measure, is assigned typicality zero, so an uncovered point off [0,1) is excused by the measure rather than covered by a cell. Here mass one is Haar mass on a compact group (circleFibre_volume_univ), every nonempty open set has positive measure, and there is nowhere for an uncovered point to hide. That is the improvement — genuine, but a different one.