SigmaLayer/PointerWeights: the selector-modulated weight field and the arena propagator (brick 2b)

Category: dynamical measurement — the smooth-Hamiltonian witness route (specs/pointer-witness-plan.md brick 2, weight-field half).

The weight of outcome j at the ontic point x = (p, θ, ·) is a circle-intrinsic trapezoid: with r = c.rate p the context rates at the base point (the ContextField / globalBasin discipline — no preparation anywhere), mⱼ the midpoint of the j-th CDF cell and rⱼ/2 its half-width,

pointerWeights c ε x j = clamp₀¹((rⱼ/2 − dist(θ₁, mⱼ))/ε).

Because the construction runs through dist on AddCircle and the (continuous) coercion ℝ → AddCircle — never through a fundamental-domain lift — joint continuity in the ontic point is a plain composition (continuous_pointerWeights), with no seam-gluing at the wrap point. The weight is 1 on the ε-shrunk cell arc (pointerWeights_eq_one), 0 off the open cell arc (pointerWeights_eq_zero), and in [0,1] always.

The arena propagator fires the brick-2a coupling with these weights:

pointerEvolve c ε (x, q) = (x, couplingUU (pointerWeights c ε x) • q).

Headlines:

• ★ continuous_pointerEvolve — the propagator is continuous on the whole arena: the theorem the piecewise witness provably cannot have (shearEvolve_not_continuous — a clopen-partition contradiction on the connected KSigma). Proof: descend through the open quotient map id × mk' (IsOpenQuotientMap.prodMap), where the lifted map is mk ∘ (matrix–vector application) of entrywise-continuous data (continuous_couplingU_entry composed with the weight field).
• pointerEvolve_measurePreserving — Liouville preservation on the arena, as a skew product (MeasurePreserving.skew_product): the sector coordinate is conserved and every pointer slice acts by an FS-preserving unitary.
• pointerEvolve_pure — on the ε-shrunk cell of outcome j (stated as the two distance hypotheses), the weights are the pure vector Pi.single j 1 and the propagator is exactly the brick-1 quarter rotation in plane j — the seed of the landing theorem.

⚠️ Honest scope. No record landing, Born accounting, or protocol packaging yet — that is bricks 3–4. The two distance hypotheses of pointerEvolve_pure (in the shrunk arc of cell j; outside every other open arc) are hypotheses here: the bridging geometry — shrunk arcs have those distance properties and carry volume ≥ rⱼ − 2ε, cells being the corpus's circleCell/torusCell — is brick 3's first job. Continuity statements require continuous context rates (hc); the witness instantiations (momentContext, basisContext) have them, but a bare ContextField promises only measurability.

⚠️ Boundary sharpened 2026-08-03 (fourth external review): substituting the selector-dependent weights w = w(x) while keeping the base fixed makes the arena map fibrewise-Hamiltonian only — the joint flow of the scalar 𝓗(x,q) = μ_{H_eff(w(x))}(q) would back-react on the register wherever the weights vary (ι_Vω ≠ d𝓗 on the ε-collars; full accounting in PointerGeneration.lean's honest-scope block). The weight functions here are Lipschitz (clampDiv/min/max), proved Continuous, not C¹ at the joins are now C^∞: the substitution landed 2026-08-04 (BACKLOG.md B1) — pointerWeights is built on smoothArcWeight (SigmaLayer/SmoothProfile.lean), the plateau interface is unchanged so every downstream proof transferred untouched, and contDiff_pointerWeights_lift is the new smoothness statement. clampDiv remains below as the construction record, no longer used by the witness.

References

specs/pointer-witness-plan.md (bricks 2b, 3); specs/BACKLOG.md (the ★ L row); specs/future-work.md. Reused corpus API: couplingUU/couplingU_single/ continuous_couplingU_entry (SigmaLayer/PointerCoupling.lean), ContextField/loSum (SigmaLayer/GlobalBasin.lean, BornFibrePartition.lean), Projectivization.isOpenQuotientMap_mk' + smul_mk_eq_mk_toEuclideanLin + toEuclideanLin_unitary_apply_ne_zero (projectivization staging), MeasurePreserving.skew_product (Mathlib).

The trapezoid clamp

noncomputable def CSD.RecordLayer.clampDiv (ε u : ℝ) : ℝ

The [0,1]-clamped ramp u ↦ clamp₀¹(u/ε): 1 for u ≥ ε, 0 for u ≤ 0, linear between. ⚠️ Superseded 2026-08-04: the witness no longer uses this — pointerWeights is built on smoothArcWeight, because this profile is not C¹ and so cannot carry a Poisson bracket. Kept as the construction record and because its plateau lemmas are the template the smooth profile matches statement-for-statement.

Equations

• CSD.RecordLayer.clampDiv ε u = max 0 (min 1 (u / ε))

theorem CSD.RecordLayer.clampDiv_nonneg (ε u : ℝ) : 0 ≤ clampDiv ε u

theorem CSD.RecordLayer.clampDiv_le_one (ε u : ℝ) : clampDiv ε u ≤ 1

theorem CSD.RecordLayer.clampDiv_eq_one {ε u : ℝ} (hε : 0 < ε) (hu : ε ≤ u) : clampDiv ε u = 1

theorem CSD.RecordLayer.clampDiv_eq_zero {ε u : ℝ} (hε : 0 < ε) (hu : u ≤ 0) : clampDiv ε u = 0

theorem CSD.RecordLayer.continuous_clampDiv (ε : ℝ) : Continuous (clampDiv ε)

The weight field

noncomputable def CSD.RecordLayer.cellMid {N : ℕ} (r : Fin N → ℝ) (j : Fin N) : CircleFibre

The midpoint of the j-th CDF cell at rate vector r, as a circle point.

Equations

• CSD.RecordLayer.cellMid r j = ↑(CSD.RecordLayer.loSum r j + r j / 2)

noncomputable def CSD.RecordLayer.pointerWeights {N : ℕ} (c : ContextField N) (ε : ℝ) (x : LF4.KSigma N) : Fin N → ℝ

The selector-modulated weight field: outcome j's weight at the ontic point x, a C^∞ corridor profile in the circle distance from the first fibre coordinate to the j-th cell midpoint, with rates read at the base point (context-fixed — no preparation).

★ Substituted onto the smooth profile 2026-08-04 (BACKLOG.md B1). This was clampDiv ε (…), a trapezoid: Lipschitz, but not C¹ at its joins. That is not a presentational defect — the Poisson bracket {wᵢ, wⱼ} on which the joint-arena Hamiltonian route turns is undefined on non-differentiable weights, so the trapezoid blocked the argument outright. smoothArcWeight has the identical plateau interface (same statements, same hypotheses: = 1 on the shrunk arc, = 0 off the open arc, values in [0,1]), so every downstream landing/Born/protocol proof is unaffected — see the four lemmas below, whose statements are unchanged. What is new is contDiff_pointerWeights_lift.

Equations

• CSD.RecordLayer.pointerWeights c ε x j = CSD.RecordLayer.smoothArcWeight ε (c.rate x.1 j) (CSD.RecordLayer.cellMid (c.rate x.1) j) x.2.1

theorem CSD.RecordLayer.pointerWeights_nonneg {N : ℕ} (c : ContextField N) (ε : ℝ) (x : LF4.KSigma N) (j : Fin N) : 0 ≤ pointerWeights c ε x j

theorem CSD.RecordLayer.pointerWeights_le_one {N : ℕ} (c : ContextField N) (ε : ℝ) (x : LF4.KSigma N) (j : Fin N) : pointerWeights c ε x j ≤ 1

theorem CSD.RecordLayer.pointerWeights_eq_one {N : ℕ} (c : ContextField N) {ε : ℝ} (hε : 0 < ε) {x : LF4.KSigma N} {j : Fin N} (hj : dist x.2.1 (cellMid (c.rate x.1) j) ≤ c.rate x.1 j / 2 - ε) : pointerWeights c ε x j = 1

In the ε-shrunk cell arc of outcome j, the weight is exactly 1.

theorem CSD.RecordLayer.pointerWeights_eq_zero {N : ℕ} (c : ContextField N) {ε : ℝ} (hε : 0 < ε) {x : LF4.KSigma N} {j : Fin N} (hj : c.rate x.1 j / 2 ≤ dist x.2.1 (cellMid (c.rate x.1) j)) : pointerWeights c ε x j = 0

Off the open cell arc of outcome j, the weight is exactly 0.

theorem CSD.RecordLayer.continuous_pointerWeights {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) : Continuous fun (x : LF4.KSigma N) => pointerWeights c ε x

Joint continuity of the weight field — circle-intrinsic, so a plain composition: no fundamental-domain lift, no seam. Requires continuous context rates.

theorem CSD.RecordLayer.pointerWeights_eq_single {N : ℕ} (c : ContextField N) {ε : ℝ} (hε : 0 < ε) {x : LF4.KSigma N} {j : Fin N} (hj : dist x.2.1 (cellMid (c.rate x.1) j) ≤ c.rate x.1 j / 2 - ε) (hk : ∀ (k : Fin N), k ≠ j → c.rate x.1 k / 2 ≤ dist x.2.1 (cellMid (c.rate x.1) k)) : pointerWeights c ε x = Pi.single j 1

On a point satisfying the shrunk-cell distance facts for outcome j, the weight vector is the pure vector of outcome j.

theorem CSD.RecordLayer.couplingUU_single {N : ℕ} (j : Fin N) : couplingUU (Pi.single j 1) = pointerRotU (Real.pi / 2) j

The pure-weight coupling propagator is the brick-1 quarter rotation, at the unitary-group level.

theorem CSD.RecordLayer.contDiff_pointerWeights_lift {N : ℕ} (c : ContextField N) {ε : ℝ} (hε : 0 < ε) (p : LF4.CPN N) {j : Fin N} (h2ε : 2 * ε < c.rate p j) (hr : c.rate p j < 1) {n : ℕ∞} (mid : ℝ) (hmid : ↑mid = cellMid (c.rate p) j) : ContDiff ℝ ↑n fun (s : ℝ) => smoothArcWeight ε (c.rate p j) (cellMid (c.rate p) j) ↑s

★ The weight field is C^∞ in the register coordinate — the property the joint-arena Hamiltonian route needs and the trapezoid could not supply. Stated on the universal cover at fixed rates, which is the strongest form available without a smooth structure on KSigma (§2a, MATHLIB-GAPS.md). Hypotheses are geometric, not technical debt: 2ε < r is the ε-Born sandwich's own nonvacuity condition, and r < 1 says there is more than one cell. With this, {wᵢ, wⱼ} is at last a well-formed expression on the corpus's weights — see specs/BACKLOG.md A2, which depends on exactly this.

The arena propagator

noncomputable def CSD.RecordLayer.pointerEvolve {N : ℕ} (c : ContextField N) (ε : ℝ) : PointerArena N N → PointerArena N N

The pointer-witness propagator at the measurement stroke: the ontic sector coordinate is conserved, and the pointer is rotated by the coupling at the selector-modulated weights.

Equations

• CSD.RecordLayer.pointerEvolve c ε y = (y.1, CSD.RecordLayer.couplingUU (CSD.RecordLayer.pointerWeights c ε y.1) • y.2)

theorem CSD.RecordLayer.pointerEvolve_fst {N : ℕ} (c : ContextField N) (ε : ℝ) (y : PointerArena N N) : (pointerEvolve c ε y).1 = y.1

The sector coordinate is conserved — records about the sector survive the stroke, and the base/selector marginals are untouched.

theorem CSD.RecordLayer.continuous_pointerEvolve_snd {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) : Continuous fun (y : PointerArena N N) => couplingUU (pointerWeights c ε y.1) • y.2

The pointer component of the propagator is continuous (the joint-continuity core).

theorem CSD.RecordLayer.continuous_pointerEvolve {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) : Continuous (pointerEvolve c ε)

★ The full arena propagator is continuous — the property shearEvolve_not_continuous proves no torus-register witness can have: the smooth horn's record transport has no seams.

theorem CSD.RecordLayer.pointerEvolve_measurePreserving {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) (p₀ : LF4.CPN N) (q₀ : Pointer N) : MeasureTheory.MeasurePreserving (pointerEvolve c ε) (pointerLiouville p₀ q₀) (pointerLiouville p₀ q₀)

Liouville preservation on the arena — a skew product: the sector coordinate is conserved, and every pointer slice acts by an FS-preserving unitary.

theorem CSD.RecordLayer.pointerEvolve_pure {N : ℕ} (c : ContextField N) {ε : ℝ} (hε : 0 < ε) {y : PointerArena N N} {j : Fin N} (hj : dist y.1.2.1 (cellMid (c.rate y.1.1) j) ≤ c.rate y.1.1 j / 2 - ε) (hk : ∀ (k : Fin N), k ≠ j → c.rate y.1.1 k / 2 ≤ dist y.1.2.1 (cellMid (c.rate y.1.1) k)) : pointerEvolve c ε y = (y.1, pointerRotU (Real.pi / 2) j • y.2)

On the shrunk cell of outcome j, the propagator is exactly the brick-1 quarter rotation in plane j — the seed of the landing theorem (brick 3 supplies the two distance facts from the cell geometry).