RecordLayer/JointLift: a back-reacting joint lift of the measurement stroke, on the arena

Category: 7-SigmaLayer (dynamical measurement) — specs/BACKLOG.md §A, the instance the conditional transfer JointFlowTransfer.lean was waiting for.

What this is

JointFlowTransfer.lean proved that any map Φ satisfying IsJointLift c ε Φ — pointer driven by the fibrewise propagator, context rates and register conserved — inherits landing, the ε-Born sandwich and the moment-marginal law. Until now the only instance was the fibrewise witness itself (isJointLift_pointerEvolve), whose base does not move at all.

jointLift c ε Δ is a family of instances whose base does move:

jointLift c ε Δ y = pointerEvolve c ε (torusAct (Δ (conservedData c y)) y).

The point y is first twisted by a torus element Δ(m, θ₁, q) — a shift that may depend on all the conserved data (the context rates m = c.rate y.1.1, the register θ₁, and the pointer q) but on nothing else — and then the pointer is driven as before. Because the twist moves the base only along its moment fibre and translates only the conjugate θ₂, everything the stroke reads is untouched, and:

• ★★ isJointLift_jointLift — for every torus-invariant context and every shift Δ, jointLift c ε Δ is a joint lift. Hence, with no further work, (isJointLift_jointLift …).landing, .born_lower, .born_upper, .outcomeSector_eq, .moment_marginal_unchanged all hold for it.
• ★★ jointLift_measurePreserving — for every measurable shift, jointLift c ε Δ preserves the arena Liouville measure. This is the arena-level Liouville theorem for the back-reacting map, obtained without disintegrating along the moment fibres: the general invariant-twist lemma MeasurePreserving.vadd_twist_of_invariant applied to the arena torus of ArenaTorus.lean, composed with pointerEvolve_measurePreserving.
• jointLift_fst, jointLift_conjugate — the base is rotated by phaseUnitary (Δ …).1 and θ₂ is translated by (Δ …).2; jointLift_base_moves_of_ne gives the concrete base-moves witness: wherever the shift's phases differ on two coordinates supporting the state, the ontic base point genuinely moves.
• jointLift_eq_pointerEvolve_of_shift_eq_zero — where the shift vanishes the joint lift is the fibrewise witness, so the latter is the special case Δ = 0 (jointLift_zero).

What this does and does not settle

The shift Δ is a parameter here. This module proves that the whole class of conserved-data twists is harmless to records, Born, and Liouville measure — the structural statement "back-reaction lives in the torus directions and is invisible to the record". Which Δ the interaction Hamiltonian actually produces is a separate question: the chart computation in SigmaLayer/UntriggeredFlow.lean shows the conjugate coordinate absorbs -∫ ∂_m 𝓗, and RecordLayer/HamiltonianShift.lean builds that shift from the pointer trajectory. Nothing in this module identifies jointLift with the time-1 map of a Hamiltonian flow on the arena manifold (⚠️ RESIDUE(R-016)).

References

specs/frozen-base-obstruction-scoping.md (brick 3); specs/future-work.md; RecordLayer/JointFlowTransfer.lean (IsJointLift, the transfer theorems); RecordLayer/ArenaTorus.lean (torusAct, torusAct_measurePreserving, ContextField.TorusInvariant); Mathlib/MeasureTheory/InvariantTwist.lean (MeasurePreserving.vadd_twist_of_invariant); RecordLayer/PointerWeights.lean (pointerEvolve, pointerEvolve_measurePreserving).

The conserved data

@[reducible, inline]

abbrev CSD.RecordLayer.ConservedData (N : ℕ) : Type

The data of an arena point that the measurement stroke conserves and a shift may read: the context rates, the register coordinate, and the pointer.

Equations

• CSD.RecordLayer.ConservedData N = ((Fin N → ℝ) × AddCircle 1 × CSD.RecordLayer.Pointer N)

def CSD.RecordLayer.conservedData {N : ℕ} (c : ContextField N) (y : PointerArena N N) : ConservedData N

Read the conserved data of an arena point.

Equations

• CSD.RecordLayer.conservedData c y = (c.rate y.1.1, y.1.2.1, y.2)

theorem CSD.RecordLayer.measurable_conservedData {N : ℕ} (c : ContextField N) : Measurable (conservedData c)

theorem CSD.RecordLayer.conservedData_torusAct {N : ℕ} {c : ContextField N} (hct : c.TorusInvariant) (g : ArenaTorus N) (y : PointerArena N N) : conservedData c (torusAct g y) = conservedData c y

The torus action does not change the conserved data — for a torus-invariant context.

theorem CSD.RecordLayer.pointerWeights_torusAct {N : ℕ} {c : ContextField N} (hct : c.TorusInvariant) (ε : ℝ) (g : ArenaTorus N) (y : PointerArena N N) : pointerWeights c ε (torusAct g y).1 = pointerWeights c ε y.1

The weights read only conserved data, so the torus action does not change them.

The joint lift

noncomputable def CSD.RecordLayer.jointLift {N : ℕ} (c : ContextField N) (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) (y : PointerArena N N) : PointerArena N N

The joint lift with shift Δ. Twist the point by the torus element the conserved data prescribes, then drive the pointer with the fibrewise propagator.

Equations

• CSD.RecordLayer.jointLift c ε Δ y = CSD.RecordLayer.pointerEvolve c ε (CSD.RecordLayer.torusAct (Δ (CSD.RecordLayer.conservedData c y)) y)

theorem CSD.RecordLayer.jointLift_fst {N : ℕ} (c : ContextField N) (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) (y : PointerArena N N) : (jointLift c ε Δ y).1 = (phaseUnitary (Δ (conservedData c y)).1 • y.1.1, y.1.2.1, y.1.2.2 + (Δ (conservedData c y)).2)

The base is rotated along its moment fibre and θ₂ is translated; the register is fixed.

theorem CSD.RecordLayer.jointLift_base {N : ℕ} (c : ContextField N) (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) (y : PointerArena N N) : (jointLift c ε Δ y).1.1 = phaseUnitary (Δ (conservedData c y)).1 • y.1.1

theorem CSD.RecordLayer.jointLift_register {N : ℕ} (c : ContextField N) (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) (y : PointerArena N N) : (jointLift c ε Δ y).1.2.1 = y.1.2.1

theorem CSD.RecordLayer.jointLift_conjugate {N : ℕ} (c : ContextField N) (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) (y : PointerArena N N) : (jointLift c ε Δ y).1.2.2 = y.1.2.2 + (Δ (conservedData c y)).2

The conjugate coordinate absorbs the shift.

theorem CSD.RecordLayer.jointLift_eq_pointerEvolve_of_shift_eq_zero {N : ℕ} (c : ContextField N) (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) {y : PointerArena N N} (h : Δ (conservedData c y) = 0) : jointLift c ε Δ y = pointerEvolve c ε y

Where the shift vanishes, the joint lift is the fibrewise witness.

@[simp]

theorem CSD.RecordLayer.jointLift_zero {N : ℕ} (c : ContextField N) (ε : ℝ) : (jointLift c ε fun (x : ConservedData N) => 0) = pointerEvolve c ε

The fibrewise witness is the joint lift with zero shift.

theorem CSD.RecordLayer.isJointLift_jointLift {N : ℕ} (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) {c : ContextField N} (hct : c.TorusInvariant) : IsJointLift c ε (jointLift c ε Δ)

The joint lift is a joint lift (for a torus-invariant context). All of JointFlowTransfer.lean — landing, the ε-Born sandwich, the outcome-sector identity, the moment-marginal law — now applies to a map whose base genuinely moves.

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

Liouville's theorem for the back-reacting joint lift. For every measurable shift, the joint lift preserves the arena Liouville measure μ_FS ⊗ vol_{T²} ⊗ μ_FS^{ptr}. The proof never disintegrates along the moment fibres: the twist y ↦ torusAct (Δ (conservedData c y)) y preserves measure by MeasurePreserving.vadd_twist_of_invariant — every torusAct g does, Haar measure on the arena torus is a left-invariant probability, and the conserved data is torus-invariant — and the fibrewise propagator preserves it by pointerEvolve_measurePreserving.

theorem CSD.RecordLayer.jointLift_base_moves_of_ne {N : ℕ} (c : ContextField N) (ε : ℝ) (Δ : ConservedData N → ArenaTorus N) {y : PointerArena N N} {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) (hy : y.1.1 = Projectivization.mk ℂ v hv) {j k : Fin N} (hj : v.ofLp j ≠ 0) (hk : v.ofLp k ≠ 0) (hg : circlePhase ((Δ (conservedData c y)).1 j) ≠ circlePhase ((Δ (conservedData c y)).1 k)) : (jointLift c ε Δ y).1.1 ≠ y.1.1

The base moves. Wherever the shift's phases differ on two coordinates that support the state, the joint lift displaces the ontic base point — the back-reaction the fibrewise witness could not show. (Together with isJointLift_jointLift, this is "the base moves and the record survives" on the arena, not in a chart.)