SigmaLayer/JointFlowTransfer: back-reaction is harmless to records and Born

Category: dynamical measurement — specs/BACKLOG.md A1, the formalisable half of the joint-arena Hamiltonian route.

The problem this solves

Paper C A2 / TN6 ask for measurement generated by a scalar 𝓗 on the whole arena. The corpus's smooth witness is fibrewise: pointerEvolve freezes the ontic coordinate (pointerEvolve_fst : (pointerEvolve c ε y).1 = y.1, by rfl), so it is not the flow of any interaction scalar wherever the weights vary (PointerGeneration.lean's boundary note). A genuine joint flow moves the base too — it back-reacts — and the worry is that the back-reaction destroys the landing and Born analysis built on the frozen-base map.

This module proves it does not, and isolates exactly why.

What is proved

IsJointLift c ε Φ asks of a candidate joint flow Φ only three things: its pointer component agrees with the fibrewise witness, and it conserves the context rates and the register coordinate. Then:

• ★★ IsJointLift.outcomeSector_eq — Φ's record preimage is the same set as the fibrewise witness's outcome sector. Not "the same measure": literally the same set. The record regions are cylinders over the pointer (arenaRecord N j = univ ×ˢ recordRegion j), so horizontal motion cannot be seen by them.
• ★ IsJointLift.landing, IsJointLift.born_lower, IsJointLift.born_upper — landing and the full ε-Born sandwich hold for Φ, transported along that set equality with no measure-theoretic work at all.
• IsJointLift.weights_conserved — the weight field is constant along Φ. This is where the Poisson argument plugs in: it is exactly what {wᵢ,wⱼ} = 0 delivers, and it is what makes iterating the stroke well-defined.
• ★ IsJointLift.moment_marginal_unchanged — the honest replacement for the no-collapse theorem. pointerEvolve_base_marginal_unchanged says the fibrewise witness leaves the sector marginal untouched; under a genuine lift that is false, because the base point moves inside its moment fibre. What survives — and all that is needed — is that the moment-and-register data is unchanged.
• isJointLift_pointerEvolve — the fibrewise witness is itself a joint lift, so none of this is vacuous.

Why the hypotheses are these and not the obvious ones

The first draft of this row asked for "arena-measure preservation" and "basinIndex conserved". Both were wrong, and the corrections are worth recording:

• Born is measured against pointerPrep, a base-Dirac slice (epistemicMeasure p ⊗ ready-conditioned FS), which is null for the arena Liouville measure. So "Hamiltonian ⇒ Liouville-preserving" says nothing about the Born statements. What actually carries them is the set equality above.
• basinIndex is the selector of the shear/swap witnesses. The smooth witness lands on shrunkCell membership instead. Conserving the rates and the register conserves both; conserving basinIndex alone would not.

⚠️ Honest scope. (i) This is a conditional (CONVENTIONS.md §8.3 _of_ pattern): it makes back-reaction harmless given the three hypotheses, and does not construct a joint flow satisfying them. Discharging them for the actual X_𝓗 is the paper's job (BACKLOG.md A2) and needs {wᵢ,wⱼ} = 0, which is well-formed only now that the weights are C^∞ (SmoothProfile.lean, B1). (ii) The transfer covers the single measurement stroke — landing and the sector Born. The protocol's two-time laws and persistence are statements about a whole propagator family, not about one map, and are not restated here. (iii) Nothing here says the joint flow is Hamiltonian; that identification is the §2a-scoped arrow (MATHLIB-GAPS.md). (iv) There is no perturbative version: circleCell is half-open and rep jumps at 0, so the selector is discontinuous in the conserved data — approximate conservation buys nothing without a separate collar estimate.

References

specs/BACKLOG.md A1 (this row), A2 (the paper half), B1 (the discharged prerequisite); SigmaLayer/PointerLanding.lean (pointer_landing), SigmaLayer/PointerBorn.lean (pointer_born_lower/_upper, pointerPrep), SigmaLayer/PointerGeneration.lean (the fibrewise boundary this answers), SigmaLayer/PointerWeights.lean (contDiff_pointerWeights_lift).

structure CSD.RecordLayer.IsJointLift {N : ℕ} (c : ContextField N) (ε : ℝ) (Φ : PointerArena N N → PointerArena N N) : Prop

What a joint lift of the measurement stroke must satisfy. Deliberately weak: the pointer component agrees with the fibrewise witness, and the data the weights and the cell geometry read — the context rates and the register coordinate — is conserved. The base point itself is free to move, which is exactly what back-reaction does.

• pointer_eq (y : PointerArena N N) : (Φ y).2 = (pointerEvolve c ε y).2

  The pointer is driven by the same fixed-weight propagator.

• rate_conserved (y : PointerArena N N) (j : Fin N) : c.rate (Φ y).1.1 j = c.rate y.1.1 j

  The context rates (the moments, for momentContext) are constants of motion.

• register_conserved (y : PointerArena N N) : (Φ y).1.2.1 = y.1.2.1

  The register coordinate is a constant of motion.

theorem CSD.RecordLayer.IsJointLift.mem_arenaRecord_iff {N : ℕ} (y : PointerArena N N) (j : Fin N) : y ∈ arenaRecord N j ↔ y.2 ∈ recordRegion j

Membership of a record cylinder reads the pointer only.

theorem CSD.RecordLayer.IsJointLift.outcomeSector_eq {N : ℕ} {c : ContextField N} {ε : ℝ} {Φ : PointerArena N N → PointerArena N N} (h : IsJointLift c ε Φ) (j : Fin N) : Φ ⁻¹' arenaRecord N j = pointerEvolve c ε ⁻¹' arenaRecord N j

★★ The record preimages coincide — as sets. Horizontal back-reaction is invisible to the record regions because they are cylinders over the pointer, and the pointer component is unchanged by hypothesis. Every sector-measure statement follows from this without any measure theory.

theorem CSD.RecordLayer.IsJointLift.weights_conserved {N : ℕ} {c : ContextField N} {ε : ℝ} {Φ : PointerArena N N → PointerArena N N} (h : IsJointLift c ε Φ) (y : PointerArena N N) : pointerWeights c ε (Φ y).1 = pointerWeights c ε y.1

The weight field is a constant of motion. This is precisely what the Poisson argument {wᵢ,wⱼ} = 0 delivers, and it is what makes repeating the stroke coherent: the second stroke sees the same weights as the first.

theorem CSD.RecordLayer.IsJointLift.moment_marginal_unchanged {N : ℕ} {c : ContextField N} {ε : ℝ} {Φ : PointerArena N N → PointerArena N N} (h : IsJointLift c ε Φ) : (fun (y : PointerArena N N) => (c.rate (Φ y).1.1, (Φ y).1.2.1)) = fun (y : PointerArena N N) => (c.rate y.1.1, y.1.2.1)

★ The honest replacement for the no-collapse theorem. The fibrewise witness leaves the whole sector marginal untouched (pointerEvolve_base_marginal_unchanged); a genuine lift does not, because the base point moves inside its moment fibre. What survives is that the moment-and-register data — everything the measurement actually reads — is unchanged. Any joint-flow prose should claim this and not the stronger statement.

theorem CSD.RecordLayer.IsJointLift.landing {N : ℕ} {c : ContextField N} {ε : ℝ} {Φ : PointerArena N N → PointerArena N N} (h : IsJointLift c ε Φ) {δ : ℝ} (hε : 0 < ε) (hδ : δ ≤ 1 / 2) {y : PointerArena N N} {j : Fin N} (hsec : y.1 ∈ shrunkCell c ε j) (hready : y.2 ∈ readyRegion δ) : Φ y ∈ arenaRecord N j

★ Landing transfers. A ready pointer over the ε-shrunk cell of outcome j lands in j's record region under any joint lift — back-reaction included.

theorem CSD.RecordLayer.IsJointLift.protocol_outcomeSector_eq {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hδ : δ ≤ 1 / 2) (j : Fin N) : (pointerProtocol c hc ε hδ).outcomeSector j = pointerEvolve c ε ⁻¹' arenaRecord N j

The fibrewise witness's outcome sector, in record-preimage form.

theorem CSD.RecordLayer.IsJointLift.born_lower {N : ℕ} {c : ContextField N} {ε : ℝ} {Φ : PointerArena N N → PointerArena N N} (h : IsJointLift c ε Φ) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) (p : LF4.CPN N) (q₀ : Pointer N) (j : Fin N) : ENNReal.ofReal (c.rate p j - 2 * ε) ≤ (pointerPrep p q₀ δ) (Φ ⁻¹' arenaRecord N j)

★ The lower Born bound transfers.

theorem CSD.RecordLayer.IsJointLift.born_upper {N : ℕ} [NeZero N] {c : ContextField N} {ε : ℝ} {Φ : PointerArena N N → PointerArena N N} (h : IsJointLift c ε Φ) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) (p : LF4.CPN N) (q₀ : Pointer N) (i : Fin N) : (pointerPrep p q₀ δ) (Φ ⁻¹' arenaRecord N i) ≤ ENNReal.ofReal (c.rate p i + 2 * (↑N - 1) * ε)

★ The upper Born bound transfers.

theorem CSD.RecordLayer.isJointLift_pointerEvolve {N : ℕ} (c : ContextField N) (ε : ℝ) : IsJointLift c ε (pointerEvolve c ε)

The fibrewise witness is a joint lift — with zero back-reaction. Non-vacuity: every theorem above has at least this instance, so the hypotheses are satisfiable.

★★ The transfer, bundled

structure CSD.RecordLayer.JointFlowTransfer {N : ℕ} (c : ContextField N) (ε δ : ℝ) (Φ : PointerArena N N → PointerArena N N) : Prop

Back-reaction is harmless: for any joint lift of the measurement stroke, landing and the full ε-Born sandwich hold exactly as they do for the frozen-base witness, and the weight field and moment-register data are constants of motion. The conditional half of the joint-arena Hamiltonian route (BACKLOG.md A1); the paper supplies the hypotheses.

• weights_conserved (y : PointerArena N N) : pointerWeights c ε (Φ y).1 = pointerWeights c ε y.1

  The weights are constants of motion.

• moment_marginal_unchanged : (fun (y : PointerArena N N) => (c.rate (Φ y).1.1, (Φ y).1.2.1)) = fun (y : PointerArena N N) => (c.rate y.1.1, y.1.2.1)

  The measurement-relevant data is unchanged (the no-collapse replacement).

• landing {y : PointerArena N N} {j : Fin N} : y.1 ∈ shrunkCell c ε j → y.2 ∈ readyRegion δ → Φ y ∈ arenaRecord N j

  Records are created, back-reaction notwithstanding.

• born_lower (p : LF4.CPN N) (q₀ : Pointer N) (j : Fin N) : ENNReal.ofReal (c.rate p j - 2 * ε) ≤ (pointerPrep p q₀ δ) (Φ ⁻¹' arenaRecord N j)

  The ε-Born sandwich, lower half.

• born_upper (p : LF4.CPN N) (q₀ : Pointer N) (i : Fin N) : (pointerPrep p q₀ δ) (Φ ⁻¹' arenaRecord N i) ≤ ENNReal.ofReal (c.rate p i + 2 * (↑N - 1) * ε)

  The ε-Born sandwich, upper half.

theorem CSD.RecordLayer.jointFlowTransfer {N : ℕ} [NeZero N] {c : ContextField N} {ε : ℝ} {Φ : PointerArena N N → PointerArena N N} (h : IsJointLift c ε Φ) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) : JointFlowTransfer c ε δ Φ

★★ The transfer theorem. Every joint lift enjoys the whole package.