SigmaLayer/SmoothProfile: the C^∞ transition profile and arc weight

Category: dynamical measurement — the low-level C^∞ primitives of the ε-corridor witness.

Extracted 2026-08-04 from PointerSmoothProfile.lean so that PointerWeights.lean can use them rather than merely cite them. That module sits above the pointer stack in the import graph (PointerWeights → … → PointerBorn → PointerGeneration → PointerSmoothProfile), so while the smooth profiles lived there the witness could not be built on them — and it was not: before this extraction grep found zero consumers of these definitions outside their own file. Two external reviews listed that as outstanding and it was twice recorded as "mechanical"; the extraction is what makes doing it possible.

Why it is load-bearing rather than cosmetic: the Poisson bracket {wᵢ, wⱼ} that the joint-arena Hamiltonian route turns on is undefined on the old trapezoid weights, because clampDiv = max 0 (min 1 (u/ε)) is Lipschitz but not C¹. Smooth weights are a prerequisite for that argument, not a presentational upgrade (specs/BACKLOG.md A2/B1).

Contents: smoothClampDiv (the Real.smoothTransition profile, same plateaus as clampDiv with the same hypotheses), smoothArcWeight (its circle-distance form), and ★ contDiff_smoothArcWeight_lift — the periodic lift is C^∞ on the universal cover, the circle-distance kinks at the cell centre and the cut locus both falling inside plateaus.

⚠️ Honest scope. Smoothness is of the periodic lift on ℝ, under 2ε < r and r < 1; manifold-level smoothness on KSigma remains the §2a-scoped A1/A3 boundary (MATHLIB-GAPS.md). The time ramp is deliberately not moved here: it is not a phase-space function, so it plays no part in the Poisson prerequisite, and substituting it would change the capstone's generation field to carry a rate factor — a separate decision, recorded in BACKLOG.md.

References

specs/BACKLOG.md (B1, and A2 which depends on it); SigmaLayer/PointerWeights.lean (the consumer); SigmaLayer/PointerSmoothProfile.lean (the time ramp and the global-time Schrödinger ODE, which stay there).

The smooth clamp

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

The smooth [0,1] transition profile u ↦ smoothTransition (u/ε): 0 for u ≤ 0, 1 for u ≥ ε, C^∞ everywhere — clampDiv with the corner-free profile.

Equations

• CSD.RecordLayer.smoothClampDiv ε u = (u / ε).smoothTransition

theorem CSD.RecordLayer.smoothClampDiv_nonneg (ε u : ℝ) : 0 ≤ smoothClampDiv ε u

theorem CSD.RecordLayer.smoothClampDiv_le_one (ε u : ℝ) : smoothClampDiv ε u ≤ 1

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

Same plateau as clampDiv_eq_one, same hypotheses.

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

Same plateau as clampDiv_eq_zero, same hypotheses.

theorem CSD.RecordLayer.contDiff_smoothClampDiv (ε : ℝ) {n : ℕ∞} : ContDiff ℝ (↑n) (smoothClampDiv ε)

The smooth clamp is C^∞ — what the trapezoid could not be at its joins.

The smooth arc weight and its lift

noncomputable def CSD.RecordLayer.smoothArcWeight (ε r : ℝ) (mid θ : CircleFibre) : ℝ

The smooth arc weight at cell radius r and midpoint mid: the smooth clamp of the signed depth into the cell. The smooth counterpart of pointerWeights' per-cell profile.

Equations

• CSD.RecordLayer.smoothArcWeight ε r mid θ = CSD.RecordLayer.smoothClampDiv ε (r / 2 - dist θ mid)

theorem CSD.RecordLayer.smoothArcWeight_nonneg (ε r : ℝ) (mid θ : CircleFibre) : 0 ≤ smoothArcWeight ε r mid θ

theorem CSD.RecordLayer.smoothArcWeight_le_one (ε r : ℝ) (mid θ : CircleFibre) : smoothArcWeight ε r mid θ ≤ 1

theorem CSD.RecordLayer.smoothArcWeight_eq_one {ε r : ℝ} (hε : 0 < ε) {mid θ : CircleFibre} (hθ : dist θ mid ≤ r / 2 - ε) : smoothArcWeight ε r mid θ = 1

In the ε-shrunk cell arc, the smooth weight is exactly 1 — the same plateau fact, with the same hypotheses, as pointerWeights_eq_one.

theorem CSD.RecordLayer.smoothArcWeight_eq_zero {ε r : ℝ} (hε : 0 < ε) {mid θ : CircleFibre} (hθ : r / 2 ≤ dist θ mid) : smoothArcWeight ε r mid θ = 0

Off the open cell arc, the smooth weight is exactly 0 — the same plateau fact, with the same hypotheses, as pointerWeights_eq_zero.

theorem CSD.RecordLayer.smoothArcWeight_lift_periodic (ε r mid : ℝ) : Function.Periodic (fun (s : ℝ) => smoothArcWeight ε r ↑mid ↑s) 1

The lift of the smooth arc weight to the universal cover is 1-periodic — the smoothness statement below is genuinely a statement about the circle function.

theorem CSD.RecordLayer.contDiff_smoothArcWeight_lift {ε r : ℝ} (hε : 0 < ε) (h2ε : 2 * ε < r) (hr : r < 1) (mid : ℝ) {n : ℕ∞} : ContDiff ℝ ↑n fun (s : ℝ) => smoothArcWeight ε r ↑mid ↑s

★ The smooth arc weight is C^∞ on the universal cover. The circle distance has kinks at the cell centre and at the cut locus, but both fall inside plateaus of the transition profile — near the centre the weight is identically 1 (ε < r/2), near the cut locus identically 0 (r < 1) — and a locally constant function is smooth no matter what it is composed with. In the transition zone d ∈ [r/2−ε, r/2] the distance lift is locally affine, so the composition is a smooth profile of an affine function.

The smooth time ramp

noncomputable def CSD.RecordLayer.smoothPointerRamp (t : ℝ) : ℝ

The smooth time ramp: 0 before the stroke, π/2 after, C^∞ throughout. Moved here 2026-08-04 (B1b) so that PointerProtocol.lean can be built on it.

Equations

• CSD.RecordLayer.smoothPointerRamp t = Real.pi / 2 * t.smoothTransition

theorem CSD.RecordLayer.smoothPointerRamp_of_nonpos {t : ℝ} (ht : t ≤ 0) : smoothPointerRamp t = 0

Before the stroke the smooth ramp is 0.

theorem CSD.RecordLayer.smoothPointerRamp_of_one_le {t : ℝ} (ht : 1 ≤ t) : smoothPointerRamp t = Real.pi / 2

After the stroke the smooth ramp is π/2, so freezing/persistence consume it unchanged.

theorem CSD.RecordLayer.contDiff_smoothPointerRamp {n : ℕ∞} : ContDiff ℝ (↑n) smoothPointerRamp

The smooth ramp is C^∞.