SigmaLayer/CircleFibre: the Born partition on a COMPACT fibre

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

Why this exists

The corpus had two record-layer constructions, and compactness and fibre-activity sat in different ones:

• KSigmaRecord.lean puts a P5 RecordSemantics on the compact KSigma = ℂℙⁿ⁻¹ × T² — but its events are π⁻¹' bornRegion ψ i, pulled back from the base. The torus fibre is inert, and the construction inherits the preparation-indexed base regions.
• FibredSigma.lean has an active fibre — it carries the CDF Born cells — but that fibre is ℝ with Lebesgue restricted to [0,1), which is not compact, so it cannot be a Paper C A1 ontic surface.

Since the general-N A7 work concluded that contextuality has to live in the fibre (specs/sigma-fibre-contextuality.md), the construction actually needed is active-fibre-on-compact-Σ, and neither module supplied it.

This file supplies the fibre half: the Born partition, on the circle.

What is proved

• circleCell — the Born cell as a subset of AddCircle 1, defined as the set of circle points whose canonical representative in (0,1] lies in the CDF interval. Defined as a preimage (not an image), so measurability is immediate.
• measurableSet_circleCell, volume_circleCell — each cell is measurable with volume (circleCell r i) = ENNReal.ofReal (r i): the same Born weights as the ℝ construction, now on a compact fibre carrying a probability measure.
• circleCell_pairwiseDisjoint — distinct outcomes remain mutually exclusive.
• volume_circleBornCell — fed the Born rates, the cell measure is ‖ψ i‖².
• circleFibre_isProbabilityMeasure, circleFibre_compactSpace — the fibre is compact and its Haar measure is a probability measure, which is what ℝ could not give.

Scope — what this does and does not settle

It gives a compact fibre carrying the active Born partition, which is the piece A1 was missing. It does not by itself make the fibred Σ a Paper C A1 ontic surface, and the fibre measure is not shown to be a Liouville measure, only exhibited as Haar. The remaining record-layer modules (FibreRecord, Measurement, RecordLayerClosure) still run on the ℝ fibre and would need re-plumbing onto this one; that is mechanical but not done here.

⚠️ A SINGLE CIRCLE CANNOT COMPLETE A1 — a dimension-parity fact, corrected 2026-07-30. An earlier version of this docstring said the missing Kähler structure was blocked on Mathlib's absent manifold exterior calculus. That was a misdiagnosis. ℂℙⁿ⁻¹ has real dimension 2n-2, so ℂℙⁿ⁻¹ × AddCircle 1 has real dimension 2n-1 — odd. A symplectic form needs ωᵏ as a volume form, so no odd-dimensional manifold carries one, hence none carries a Kähler structure. The A1 obstruction here is therefore not missing tooling: it would survive any amount of Mathlib API. (The same parity objection applies retroactively to FibredSigma's ℂℙⁿ⁻¹ × ℝ, also 2n-1.)

The fix is already in the corpus and is cheap. LF4/KahlerInstance.lean has KTorus = AddCircle 1 × AddCircle 1 and KSigma N = CPN N × KTorus, of real dimension 2n — even, and a product of Kähler manifolds. The intended successor construction puts this file's circleCell on the first torus coordinate, leaving the second as its symplectic partner. Every theorem below is stated about one AddCircle 1 and transports to that factor; what is missing is the product-measure step, not new fibre mathematics. See specs/BACKLOG.md (the ★★ row).

References

SigmaLayer/BornFibrePartition.lean (cdfCell, loSum, bornRate — the ℝ construction); SigmaLayer/FibredSigma.lean (the active-fibre Σ); SigmaLayer/KSigmaRecord.lean (the compact but inert-fibre Σ); LF4/KahlerInstance.lean (KTorus = AddCircle 1 × AddCircle 1); specs/sigma-fibre-contextuality.md; specs/BACKLOG.md (the ★★ fibre/A1 row).

The compact fibre

@[reducible, inline]

abbrev CSD.RecordLayer.CircleFibre : Type

The compact record fibre: the unit circle, the same factor the corpus's KTorus is built from. Replaces the non-compact ℝ of FibredSigma.

Equations

• CSD.RecordLayer.CircleFibre = AddCircle 1

instance CSD.RecordLayer.circleFibre_factPos : Fact (0 < 1)

instance CSD.RecordLayer.circleFibre_compactSpace : CompactSpace CircleFibre

theorem CSD.RecordLayer.circleFibre_volume_univ : MeasureTheory.volume Set.univ = 1

The fibre's Haar measure is a probability measure — the property the restricted Lebesgue measure on ℝ only had by fiat.

instance CSD.RecordLayer.circleFibre_isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

The Born partition, transported to the circle

noncomputable def CSD.RecordLayer.rep (x : CircleFibre) : ℝ

The canonical representative of a circle point in (0, 1].

Equations

• CSD.RecordLayer.rep x = ↑((AddCircle.equivIoc 1 0) x)

theorem CSD.RecordLayer.measurable_rep : Measurable rep

noncomputable def CSD.RecordLayer.circleCell {n : ℕ} (r : Fin n → ℝ) (i : Fin n) : Set CircleFibre

The Born cell on the circle: the points whose canonical representative lies in the CDF interval. A preimage, so measurability is immediate — unlike the image of cdfCell.

Equations

• CSD.RecordLayer.circleCell r i = CSD.RecordLayer.rep ⁻¹' Set.Ioc (CSD.RecordLayer.loSum r i) (CSD.RecordLayer.loSum r i + r i)

theorem CSD.RecordLayer.measurableSet_circleCell {n : ℕ} (r : Fin n → ℝ) (i : Fin n) : MeasurableSet (circleCell r i)

theorem CSD.RecordLayer.circleCell_pairwiseDisjoint {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) : Pairwise (Function.onFun Disjoint (circleCell r))

Distinct outcomes stay mutually exclusive on the circle. Inherited from the disjointness of the underlying CDF intervals, since each cell is the rep-preimage of its own interval.

The Born weights survive the transport

theorem CSD.RecordLayer.volume_circleCell {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) (hsum : ∀ (i : Fin n), loSum r i + r i ≤ 1) (i : Fin n) : MeasureTheory.volume (circleCell r i) = ENNReal.ofReal (r i)

The circle cell carries exactly the Born weight rᵢ. The whole point of the swap: moving to a compact fibre changes nothing about the outcome probabilities. Requires the rates to be a sub-probability vector, so the cells fit inside one turn of the circle.

theorem CSD.RecordLayer.volume_circleBornCell {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (i : Fin n) : MeasureTheory.volume (circleCell (bornRate ψ) i) = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)

Born rates on the compact fibre. For a unit state the circle cell for outcome i has measure ‖ψ i‖² — the same Born weight the ℝ fibre gave, now on a compact space with a genuine Haar probability measure.