SigmaLayer/TorusRecord: the record layer on the even-dimensional fibre

Category: 7-SigmaLayer (the record layer, A1 compactness and parity).

CircleFibre/CircleRecord moved the Born partition and then the record layer onto a compact fibre, which fixed the non-compactness of the original ℝ fibre. It did not fix parity: a single circle is one-dimensional, so ℂℙ^{N-1} × S¹ has odd real dimension and cannot carry a symplectic or Kähler structure at all. TorusFibre responded by putting the Born cells on T² = S¹ × S¹, constraining the first angle and leaving the second free, so that the total space KSigma = ℂℙ^{N-1} × T² is compact, even-dimensional, and a product of Kähler manifolds.

This file moves the rest of the record layer across, so that the active fibre and the A1-admissible arena are finally the same object:

• torusRecordSemantics — a postulate-P5 RecordSemantics on KTorus. The signature is fibreSignature, reused unchanged: it only ever mentioned rate vectors and outcome indices, never the fibre.
• compatibleSet_torus_single — isolation is conditioning (P6).
• torusOutcome_eq_record — the ontic selection is the record: reading which cell the microstate occupies and testing the record event are the same statement.
• TorusMeasurement / prob / torusBornMeasurement — measurement as context plus unknown microstate.
• ★ torusBornMeasurement_prob — the Born weight is ‖ψ i‖², the same number the ℝ and S¹ fibres gave. Moving to the even-dimensional fibre changes no probability.
• torusBornMeasurement_ae_total — the cells cover T² up to a null set.

Scope

What this delivers is an active record fibre on a compact, even-dimensional arena: the outcome is read off the fibre coordinate rather than pulled back from the base, and the arena's dimension no longer forbids the structure Paper C A1 asks for. It does not construct a Kähler form on that arena, and does not prove the fibre measure is a Liouville volume for one: Mathlib has no manifold differential-forms API, which is the standing KG-1 block. Parity is a necessary condition that was previously violated and now is not; it is not sufficiency, and no A1 discharge is claimed here.

References

SigmaLayer/TorusFibre.lean (the cells and the parity argument); SigmaLayer/CircleRecord.lean (the compact-fibre record layer this ports); SigmaLayer/Measurement.lean (P5/P6, bornContext); specs/BACKLOG.md (the A1 sector row); MATHLIB-GAPS.md (KG-1).

The P5 record semantics on the even-dimensional fibre

noncomputable def CSD.RecordLayer.torusRecordSemantics (n : ℕ) : SigmaLayer.RecordSemantics LF4.KTorus (fibreSignature n)

The torus record semantics (P5). The ontic event of "context c recorded outcome i" is the Born cell torusCell c.rate i: measurable, and within one context at one time distinct outcomes are mutually exclusive.

Equations

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

@[simp]

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

theorem CSD.RecordLayer.compatibleSet_torus_single {n : ℕ} (c : FibreContext n) (i : Fin n) (t : SigmaLayer.OnticTime) : SigmaLayer.compatibleSet (torusRecordSemantics n) [{ context := c, outcome := i, time := t }] = torusCell 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 cell.

The ontic selection is the record

noncomputable def CSD.RecordLayer.torusOutcome {n : ℕ} (r : Fin n → ℝ) (x : LF4.KTorus) : Option (Fin n)

The outcome the unknown microstate selects: the cell it occupies.

Equations

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

theorem CSD.RecordLayer.torusOutcome_eq_some_iff {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) (x : LF4.KTorus) (i : Fin n) : torusOutcome r x = some i ↔ x ∈ torusCell r i

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

theorem CSD.RecordLayer.torusOutcome_eq_record {n : ℕ} (c : FibreContext n) (i : Fin n) (t : SigmaLayer.OnticTime) (x : LF4.KTorus) : torusOutcome c.rate x = some i ↔ x ∈ (torusRecordSemantics n).event { context := c, outcome := i, time := t }

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

Measurement on the even-dimensional fibre

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

A measurement: a context awaiting an unknown microstate.

• context : FibreContext n

  The measurement context, which fixes the cells and the weights.

• time : SigmaLayer.OnticTime

  The ontic time at which the record is established.

def CSD.RecordLayer.TorusMeasurement.basin {n : ℕ} (m : TorusMeasurement n) (i : Fin n) : Set LF4.KTorus

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

Equations

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

noncomputable def CSD.RecordLayer.TorusMeasurement.prob {n : ℕ} (m : TorusMeasurement 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.TorusMeasurement.basin_eq {n : ℕ} (m : TorusMeasurement n) (i : Fin n) : m.basin i = torusCell m.context.rate i

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

The Born measurement on the even-dimensional fibre.

Equations

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

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

★ The Born rule on the even-dimensional fibre. The outcome-i probability is ‖ψ i‖², the same weight the ℝ and S¹ fibres gave: fixing the parity defect costs no probability.

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

A.e. every microstate yields a record. The cells cover T² up to a null set, so there is no positive-measure "no outcome" region.