SigmaLayer/UntriggeredFlow: one flow that records and back-reacts, with no trigger

Category: 7-SigmaLayer (dynamical measurement) — specs/frozen-base-obstruction-scoping.md brick 2.

What this is

specs/BACKLOG.md row 350 closes on: "the relocation is not the obstacle; the trigger is." The corpus's measurement is two strokes — create the record, then a readout-triggered relocation. Brick 1 (SigmaLayer/FrozenBase.lean) says why one stroke could not do both while the base stayed frozen: a C¹ generator with a pointwise-frozen base is base-constant, so it cannot depend on the outcome at all.

This module supplies the converse witness in the chart. One Hamiltonian, one flow, no trigger, no second stroke:

𝓗(z) = (Σᵢ cᵢ xᵢ) · y_k, with c k = 0

the ontic analogue of the textbook von Neumann coupling  ⊗ p̂, with the base position read out onto the pointer. Hamilton's equations give, in closed form:

• ẋ_k = Σᵢ cᵢ xᵢ — the record. The pointer coordinate drifts at a rate set by the base, so its displacement is the measured value (untriggeredCurve_records).
• ẏᵢ = −cᵢ · y_k — the back-reaction. The base momenta move, at a rate set by the pointer momentum (untriggeredCurve_backreacts).
• ẋⱼ = 0 for j ≠ k, and ẏ_k = 0: everything else is fixed, which is what makes the system integrable in closed form.

★★ untriggeredCurve_isHamiltonianCurve — the explicit curve is an integral curve of the coupling.

★ The loop with brick 1 closes

not_baseFrozen_interactionH shows this generator is not BaseFrozen whenever the coupling and the pointer momentum are both non-trivial — which brick 1 requires, since the generator is outcome-dependent by construction. The two modules are the two directions of one statement: brick 1 says an outcome-dependent C¹ generator must move the base; this exhibits one that does, and computes exactly how much (−cᵢ·y_k per unit time).

Note which base coordinate moves. The base position is fixed (ẋⱼ = 0 for j ≠ k) — the measured value is not disturbed, so the measurement is repeatable — while the base momentum absorbs the back-reaction. That is the ontic form of "a measurement disturbs the conjugate variable", and it is a computation here rather than a slogan.

⚠️ Honest scope — this does NOT close H_int(M)

1. A chart witness, not an arena one. Chart n is globally ℝ^{2n}; the arena is not, and nothing here transports (SigmaLayer/ChartBracket.lean honest scope). The chart→arena transport remains open (⚠️ RESIDUE(R-016)).
2. A witness, not a derivation. 𝓗 is engineered to record. That a physically natural interaction must take this form is not shown and is not the kind of thing Lean shows — which interaction an apparatus realises is a permanent boundary (⚠️ RESIDUE(R-015)).
3. Records here are not yet Born weights. This module builds the dynamics; it does not redo shear_sector_born on it, so the measure-theoretic half — that the basins of this flow carry the moment-map weights — is not established. That is the work an arena-level successor would have to do, and it is not attempted.
4. c k = 0 is a hypothesis, and it is what keeps the system closed-form: with c k ≠ 0 the pointer feeds back into its own drift rate and the flow is no longer affine.
5. Uniqueness is not proved here. RESOLVED — SigmaLayer/UntriggeredVolume.lean establishes the LipschitzWith bound (lipschitzWith_interactionH_field: the field is a continuous linear map, so its operator norm is a Lipschitz constant) and feeds it to brick 0's hamiltonianCurve_unique, giving untriggeredCurve_unique: this is the integral curve through z₀, not merely an integral curve. The same module proves the flow preserves chart volume (untriggeredCurve_measurePreserving). (This item originally recorded the gap; the strikethrough keeps the record.)

References

specs/frozen-base-obstruction-scoping.md (brick 2); specs/BACKLOG.md (row "★★ The dynamical measurement layer (Paper D H_int)", the trigger); specs/future-work.md; SigmaLayer/ChartBracket.lean (Chart, dPos, dMom, hamiltonianField); SigmaLayer/ChartIntegralCurve.lean (brick 0 — IsHamiltonianCurve, hamiltonianCurve_unique); SigmaLayer/FrozenBase.lean (brick 1 — BaseFrozen, not_baseFrozen_of_outcomeDependent); RecordLayer/ShearWitness.lean (the two-stroke witness this is the one-stroke counterpart to); RecordLayer/JoinGeneration.lean (joinSwap_eq_flowTimeOne, the triggered relocation).

The coupling

noncomputable def CSD.SigmaLayer.posCLM {n : ℕ} (c : Fin n → ℝ) : Chart n →L[ℝ] ℝ

The base functional z ↦ Σᵢ cᵢ xᵢ, as a continuous linear map.

Equations

• CSD.SigmaLayer.posCLM c = (∑ i : Fin n, c i • ContinuousLinearMap.proj i) ∘SL ContinuousLinearMap.fst ℝ (Fin n → ℝ) (Fin n → ℝ)

@[simp]

theorem CSD.SigmaLayer.posCLM_apply {n : ℕ} (c : Fin n → ℝ) (z : Chart n) : (posCLM c) z = ∑ i : Fin n, c i * z.1 i

noncomputable def CSD.SigmaLayer.momCoord {n : ℕ} (k : Fin n) : Chart n →L[ℝ] ℝ

The pointer-momentum functional z ↦ y_k.

Equations

• CSD.SigmaLayer.momCoord k = ContinuousLinearMap.proj k ∘SL ContinuousLinearMap.snd ℝ (Fin n → ℝ) (Fin n → ℝ)

@[simp]

theorem CSD.SigmaLayer.momCoord_apply {n : ℕ} (k : Fin n) (z : Chart n) : (momCoord k) z = z.2 k

noncomputable def CSD.SigmaLayer.interactionH {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z : Chart n) : ℝ

The von Neumann coupling in the chart: 𝓗(z) = (Σᵢ cᵢ xᵢ) · y_k. The base position is coupled to the pointer momentum, so the pointer translates at a base-dependent rate.

Equations

• CSD.SigmaLayer.interactionH c k z = (∑ i : Fin n, c i * z.1 i) * z.2 k

theorem CSD.SigmaLayer.hasFDerivAt_interactionH {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z : Chart n) : HasFDerivAt (interactionH c k) ((∑ i : Fin n, c i * z.1 i) • momCoord k + z.2 k • posCLM c) z

theorem CSD.SigmaLayer.fderiv_interactionH {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z : Chart n) : fderiv ℝ (interactionH c k) z = (∑ i : Fin n, c i * z.1 i) • momCoord k + z.2 k • posCLM c

Hamilton's equations for the coupling

theorem CSD.SigmaLayer.sum_mul_single {n : ℕ} (c : Fin n → ℝ) (i : Fin n) : ∑ x : Fin n, c x * Pi.single i 1 x = c i

Contracting a coefficient vector against a coordinate direction.

@[simp]

theorem CSD.SigmaLayer.dPos_interactionH {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z : Chart n) (i : Fin n) : dPos (interactionH c k) z i = c i * z.2 k

@[simp]

theorem CSD.SigmaLayer.dMom_interactionH {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z : Chart n) (i : Fin n) : dMom (interactionH c k) z i = if i = k then ∑ j : Fin n, c j * z.1 j else 0

★ The loop with brick 1

theorem CSD.SigmaLayer.not_baseFrozen_interactionH {n : ℕ} {c : Fin n → ℝ} {k : Fin n} {S : Finset (Fin n)} {i : Fin n} (hiS : i ∈ S) (hc : c i ≠ 0) (z : Chart n) (hz : z.2 k ≠ 0) : ¬BaseFrozen (interactionH c k) S

★ The recording generator is not base-frozen — exactly as brick 1 requires. If the coupling is non-trivial at some base index and the pointer momentum is non-zero somewhere, BaseFrozen fails: the flow must move the base.

The flow, in closed form

noncomputable def CSD.SigmaLayer.untriggeredCurve {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z₀ : Chart n) (t : ℝ) : Chart n

The one-stroke measurement flow. Positions: only the pointer coordinate k moves, at the base-determined rate Σᵢ cᵢ xᵢ. Momenta: every base momentum drifts at −cᵢ·y_k, the back-reaction.

Equations

• CSD.SigmaLayer.untriggeredCurve c k z₀ t = (fun (j : Fin n) => if j = k then z₀.1 k + t * ∑ i : Fin n, c i * z₀.1 i else z₀.1 j, fun (j : Fin n) => z₀.2 j - t * (c j * z₀.2 k))

@[simp]

theorem CSD.SigmaLayer.untriggeredCurve_zero {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z₀ : Chart n) : untriggeredCurve c k z₀ 0 = z₀

theorem CSD.SigmaLayer.untriggeredCurve_snd_k {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (z₀ : Chart n) (t : ℝ) : (untriggeredCurve c k z₀ t).2 k = z₀.2 k

The pointer momentum is conserved (because c k = 0), so the drift rate is constant.

theorem CSD.SigmaLayer.untriggeredCurve_fst_ne {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z₀ : Chart n) (t : ℝ) {j : Fin n} (hj : j ≠ k) : (untriggeredCurve c k z₀ t).1 j = z₀.1 j

The base positions are conserved, so the measured value is not disturbed.

theorem CSD.SigmaLayer.untriggeredCurve_sum {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (z₀ : Chart n) (t : ℝ) : ∑ i : Fin n, c i * (untriggeredCurve c k z₀ t).1 i = ∑ i : Fin n, c i * z₀.1 i

The coupling's value is conserved along the curve — the reason the system is affine.

★★ It is the integral curve

theorem CSD.SigmaLayer.untriggeredCurve_isHamiltonianCurve {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (z₀ : Chart n) : IsHamiltonianCurve (interactionH c k) (untriggeredCurve c k z₀)

★★ The one-stroke flow is an integral curve of the coupling — a single Hamiltonian flow that creates the record and back-reacts, with no readout trigger anywhere.

★ What it does: a record, and a back-reaction

theorem CSD.SigmaLayer.untriggeredCurve_records {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z₀ : Chart n) (t : ℝ) : (untriggeredCurve c k z₀ t).1 k - z₀.1 k = t * ∑ i : Fin n, c i * z₀.1 i

★ The record. The pointer's displacement at time t is exactly t times the measured base quantity — the readout, as a closed-form computation.

theorem CSD.SigmaLayer.untriggeredCurve_backreacts {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z₀ : Chart n) (t : ℝ) (i : Fin n) : (untriggeredCurve c k z₀ t).2 i = z₀.2 i - t * (c i * z₀.2 k)

★ The back-reaction. Each base momentum moves at −cᵢ·y_k. The base position is untouched (untriggeredCurve_fst_ne), so the measured value is repeatable while its conjugate absorbs the disturbance.

theorem CSD.SigmaLayer.untriggeredCurve_backreaction_ne {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (z₀ : Chart n) {t : ℝ} (ht : t ≠ 0) {i : Fin n} (hc : c i ≠ 0) (hz : z₀.2 k ≠ 0) : (untriggeredCurve c k z₀ t).2 i ≠ z₀.2 i

The back-reaction is genuinely non-trivial: at any t ≠ 0, a non-trivial coupling and a non-zero pointer momentum move the base momentum.