SigmaLayer/PointerArena: the compact Kähler pointer — arena, regions, ready state (brick 0)

Category: dynamical measurement — the smooth-Hamiltonian witness route (specs/pointer-witness-plan.md brick 0; the ★ L backlog item, route confirmed 2026-08-03).

The torus-flux correction (2026-08-02, SigmaLayer/PiecewiseHamiltonian.lean) showed the landed witnesses' register translations are symplectic but not globally Hamiltonian on T² (ι_Xω = a·dp closed-not-exact, ∮dp ≠ 0). The confirmed repair replaces the torus register with a projective pointer ℂℙ^K = ℙ(ℂ^{K+1}) — compact Kähler with H¹ = 0, where unitary one-parameter groups are globally Hamiltonian flows. This module is the kinematic floor of that witness:

• Pointer K — the pointer manifold ℂℙ^K; readyState = [f₀] and, for each outcome j : Fin K, recordState j = [f_{j+1}] (reusing vertexPoint/momentMap_vertex);
• recordRegion j = {q | 1/2 < m_{j+1}(q)} and readyRegion δ = {q | 1 − δ < m₀(q)} via the pointer moment map — open (so a continuous propagator can land in them stably), measurable, pairwise disjoint, each containing its vertex, each of positive Fubini–Study measure (fubiniStudyMeasure_pos_of_isOpen, full support);
• PointerArena N K = KSigma N × Pointer K with pointerLiouville = kMuL ⊗ μ_FS^{ptr}, a probability measure; the arena-level ready/record cylinders and their measures.

⚠️ Honest scope. Kinematics only: no propagator, no Hamiltonian, and no record is created here — that is bricks 1–4 of pointer-witness-plan.md. The 1/2 threshold makes disjointness a one-line simplex fact (two moment coordinates cannot both exceed 1/2); nothing downstream may read q ∈ recordRegion j as "the pointer IS [f_{j+1}]" — transition states (all moment coordinates ≤ 1/2) are legitimate pointer points lying outside every region by design, which is exactly the exceptional room no_everywhere_correlation (SigmaLayer/MeasurementConstraints.lean) forces every continuous exact-record dynamics to have. Contrast the piecewise horn: the openness of these regions is the property whose torus analogue (discrete register arcs) fed shearEvolve_not_continuous (SigmaLayer/ShearDiscontinuity.lean).

References

specs/pointer-witness-plan.md (the brick ladder and the trade-off table); specs/BACKLOG.md (the ★ L row); specs/future-work.md; second external review 2026-08-02 (steps 1–3). Reused corpus API: vertexPoint (SigmaLayer/SwapLuders.lean), momentMap_vertex (SigmaLayer/DegenerateLuders.lean), the momentMap simplex facts (LF4/MomentMap.lean), fubiniStudyMeasure_pos_of_isOpen (LF4/TypicalityForcing.lean), kMuL (LF4/KahlerInstance.lean).

@[reducible, inline]

abbrev CSD.RecordLayer.Pointer (K : ℕ) : Type

The pointer manifold ℂℙ^K = ℙ(ℂ^{K+1}): one ready direction f₀ and K record directions f₁, …, f_K. Compact Kähler with H¹ = 0 — the property that makes unitary one-parameter groups globally Hamiltonian, killing the torus-flux obstruction.

Equations

• CSD.RecordLayer.Pointer K = CSD.LF4.CPN (K + 1)

noncomputable def CSD.RecordLayer.readyState {K : ℕ} : Pointer K

The ready state: the vertex ray [f₀].

Equations

• CSD.RecordLayer.readyState = CSD.RecordLayer.vertexPoint 0

noncomputable def CSD.RecordLayer.recordState {K : ℕ} (j : Fin K) : Pointer K

The record state for outcome j: the vertex ray [f_{j+1}].

Equations

• CSD.RecordLayer.recordState j = CSD.RecordLayer.vertexPoint j.succ

theorem CSD.RecordLayer.momentMap_add_le_one {K : ℕ} (q : Pointer K) {i j : Fin (K + 1)} (hij : i ≠ j) : LF4.momentMap q i + LF4.momentMap q j ≤ 1

Two moment coordinates at distinct indices sum to at most 1 — the simplex fact behind every disjointness statement below.

Record regions

def CSD.RecordLayer.recordRegion {K : ℕ} (j : Fin K) : Set (Pointer K)

The record region for outcome j: pointer states whose f_{j+1} moment coordinate dominates, m_{j+1}(q) > 1/2. Open by design — a continuous propagator can land in it with a stable margin.

Equations

• CSD.RecordLayer.recordRegion j = {q : CSD.RecordLayer.Pointer K | 1 / 2 < CSD.LF4.momentMap q j.succ}

theorem CSD.RecordLayer.isOpen_recordRegion {K : ℕ} (j : Fin K) : IsOpen (recordRegion j)

theorem CSD.RecordLayer.measurableSet_recordRegion {K : ℕ} (j : Fin K) : MeasurableSet (recordRegion j)

theorem CSD.RecordLayer.recordRegion_pairwiseDisjoint {K : ℕ} : Pairwise (Function.onFun Disjoint recordRegion)

Distinct record regions are disjoint: two moment coordinates cannot both exceed 1/2.

theorem CSD.RecordLayer.recordState_mem_recordRegion {K : ℕ} (j : Fin K) : recordState j ∈ recordRegion j

The record state lies in its own record region.

theorem CSD.RecordLayer.recordRegion_pos {K : ℕ} (q₀ : Pointer K) (j : Fin K) : (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) (recordRegion j) ≠ 0

Every record region has positive Fubini–Study measure (openness + full support).

The ready region

def CSD.RecordLayer.readyRegion {K : ℕ} (δ : ℝ) : Set (Pointer K)

The ready region at margin δ: pointer states with m₀(q) > 1 − δ. A genuinely open neighbourhood of the ready state — the positive-measure ready region the landing theorem (brick 3) will start from.

Equations

• CSD.RecordLayer.readyRegion δ = {q : CSD.RecordLayer.Pointer K | 1 - δ < CSD.LF4.momentMap q 0}

theorem CSD.RecordLayer.isOpen_readyRegion {K : ℕ} (δ : ℝ) : IsOpen (readyRegion δ)

theorem CSD.RecordLayer.measurableSet_readyRegion {K : ℕ} (δ : ℝ) : MeasurableSet (readyRegion δ)

theorem CSD.RecordLayer.readyState_mem_readyRegion {K : ℕ} {δ : ℝ} (hδ : 0 < δ) : readyState ∈ readyRegion δ

theorem CSD.RecordLayer.readyRegion_pos {K : ℕ} (q₀ : Pointer K) {δ : ℝ} (hδ : 0 < δ) : (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) (readyRegion δ) ≠ 0

The ready region has positive Fubini–Study measure for every positive margin.

theorem CSD.RecordLayer.readyRegion_disjoint_recordRegion {K : ℕ} {δ : ℝ} (hδ : δ ≤ 1 / 2) (j : Fin K) : Disjoint (readyRegion δ) (recordRegion j)

With margin δ ≤ 1/2, the ready region is disjoint from every record region: being ready and carrying a record exclude each other.

The arena

@[reducible, inline]

abbrev CSD.RecordLayer.PointerArena (N K : ℕ) : Type

The pointer arena: the ontic sector Σ = ℂℙ^{N-1} × T² (base + selector fibre) times the pointer ℂℙ^K. A product of compact Kähler manifolds, real dimension 2(N−1) + 2 + 2K — even, with no odd factor for the parity check to catch.

Equations

• CSD.RecordLayer.PointerArena N K = (CSD.LF4.KSigma N × CSD.RecordLayer.Pointer K)

noncomputable def CSD.RecordLayer.pointerLiouville {K N : ℕ} (p₀ : LF4.CPN N) (q₀ : Pointer K) : MeasureTheory.Measure (PointerArena N K)

The arena Liouville measure μL = (μ_FS ⊗ vol_{T²}) ⊗ μ_FS^{ptr}.

Equations

• CSD.RecordLayer.pointerLiouville p₀ q₀ = (CSD.LF4.kMuL p₀).prod (Matrix.UnitaryGroup.fubiniStudyMeasure q₀)

instance CSD.RecordLayer.instIsProbabilityMeasurePointerArenaPointerLiouville {K N : ℕ} (p₀ : LF4.CPN N) (q₀ : Pointer K) : MeasureTheory.IsProbabilityMeasure (pointerLiouville p₀ q₀)

def CSD.RecordLayer.arenaReady {K : ℕ} (N : ℕ) (δ : ℝ) : Set (PointerArena N K)

The arena-level ready cylinder: pointer in the ready region, sector free.

Equations

• CSD.RecordLayer.arenaReady N δ = Set.univ ×ˢ CSD.RecordLayer.readyRegion δ

def CSD.RecordLayer.arenaRecord {K : ℕ} (N : ℕ) (j : Fin K) : Set (PointerArena N K)

The arena-level record cylinder for outcome j.

Equations

• CSD.RecordLayer.arenaRecord N j = Set.univ ×ˢ CSD.RecordLayer.recordRegion j

theorem CSD.RecordLayer.measurableSet_arenaReady {K N : ℕ} (δ : ℝ) : MeasurableSet (arenaReady N δ)

theorem CSD.RecordLayer.measurableSet_arenaRecord {K N : ℕ} (j : Fin K) : MeasurableSet (arenaRecord N j)

theorem CSD.RecordLayer.pointerLiouville_arenaReady {K N : ℕ} (p₀ : LF4.CPN N) (q₀ : Pointer K) (δ : ℝ) : (pointerLiouville p₀ q₀) (arenaReady N δ) = (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) (readyRegion δ)

The arena ready cylinder's Liouville measure is the pointer-side FS measure of the ready region (the sector factor integrates to 1).

theorem CSD.RecordLayer.arenaReady_pos {K N : ℕ} (p₀ : LF4.CPN N) (q₀ : Pointer K) {δ : ℝ} (hδ : 0 < δ) : (pointerLiouville p₀ q₀) (arenaReady N δ) ≠ 0

The apparatus-ready state has positive Liouville measure — the structural property the GlobalBasin arena provably lacks (globalBasin_ae_total: a.e. every point there already carries a record) and the reason the pointer factor exists at all.