RecordLayer/HamiltonianShift: the shift the stroke Hamiltonian generates

Category: 7-SigmaLayer (dynamical measurement) — specs/BACKLOG.md §A; brick 3 of specs/frozen-base-obstruction-scoping.md, third step (chart-level generation of each component of the joint lift).

What this is

JointLift.lean took the torus shift Δ as a parameter and proved that every conserved-data shift is harmless to records, Born and Liouville measure. This module builds the shift the interaction Hamiltonian actually produces, and proves — at the chart level, on regular data — that it is what the stroke Hamiltonian generates in the conjugate directions.

The setting. Conserved data d = (m, θ₁, q) (ConservedData): context rates, register, pointer. The chart positions are x = (m, rep θ₁) ∈ ℝ^{N+1} (chartPos) and the momenta are their conjugates — the N moment-fibre phases and θ₂. The weights the stroke reads are W(x) = arcWeights ε x, and arcWeights_chartPos says they are exactly the arena's pointerWeights. The stroke Hamiltonian, for a fixed pointer q, is

𝓗_t(x, y) = ṫ(t) · (π/2) · E(W(x), q), E(w, q) = ⟨q, H(w) q⟩ / ‖q‖²

(strokeH, pointerEnergy): the ramped coupling energy whose Schrödinger flow drives the pointer (rampedU_schrodinger, coupling_hamiltonian_duality), now read as a function on the base chart through the weights. Hamilton's equations in the chart are

ẋ = ∂ᵧ𝓗 = 0, ẏᵢ = −∂ₓᵢ𝓗_t = −ṫ(t) (π/2) Σₖ Eₖ(q) ∂ᵢWₖ(x)

(dMom_strokeH, dPos_strokeH, hamiltonianField_strokeH): the positions — rates and register, everything the record reads — are frozen, and the back-reaction goes entirely into the momenta. This is the frozen-base obstruction dissolved rather than denied: the base moves, but along the moment fibre, where the record cannot see it.

Evaluating along the actual pointer trajectory q(s) = strokeTraj ε d s and integrating over the stroke gives the momentum shift

shiftReal ε d i = −Σₖ (∫₀¹ ṫ (π/2) Eₖ(q(s)) ds) · ∂ᵢWₖ(x₀)

and hamiltonianShift ε d is that shift read on the arena torus — the Δ fed to jointLift.

Results

• pointerEnergy, pointerEnergy_eq_sum, hasFDerivAt_pointerEnergy, continuous_pointerEnergy — the projective coupling energy: well defined on ℙ, linear in the weights with gradient energyGradient, continuous in the pointer.
• arcWeights, arcWeights_chartPos, contDiffAt_arcWeights — the chart weights agree with the arena weights and are C^∞ at every regular position (RegularPos: every rate in (2ε, 1), so both non-smooth points of the circle distance — the cell midpoint and its antipode — fall inside a plateau of the profile).
• OffCorridor, fderiv_arcWeights_eq_zero_of_offCorridor — where the register sits strictly inside a plateau of every cell, the weights are locally constant.
• strokeTraj, strokeTraj_one_eq_pointerEvolve, strokeEnergy, avgEnergy, shiftReal, hamiltonianShift, measurable_hamiltonianShift — the trajectory, the stroke energies along it, and the integrated shift; measurable in the conserved data.
• strokeCurve, strokeCurve_zero, strokeCurve_one_snd, hamiltonianShift_eq_strokeCurve_one — the chart curve with frozen positions and accumulating momenta; its endpoint is the shift.
• ★★ strokeCurve_hasDerivAt_hamiltonianField — on regular data the curve is an integral curve of the time-dependent stroke Hamiltonian evaluated on the pointer trajectory: γ̇(t) = X_{𝓗_t(q(t))}(γ(t)) for every t.
• ★★ isJointLift_hamiltonianShift, jointLift_hamiltonianShift_measurePreserving — the joint lift with the generated shift is a joint lift (so landing, the ε-Born sandwich, the outcome-sector identity and the moment-marginal law all hold for it) and preserves the arena Liouville measure.
• jointLift_eq_pointerEvolve_off_corridor — off the corridor the generated shift vanishes and the joint lift is the fibrewise witness, as SigmaLayer/UntriggeredFlow.lean predicts for the untriggered region.

What this does and does not settle

Chart level, regular data. Generation is proved in the Darboux chart of SigmaLayer/ChartBracket.lean, for a time-dependent Hamiltonian (so stated directly as HasDerivAt … (hamiltonianField (strokeH ε t …) …) rather than through the autonomous IsHamiltonianCurve), and only on regular data. The construction itself is total: at a non-regular position the weights need not be differentiable and fderiv is 0 there by Mathlib's convention, so hamiltonianShift is defined everywhere and measurable everywhere; the generation statement is claimed only where the weights are smooth.

Nonvanishing. That hamiltonianShift is actually non-zero — that the integrated energies against the weight derivatives produce phases differing on two coordinates supporting the state, which is what jointLift_base_moves_of_ne needs — is not claimed here. The computation is one about the coupling generators along the trajectory: in a collar where only one weight Wₖ varies the stroke Hamiltonian is ṫ(π/2) Wₖ hₖ, so Eₖ is conserved along the trajectory and vanishes on the ready pointer (hₖ is off-diagonal against e₀), while at a shared cell edge two weights vary at once and the energies are not conserved. This heuristic is paper-side and not formalised.

Arena level. Nothing here identifies jointLift c ε (hamiltonianShift ε) with the time-1 map of a Hamiltonian flow on the arena Kähler manifold — the chart→arena transport of the generation statement is what is missing (⚠️ RESIDUE(R-016)), now with the chart-level generation of the shift components in hand.

References

specs/frozen-base-obstruction-scoping.md (brick 3); specs/future-work.md; RecordLayer/JointLift.lean (jointLift, isJointLift_jointLift, jointLift_measurePreserving, jointLift_base_moves_of_ne); RecordLayer/JointFlowTransfer.lean (IsJointLift); RecordLayer/PointerGeneration.lean (rampedU_schrodinger, couplingUAt); RecordLayer/PointerHamiltonianField.lean (coupling_hamiltonian_duality, couplingEnergy); RecordLayer/SmoothProfile.lean (contDiff_smoothArcWeight_lift, of which contDiffAt_smoothArcWeight_lift₃ is the joint three-variable version); SigmaLayer/ChartBracket.lean (hamiltonianField, dPos, dMom); SigmaLayer/ChartIntegralCurve.lean (IsHamiltonianCurve, translationCurve_isHamiltonianCurve); SigmaLayer/UntriggeredFlow.lean.

The projective coupling energy

theorem CSD.RecordLayer.couplingEnergy_smul {K : ℕ} (w : Fin K → ℝ) (a : ℂ) (v : EuclideanSpace ℂ (Fin (K + 1))) : couplingEnergy w (a • v) = ‖a‖ ^ 2 * couplingEnergy w v

The coupling energy scales quadratically under complex rescaling of the state.

noncomputable def CSD.RecordLayer.pointerEnergy {K : ℕ} (w : Fin K → ℝ) (q : Pointer K) : ℝ

The projective coupling energy E_w([v]) = couplingEnergy w v / ‖v‖²: the A4 energy observable of the fixed-weight coupling, read on the pointer's projective space (the normalised expectation ½⟨ψ, H(w)ψ⟩/‖ψ‖²). Well defined on the projective point by couplingEnergy_smul; see pointerEnergy_mk.

Equations

• CSD.RecordLayer.pointerEnergy w q = CSD.RecordLayer.couplingEnergy w (Projectivization.rep q) / ‖Projectivization.rep q‖ ^ 2

theorem CSD.RecordLayer.pointerEnergy_mk {K : ℕ} (w : Fin K → ℝ) (v : EuclideanSpace ℂ (Fin (K + 1))) (hv : v ≠ 0) : pointerEnergy w (Projectivization.mk ℂ v hv) = couplingEnergy w v / ‖v‖ ^ 2

The projective energy at a representative.

theorem CSD.RecordLayer.couplingCLM_apply_eq_sum {K : ℕ} (w : Fin K → ℝ) (v : EuclideanSpace ℂ (Fin (K + 1))) : (couplingCLM w) v = ∑ k : Fin K, ↑(w k) • (couplingCLM (Pi.single k 1)) v

The coupling operator is linear in the weights: H(w) = Σₖ wₖ H(eₖ) on every vector.

theorem CSD.RecordLayer.couplingEnergy_eq_sum {K : ℕ} (w : Fin K → ℝ) (v : EuclideanSpace ℂ (Fin (K + 1))) : couplingEnergy w v = ∑ k : Fin K, w k * couplingEnergy (Pi.single k 1) v

The coupling energy is linear in the weights.

@[reducible, inline]

noncomputable abbrev CSD.RecordLayer.outcomeEnergy {K : ℕ} (k : Fin K) (q : Pointer K) : ℝ

The outcome energy Eₖ(q): the projective energy of the pure plane swap hₖ, the k-th coefficient of the projective coupling energy in the weights.

Equations

• CSD.RecordLayer.outcomeEnergy k q = CSD.RecordLayer.pointerEnergy (Pi.single k 1) q

theorem CSD.RecordLayer.pointerEnergy_eq_sum {K : ℕ} (w : Fin K → ℝ) (q : Pointer K) : pointerEnergy w q = ∑ k : Fin K, w k * outcomeEnergy k q

The projective coupling energy is linear in the weights: E_w(q) = Σₖ wₖ Eₖ(q).

noncomputable def CSD.RecordLayer.energyGradient {K : ℕ} (q : Pointer K) : (Fin K → ℝ) →L[ℝ] ℝ

The weight-gradient of the projective coupling energy at a fixed pointer state.

Equations

• CSD.RecordLayer.energyGradient q = ∑ k : Fin K, CSD.RecordLayer.outcomeEnergy k q • ContinuousLinearMap.proj k

@[simp]

theorem CSD.RecordLayer.energyGradient_apply {K : ℕ} (q : Pointer K) (u : Fin K → ℝ) : (energyGradient q) u = ∑ k : Fin K, outcomeEnergy k q * u k

theorem CSD.RecordLayer.hasFDerivAt_pointerEnergy {K : ℕ} (q : Pointer K) (w : Fin K → ℝ) : HasFDerivAt (fun (w : Fin K → ℝ) => pointerEnergy w q) (energyGradient q) w

The projective coupling energy is differentiable in the weights, with derivative energyGradient q.

theorem CSD.RecordLayer.continuous_pointerEnergy {K : ℕ} (w : Fin K → ℝ) : Continuous (pointerEnergy w)

The projective coupling energy is continuous on the pointer (descent through mk').

The weights on the joint chart

noncomputable def CSD.RecordLayer.cellMidLift {N : ℕ} (r : Fin N → ℝ) (k : Fin N) : ℝ

The real lift of the cell midpoint loSum r k + r k / 2 (so cellMid r k = ↑(cellMidLift r k)).

Equations

• CSD.RecordLayer.cellMidLift r k = CSD.RecordLayer.loSum r k + r k / 2

theorem CSD.RecordLayer.cellMid_eq_coe {N : ℕ} (r : Fin N → ℝ) (k : Fin N) : cellMid r k = ↑(cellMidLift r k)

noncomputable def CSD.RecordLayer.arcWeights {N : ℕ} (ε : ℝ) (x : Fin (N + 1) → ℝ) : Fin N → ℝ

The weight field on the joint chart. Positions x : Fin (N+1) → ℝ carry the N context rates x (castSucc k) = mₖ and the register lift x (last N) = θ₁; the weights are the smooth arc profiles read in these coordinates. On the arena this is pointerWeights (arcWeights_chartPos).

Equations

• CSD.RecordLayer.arcWeights ε x k = CSD.RecordLayer.smoothArcWeight ε (x k.castSucc) (CSD.RecordLayer.cellMid (Fin.init x) k) ↑(x (Fin.last N))

noncomputable def CSD.RecordLayer.chartPos {N : ℕ} (d : ConservedData N) : Fin (N + 1) → ℝ

The chart position of conserved data (m, θ₁, q): the rates, then the canonical lift of the register.

Equations

• CSD.RecordLayer.chartPos d = Fin.snoc d.1 (CSD.RecordLayer.rep d.2.1)

@[simp]

theorem CSD.RecordLayer.chartPos_castSucc {N : ℕ} (d : ConservedData N) (k : Fin N) : chartPos d k.castSucc = d.1 k

@[simp]

theorem CSD.RecordLayer.chartPos_last {N : ℕ} (d : ConservedData N) : chartPos d (Fin.last N) = rep d.2.1

theorem CSD.RecordLayer.init_chartPos {N : ℕ} (d : ConservedData N) : Fin.init (chartPos d) = d.1

theorem CSD.RecordLayer.measurable_chartPos {N : ℕ} : Measurable chartPos

noncomputable def CSD.RecordLayer.dataWeights {N : ℕ} (ε : ℝ) (d : ConservedData N) : Fin N → ℝ

The arena weights of conserved data, in arena form (continuous in the data).

Equations

• CSD.RecordLayer.dataWeights ε d k = CSD.RecordLayer.smoothArcWeight ε (d.1 k) (CSD.RecordLayer.cellMid d.1 k) d.2.1

theorem CSD.RecordLayer.dataWeights_conservedData {N : ℕ} (c : ContextField N) (ε : ℝ) (y : PointerArena N N) : dataWeights ε (conservedData c y) = pointerWeights c ε y.1

theorem CSD.RecordLayer.arcWeights_chartPos {N : ℕ} (ε : ℝ) (d : ConservedData N) : arcWeights ε (chartPos d) = dataWeights ε d

The chart weights at the chart position of conserved data are the arena weights.

theorem CSD.RecordLayer.continuous_dataWeights {N : ℕ} (ε : ℝ) : Continuous (dataWeights ε)

Joint smoothness of the arc weight in (rate, midpoint, register)

theorem CSD.RecordLayer.contDiffAt_smoothArcWeight_lift₃ {ε : ℝ} (hε : 0 < ε) {z₀ : ℝ × ℝ × ℝ} (h2ε : 2 * ε < z₀.1) (hr : z₀.1 < 1) {n : ℕ∞} : ContDiffAt ℝ (↑n) (fun (z : ℝ × ℝ × ℝ) => smoothArcWeight ε z.1 ↑z.2.1 ↑z.2.2) z₀

★ The smooth arc weight is C^∞ jointly in the rate, the midpoint lift and the register lift, at every point with 2ε < r < 1. The three-variable form of contDiff_smoothArcWeight_lift: the circle distance is kinked only at the centre and the cut locus, and both kinks fall inside plateaus of the profile (ε < r/2, r < 1); in the transition zone the distance lift is locally the absolute value of an affine function that does not vanish.

def CSD.RecordLayer.RegularPos {N : ℕ} (ε : ℝ) (x : Fin (N + 1) → ℝ) : Prop

Regular chart positions: every rate strictly inside (2ε, 1).

Equations

• CSD.RecordLayer.RegularPos ε x = ∀ (k : Fin N), 2 * ε < x k.castSucc ∧ x k.castSucc < 1

theorem CSD.RecordLayer.contDiffAt_arcWeights {N : ℕ} {ε : ℝ} (hε : 0 < ε) {x₀ : Fin (N + 1) → ℝ} (hreg : RegularPos ε x₀) {n : ℕ∞} : ContDiffAt ℝ (↑n) (arcWeights ε) x₀

★ The chart weight field is C^∞ at every regular position — jointly in all the rates and the register. This is what makes the base derivative ∂_m 𝓗 of the stroke Hamiltonian meaningful on the joint chart, not only its register derivative.

def CSD.RecordLayer.OffCorridor {N : ℕ} (ε : ℝ) (d : ConservedData N) : Prop

Off-corridor data: the register sits strictly inside a plateau of every weight — in the centre plateau (dist < m/2 − ε) or the outer plateau (m/2 < dist) of each cell.

Equations

• CSD.RecordLayer.OffCorridor ε d = ∀ (k : Fin N), dist d.2.1 (CSD.RecordLayer.cellMid d.1 k) < d.1 k / 2 - ε ∨ d.1 k / 2 < dist d.2.1 (CSD.RecordLayer.cellMid d.1 k)

theorem CSD.RecordLayer.arcWeights_eventuallyEq_const_of_offCorridor {N : ℕ} {ε : ℝ} (hε : 0 < ε) {d : ConservedData N} (hd : OffCorridor ε d) : arcWeights ε =ᶠ[nhds (chartPos d)] fun (x : Fin (N + 1) → ℝ) => arcWeights ε (chartPos d)

Off the corridor the chart weight field is locally constant around the chart position.

theorem CSD.RecordLayer.fderiv_arcWeights_eq_zero_of_offCorridor {N : ℕ} {ε : ℝ} (hε : 0 < ε) {d : ConservedData N} (hd : OffCorridor ε d) : fderiv ℝ (arcWeights ε) (chartPos d) = 0

Off the corridor the weight field has zero derivative at the chart position.

The pointer trajectory and the energies along it

noncomputable def CSD.RecordLayer.strokeTraj {N : ℕ} (ε : ℝ) (d : ConservedData N) (s : ℝ) : Pointer N

The pointer trajectory of conserved data under the ramped stroke: q(s) = U(r(s), w) • q with w the arena weights of the data.

Equations

• CSD.RecordLayer.strokeTraj ε d s = CSD.RecordLayer.couplingUUAt (CSD.RecordLayer.pointerRamp s) (CSD.RecordLayer.dataWeights ε d) • d.2.2

theorem CSD.RecordLayer.strokeTraj_zero {N : ℕ} (ε : ℝ) (d : ConservedData N) : strokeTraj ε d 0 = d.2.2

theorem CSD.RecordLayer.strokeTraj_one {N : ℕ} (ε : ℝ) (d : ConservedData N) : strokeTraj ε d 1 = couplingUU (dataWeights ε d) • d.2.2

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

At the end of the stroke the trajectory is the pointer of the fibrewise witness — and hence of every joint lift (IsJointLift.pointer_eq).

theorem CSD.RecordLayer.continuous_strokeTraj {N : ℕ} (ε : ℝ) : Continuous fun (p : ℝ × ConservedData N) => strokeTraj ε p.2 p.1

noncomputable def CSD.RecordLayer.strokeEnergy {N : ℕ} (ε : ℝ) (d : ConservedData N) (k : Fin N) (s : ℝ) : ℝ

The stroke energy of outcome k along the trajectory, ṫ(s) · (π/2) · Eₖ(q(s)): the k-th weight-coefficient of the time-dependent stroke Hamiltonian, evaluated on the moving pointer.

Equations

• CSD.RecordLayer.strokeEnergy ε d k s = deriv Real.smoothTransition s * (Real.pi / 2 * CSD.RecordLayer.outcomeEnergy k (CSD.RecordLayer.strokeTraj ε d s))

theorem CSD.RecordLayer.continuous_strokeEnergy {N : ℕ} (ε : ℝ) (k : Fin N) : Continuous fun (p : ℝ × ConservedData N) => strokeEnergy ε p.2 k p.1

noncomputable def CSD.RecordLayer.avgEnergy {N : ℕ} (ε : ℝ) (d : ConservedData N) (k : Fin N) : ℝ

The stroke-averaged outcome energy ∫₀¹ ṫ(s) (π/2) Eₖ(q(s)) ds.

Equations

• CSD.RecordLayer.avgEnergy ε d k = ∫ (s : ℝ) in 0..1, CSD.RecordLayer.strokeEnergy ε d k s

theorem CSD.RecordLayer.continuous_avgEnergy {N : ℕ} (ε : ℝ) (k : Fin N) : Continuous fun (d : ConservedData N) => avgEnergy ε d k

The Hamiltonian shift

noncomputable def CSD.RecordLayer.shiftReal {N : ℕ} (ε : ℝ) (d : ConservedData N) (i : Fin (N + 1)) : ℝ

The real shift in chart direction i: −Σₖ (∫₀¹ ṫ (π/2) Eₖ(q(s)) ds) · ∂ᵢWₖ(x₀) — the total impulse −∫₀¹ ∂ₓᵢ𝓗_s ds the stroke Hamiltonian delivers to the conjugate momentum yᵢ, computed along the pointer trajectory at the frozen chart position x₀ = chartPos d.

Equations

• CSD.RecordLayer.shiftReal ε d i = -∑ k : Fin N, CSD.RecordLayer.avgEnergy ε d k * (fderiv ℝ (CSD.RecordLayer.arcWeights ε) (CSD.RecordLayer.chartPos d)) (Pi.single i 1) k

noncomputable def CSD.RecordLayer.hamiltonianShift {N : ℕ} (ε : ℝ) (d : ConservedData N) : ArenaTorus N

The Hamiltonian shift: the real shifts of the N rate-conjugate angles and of the register-conjugate θ₂, read on the arena torus. This is the Δ fed to jointLift.

Equations

• CSD.RecordLayer.hamiltonianShift ε d = (fun (j : Fin N) => ↑(CSD.RecordLayer.shiftReal ε d j.castSucc), ↑(CSD.RecordLayer.shiftReal ε d (Fin.last N)))

theorem CSD.RecordLayer.measurable_shiftReal {N : ℕ} (ε : ℝ) (i : Fin (N + 1)) : Measurable fun (d : ConservedData N) => shiftReal ε d i

theorem CSD.RecordLayer.measurable_hamiltonianShift {N : ℕ} (ε : ℝ) : Measurable (hamiltonianShift ε)

The Hamiltonian shift is measurable — the hypothesis jointLift_measurePreserving needs. The averaged energies are continuous in the data; the weight derivative is measurable (measurable_fderiv_apply_const) though not continuous.

theorem CSD.RecordLayer.shiftReal_eq_zero_of_offCorridor {N : ℕ} (ε : ℝ) (hε : 0 < ε) {d : ConservedData N} (hd : OffCorridor ε d) (i : Fin (N + 1)) : shiftReal ε d i = 0

Off the corridor the shift vanishes: the weights are locally constant there.

theorem CSD.RecordLayer.hamiltonianShift_eq_zero_of_offCorridor {N : ℕ} (ε : ℝ) (hε : 0 < ε) {d : ConservedData N} (hd : OffCorridor ε d) : hamiltonianShift ε d = 0

The stroke Hamiltonian on the chart

noncomputable def CSD.RecordLayer.strokeH {N : ℕ} (ε t : ℝ) (q : Pointer N) (z : SigmaLayer.Chart (N + 1)) : ℝ

The time-dependent stroke Hamiltonian on the chart, for a fixed pointer q: 𝓗_t(x, y) = ṫ(t) · (π/2) · E(W(x), q) — the ramped coupling energy of the pointer, with the weights read off the chart positions x (the N rates and the register; the momenta y are their conjugates). It depends on the positions only, so the positions are frozen along its flow and the momenta absorb −∫ ∂ₓ𝓗.

Equations

• CSD.RecordLayer.strokeH ε t q z = deriv Real.smoothTransition t * (Real.pi / 2 * CSD.RecordLayer.pointerEnergy (CSD.RecordLayer.arcWeights ε z.1) q)

theorem CSD.RecordLayer.hasFDerivAt_strokeH {N : ℕ} (ε t : ℝ) (q : Pointer N) {z : SigmaLayer.Chart (N + 1)} {W' : (Fin (N + 1) → ℝ) →L[ℝ] Fin N → ℝ} (hW' : HasFDerivAt (arcWeights ε) W' z.1) : HasFDerivAt (strokeH ε t q) ((deriv Real.smoothTransition t * (Real.pi / 2)) • energyGradient q ∘SL W' ∘SL ContinuousLinearMap.fst ℝ (Fin (N + 1) → ℝ) (Fin (N + 1) → ℝ)) z

Chain rule: wherever the chart weights are differentiable, so is the stroke Hamiltonian, with derivative the weight-gradient of the energy pulled back through W'.

theorem CSD.RecordLayer.dPos_strokeH {N : ℕ} (ε t : ℝ) (q : Pointer N) {z : SigmaLayer.Chart (N + 1)} {W' : (Fin (N + 1) → ℝ) →L[ℝ] Fin N → ℝ} (hW' : HasFDerivAt (arcWeights ε) W' z.1) (i : Fin (N + 1)) : SigmaLayer.dPos (strokeH ε t q) z i = deriv Real.smoothTransition t * (Real.pi / 2) * ∑ k : Fin N, outcomeEnergy k q * W' (Pi.single i 1) k

∂ₓᵢ𝓗_t = ṫ (π/2) Σₖ Eₖ(q) ∂ᵢWₖ.

theorem CSD.RecordLayer.dMom_strokeH {N : ℕ} (ε t : ℝ) (q : Pointer N) {z : SigmaLayer.Chart (N + 1)} {W' : (Fin (N + 1) → ℝ) →L[ℝ] Fin N → ℝ} (hW' : HasFDerivAt (arcWeights ε) W' z.1) (i : Fin (N + 1)) : SigmaLayer.dMom (strokeH ε t q) z i = 0

∂ᵧᵢ𝓗_t = 0: the stroke Hamiltonian is momentum-independent.

theorem CSD.RecordLayer.hamiltonianField_strokeH {N : ℕ} (ε t : ℝ) (q : Pointer N) {z : SigmaLayer.Chart (N + 1)} {W' : (Fin (N + 1) → ℝ) →L[ℝ] Fin N → ℝ} (hW' : HasFDerivAt (arcWeights ε) W' z.1) : SigmaLayer.hamiltonianField (strokeH ε t q) z = (0, fun (i : Fin (N + 1)) => -(deriv Real.smoothTransition t * (Real.pi / 2) * ∑ k : Fin N, outcomeEnergy k q * W' (Pi.single i 1) k))

The Hamiltonian field of the stroke Hamiltonian: positions frozen, momenta driven by −∂ₓ𝓗.

The generated chart curve

noncomputable def CSD.RecordLayer.strokeCurve {N : ℕ} (ε : ℝ) (d : ConservedData N) (t : ℝ) : SigmaLayer.Chart (N + 1)

The chart curve the stroke generates from the frozen data d: the positions stay at the frozen chart position (the Hamiltonian is momentum-independent), and each conjugate momentum accumulates −∫₀ᵗ ∂ₓᵢ𝓗_s ds, with 𝓗_s evaluated on the actual pointer trajectory strokeTraj ε d s.

Equations

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

theorem CSD.RecordLayer.strokeCurve_fst {N : ℕ} (ε : ℝ) (d : ConservedData N) (t : ℝ) : (strokeCurve ε d t).1 = chartPos d

theorem CSD.RecordLayer.strokeCurve_zero {N : ℕ} (ε : ℝ) (d : ConservedData N) : strokeCurve ε d 0 = (chartPos d, 0)

theorem CSD.RecordLayer.strokeCurve_one_snd {N : ℕ} (ε : ℝ) (d : ConservedData N) : (strokeCurve ε d 1).2 = shiftReal ε d

At the end of the stroke the momenta have moved by exactly the real shift.

theorem CSD.RecordLayer.hamiltonianShift_eq_strokeCurve_one {N : ℕ} (ε : ℝ) (d : ConservedData N) : hamiltonianShift ε d = (fun (j : Fin N) => ↑((strokeCurve ε d 1).2 j.castSucc), ↑((strokeCurve ε d 1).2 (Fin.last N)))

The Hamiltonian shift is the endpoint of the generated curve, read on the torus.

theorem CSD.RecordLayer.strokeCurve_hasDerivAt_hamiltonianField {N : ℕ} (ε : ℝ) (hε : 0 < ε) {d : ConservedData N} (hreg : RegularPos ε (chartPos d)) (t : ℝ) : HasDerivAt (strokeCurve ε d) (SigmaLayer.hamiltonianField (strokeH ε t (strokeTraj ε d t)) (strokeCurve ε d t)) t

★★ Chart-level generation of the Hamiltonian shift. On regular data — every context rate strictly inside (2ε, 1), so the chart weights are smooth at the frozen position — the stroke curve is an integral curve of the time-dependent stroke Hamiltonian, evaluated on the actual pointer trajectory: γ̇(t) = X_{𝓗_t(q(t))}(γ(t)) for every t. The positions stay frozen (∂ᵧ𝓗 = 0) and the momenta are driven by −∂ₓ𝓗_t — the fundamental theorem of calculus applied to the continuous stroke energies. Together with hamiltonianShift_eq_strokeCurve_one, this is the statement "the shift jointLift is fed is what the stroke Hamiltonian generates in the conjugate directions".

Headline corollaries: the Hamiltonian shift fed to the joint lift

theorem CSD.RecordLayer.jointLift_eq_pointerEvolve_off_corridor {N : ℕ} (ε : ℝ) (c : ContextField N) (hε : 0 < ε) {y : PointerArena N N} (hy : OffCorridor ε (conservedData c y)) : jointLift c ε (hamiltonianShift ε) y = pointerEvolve c ε y

Off the corridor, the Hamiltonian-shift joint lift is the fibrewise witness. Where the register sits strictly inside a plateau of every cell the weights are locally constant, the generated shift vanishes and the base does not move — exactly as SigmaLayer/UntriggeredFlow predicts for the untriggered region.

theorem CSD.RecordLayer.isJointLift_hamiltonianShift {N : ℕ} (ε : ℝ) {c : ContextField N} (hct : c.TorusInvariant) : IsJointLift c ε (jointLift c ε (hamiltonianShift ε))

★★ The Hamiltonian-shift joint lift is a joint lift. For every torus-invariant context, landing, the ε-Born sandwich, the outcome-sector identity and the moment-marginal law (JointFlowTransfer.lean) hold for the map whose base is shifted by what the stroke Hamiltonian generates.

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

★★ Liouville's theorem for the Hamiltonian-shift joint lift. The generated shift is measurable (measurable_hamiltonianShift), so jointLift_measurePreserving applies: the back-reacting map preserves the arena Liouville measure.