SigmaLayer/FrozenBase: a frozen base forbids an outcome-dependent generator

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

The statement

Both of the corpus's record-creating witnesses freeze the base pointwise: Prod.fst ∘ evolve = Prod.fst, from which shear_base_marginal_unchanged and pointerEvolve_base_marginal_unchanged follow by rfl. This module prices that choice.

(a) ∧ (c′) ⇒ ¬(b) — a generator that is C¹ on a Darboux chart (a), whose flow leaves the base block pointwise fixed (c′), cannot depend on the base — so it cannot depend on the outcome index, and no record correlated with the outcome can be created (¬b).

• ★ BaseFrozen — (c′) as a condition on the generator: both partials vanish on the base block S. This is exactly "the base components of hamiltonianField H are identically zero", i.e. ẋ_S = 0 and ẏ_S = 0.
• ★★ baseConstant_of_baseFrozen — the theorem. A base-frozen C¹ generator takes the same value at any two points that agree off S.
• ★★ not_baseFrozen_of_outcomeDependent — the contrapositive, in the shape the obstruction is used: a generator that does distinguish two base sectors sharing a fibre point is not base-frozen. Its flow must move the base.

Why the base block carries BOTH coordinates

LF4.KSigma N = ℂℙ^{N-1} × T² is a full even-dimensional symplectic factor: base positions and base momenta both live in the base slot. So (c′) kills both halves of (∂_y 𝓗, −∂_x 𝓗) on S, and the conclusion is that 𝓗 is base-constant, not merely locally constant. ⚠️ This is the correction that makes the argument non-circular: reading (c′) as killing only one partial yields "locally constant with seams", which is ¬(a) assumed in order to derive ¬(a). See specs/frozen-base-obstruction-scoping.md §5.

⚠️ Honest scope

Two side conditions, both explicit in the statements, and neither is automatic.

1. Product ω. The chart is Chart n = (Fin n → ℝ) × (Fin n → ℝ) with the canonical form, and S/T split the index set. True of PointerArena N K := LF4.KSigma N × Pointer K, a product of Kähler factors; false in general — a coupling that geometrically entangles system and apparatus need not split, and then the base component of the field picks up fibre derivatives through the cross terms and this argument dies.
2. C¹. Differentiable ℝ H is a hypothesis, not a consequence. Dropping it is exactly the seam horn (RecordLayer/PiecewiseHamiltonian.lean).

This does not say back-reaction is required, and does not say the corpus's witnesses are defective. RecordLayer/JointFlowTransfer.lean proves the opposite direction — a genuine joint lift does move the base, and back-reaction is harmless to records and Born (IsJointLift.moment_marginal_unchanged). What this module adds is the price of the other choice: freezing the base costs outcome-dependence of the generator. Both are theorems; the corpus is not forced onto either horn.

And it is a chart statement. Nothing here transports to the arena — that transport is the missing arrow (SigmaLayer/ChartBracket.lean honest scope, unchanged), and the mathematics of H_int(M) remains open (⚠️ RESIDUE(R-016)). Which physical interaction an apparatus realises is a permanent boundary rather than open work (⚠️ RESIDUE(R-015)).

References

specs/frozen-base-obstruction-scoping.md (brick 1, and §5 for the withdrawn draft); specs/BACKLOG.md A2/A3/A4; specs/future-work.md; SigmaLayer/ChartBracket.lean (Chart, dPos, dMom, hamiltonianField); SigmaLayer/ChartIntegralCurve.lean (brick 0 — the integral curve exists and is unique); RecordLayer/ShearWitness.lean (shear_base_marginal_unchanged, the frozen base); RecordLayer/JointFlowTransfer.lean (IsJointLift.moment_marginal_unchanged, the other horn); RecordLayer/PiecewiseHamiltonian.lean (dropping C¹).

Coordinate expansion of a chart functional

theorem CSD.SigmaLayer.clm_apply_eq_sum {n : ℕ} (L : Chart n →L[ℝ] ℝ) (Δ : Chart n) : L Δ = ∑ i : Fin n, Δ.1 i * L (posDir i) + ∑ i : Fin n, Δ.2 i * L (momDir i)

Any chart covector is determined by its values on the coordinate directions: the gradient expansion L Δ = Σᵢ Δxᵢ · L(∂xᵢ) + Σᵢ Δyᵢ · L(∂yᵢ).

theorem CSD.SigmaLayer.fderiv_apply_eq_sum {n : ℕ} (H : Chart n → ℝ) (z Δ : Chart n) : (fderiv ℝ H z) Δ = ∑ i : Fin n, Δ.1 i * dPos H z i + ∑ i : Fin n, Δ.2 i * dMom H z i

The gradient expansion for fderiv, in the corpus's dPos/dMom notation.

The frozen base

def CSD.SigmaLayer.BaseFrozen {n : ℕ} (H : Chart n → ℝ) (S : Finset (Fin n)) : Prop

(c′) The base is pointwise frozen. Both partials of the generator vanish on the base block S, which is exactly "the base components of hamiltonianField H are identically zero": ẋ_S = ∂_y H = 0 and ẏ_S = −∂_x H = 0.

Equations

• CSD.SigmaLayer.BaseFrozen H S = ∀ (z : CSD.SigmaLayer.Chart n), ∀ i ∈ S, CSD.SigmaLayer.dPos H z i = 0 ∧ CSD.SigmaLayer.dMom H z i = 0

theorem CSD.SigmaLayer.hamiltonianField_base_eq_zero {n : ℕ} {H : Chart n → ℝ} {S : Finset (Fin n)} (h : BaseFrozen H S) (z : Chart n) (i : Fin n) (hi : i ∈ S) : (hamiltonianField H z).1 i = 0 ∧ (hamiltonianField H z).2 i = 0

The frozen base is literally the vanishing of the field's base components.

def CSD.SigmaLayer.AgreeOff {n : ℕ} (S : Finset (Fin n)) (z z' : Chart n) : Prop

Two chart points agree off S: they share every coordinate outside the base block.

Equations

• CSD.SigmaLayer.AgreeOff S z z' = ∀ i ∉ S, z.1 i = z'.1 i ∧ z.2 i = z'.2 i

theorem CSD.SigmaLayer.fderiv_apply_eq_zero_of_baseFrozen {n : ℕ} {H : Chart n → ℝ} {S : Finset (Fin n)} (h : BaseFrozen H S) (z Δ : Chart n) (hΔ : ∀ i ∉ S, Δ.1 i = 0 ∧ Δ.2 i = 0) : (fderiv ℝ H z) Δ = 0

A frozen generator annihilates every direction supported in S.

★★ The obstruction

theorem CSD.SigmaLayer.baseConstant_of_baseFrozen {n : ℕ} {H : Chart n → ℝ} {S : Finset (Fin n)} (hdiff : Differentiable ℝ H) (h : BaseFrozen H S) {z z' : Chart n} (hagree : AgreeOff S z z') : H z = H z'

★★ A frozen base forces a base-constant generator. If H is differentiable (a) and base-frozen (c′), it takes the same value at any two points agreeing off the base block.

The proof is the segment argument: the difference of two such points is supported in S, a frozen generator annihilates every such direction, so H is constant along the segment.

theorem CSD.SigmaLayer.not_baseFrozen_of_outcomeDependent {n : ℕ} {H : Chart n → ℝ} {S : Finset (Fin n)} (hdiff : Differentiable ℝ H) {z z' : Chart n} (hagree : AgreeOff S z z') (hne : H z ≠ H z') : ¬BaseFrozen H S

★★ The contrapositive, in the shape the obstruction is used. A generator that distinguishes two base sectors sharing their fibre data — which is what "the interaction depends on the outcome index" means — is not base-frozen. Its flow must move the base.

This is the price of the frozen-base design, stated as a theorem: exact outcome-dependence and a pointwise-frozen base are incompatible for a C¹ generator on a product chart.