CV-20: carrier persistence priced by locality (H7, level 1)

Category: 3-Local (CV track; CSD-free construction).

The first statements in which a record carrier's stability is priced by field locality rather than posited (specs/BACKLOG.md H7). Framing constraint, binding per the row: these are theorems about carriers — the present-tense evolution of readout observables — never about "the past changing"; the record event is trajectory-indexed and invariant by construction (the level-2 lemmas in Empirical/CSD/QuantumChaos/CarrierPersistence.lean), and information is conserved outright (perturbed_overlap_invariant below — every global overlap is exact at every period, so what a perturbation does to a carrier is relocation, never loss).

• ★ heisenberg_perturbed_pow_eq — exactness in the cone-complement: perturbing the interacting drive by an arbitrary unitary W supported on R leaves the Heisenberg evolution of every readout supported on Q exactly unchanged for n periods, provided the coupling graph's n-ball of Q has not reached R. Not a bound — an equality.
• ★ heisenberg_diagonal_pow_eq — einselection of the configuration basis: a diagonal readout is exactly invariant under the entire diagonal-phase drive family, at every period and every coupling. In this model the pointer basis is the configuration basis, and carriers written in it are eternally intact under every diagonal drive — degradation can only enter through genuinely non-diagonal perturbations, which is what W above and below is for.
• norm_unitary_pow_sub_pow_le — the telescoping bound ‖Xⁿ − Yⁿ‖ ≤ n·‖X − Y‖ for unitary steps (each factor is an isometry).
• ★ heisenberg_perturbed_pow_dist_le — the bounded half: with no geometric hypothesis at all, n perturbed periods move a readout by at most 2n·‖W − 1‖·‖B‖ — the Duhamel rate of heisenberg_dist_le.
• ★★ carrier_persistence_window — the window form, the H7 level-1 headline: if the perturbation stays outside the readout's m-ball, the deviation after n ≥ m periods is at most 2·(n − m)·‖W − 1‖·‖B‖ — zero until the cone arrives, the Duhamel rate only after. Locality itself supplies the isolation window; ε is derived, not posited.

Scope

Finite cutoff throughout (K modes, N levels); the base drive is the kicked diagonal-phase family (graphInteractingU), the perturbation W an arbitrary unitary with stated support. The ontic-level lift (feeding the derived rate into recordFlip/recordIntact_compl_measure_le) is recorded in the H7 row as the remaining level; the operational-fixedness clause (d) is the finite-arena csd_repeatability_same, cited at level 2.

(c1) Exactness in the cone-complement

theorem CSD.CV.heisenberg_perturbed_pow_eq {K N : ℕ} {Q R : Finset (Fin K)} (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) {W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} (hW : SupportedOn R ↑W) {B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hB : SupportedOn Q B) (n : ℕ) (hdisj : Disjoint (graphBall E Q n) R) : heisenberg ((graphInteractingU K N τ lam E g * W) ^ n) B = heisenberg (graphInteractingU K N τ lam E g ^ n) B

★ Exactness in the cone-complement. Perturbing each period of the interacting drive by an arbitrary unitary W supported on R leaves the Heisenberg evolution of a Q-supported readout exactly unchanged for n periods, provided the coupling graph's n-ball of Q is still disjoint from R: the readout's cone has not reached the perturbation, so every W-conjugation acts trivially on the evolved readout (heisenberg_eq_of_disjoint).

(c1′) Einselection of the configuration basis

theorem CSD.CV.heisenberg_diagonal_of_diagonal {K N : ℕ} {U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} {u : FieldConfig K N → ℂ} (hU : ↑U = Matrix.diagonal u) (b : FieldConfig K N → ℂ) : heisenberg U (Matrix.diagonal b) = Matrix.diagonal b

Conjugation by a diagonal unitary fixes every diagonal observable.

theorem CSD.CV.heisenberg_diagonal_pow_eq {K N : ℕ} (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) (n : ℕ) (b : FieldConfig K N → ℂ) : heisenberg (graphInteractingU K N τ lam E g ^ n) (Matrix.diagonal b) = Matrix.diagonal b

★ Einselection of the configuration basis: a diagonal readout is exactly invariant under the whole diagonal-phase drive family — every coupling graph, every strength, every period count. Carriers written in the pointer (configuration) basis are eternally intact under every diagonal drive; only genuinely non-diagonal perturbations can move them.

(c2) The bounded half

theorem CSD.CV.norm_unitary_pow_sub_pow_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (X Y : ↥(Matrix.unitaryGroup ι ℂ)) (n : ℕ) : ‖↑(X ^ n) - ↑(Y ^ n)‖ ≤ ↑n * ‖↑X - ↑Y‖

Iterated unitary steps separate at most linearly: ‖Xⁿ − Yⁿ‖ ≤ n·‖X − Y‖ (one fresh X − Y per period, the other factors isometries).

theorem CSD.CV.norm_mul_sub_self_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (U W : ↥(Matrix.unitaryGroup ι ℂ)) : ‖↑(U * W) - ↑U‖ ≤ ‖↑W - 1‖

The per-period perturbation distance: ‖UW − U‖ ≤ ‖W − 1‖.

theorem CSD.CV.norm_heisenberg_le {K N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : ‖heisenberg U B‖ ≤ ‖B‖

Conjugation contracts: ‖heisenberg U B‖ ≤ ‖B‖.

theorem CSD.CV.heisenberg_perturbed_pow_dist_le {K N : ℕ} [NeZero N] (U W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (n : ℕ) : ‖heisenberg ((U * W) ^ n) B - heisenberg (U ^ n) B‖ ≤ 2 * ↑n * ‖↑W - 1‖ * ‖B‖

★ The bounded half: with no geometric hypothesis, n perturbed periods move any readout by at most 2n·‖W − 1‖·‖B‖ — the Duhamel rate of heisenberg_dist_le, telescoped.

★★ The window form — the H7 level-1 headline

theorem CSD.CV.carrier_persistence_window {K N : ℕ} [NeZero N] {Q R : Finset (Fin K)} (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) {W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} (hW : SupportedOn R ↑W) {B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hB : SupportedOn Q B) {m n : ℕ} (hmn : m ≤ n) (hdisj : Disjoint (graphBall E Q m) R) : ‖heisenberg ((graphInteractingU K N τ lam E g * W) ^ n) B - heisenberg (graphInteractingU K N τ lam E g ^ n) B‖ ≤ 2 * ↑(n - m) * ‖↑W - 1‖ * ‖B‖

★★ Carrier persistence, the window form. A readout supported on Q, evolved under the interacting drive perturbed each period by an arbitrary unitary W supported on R: if R is outside the readout's m-ball, the deviation after n ≥ m periods is at most 2·(n − m)·‖W − 1‖·‖B‖ — exactly zero until the cone arrives, the Duhamel rate only after. Locality supplies the isolation window; the rate is derived, not posited.

(b) Information conservation, instantiated

theorem CSD.CV.perturbed_overlap_invariant {K N : ℕ} (U W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (n : ℕ) (ψ φ : EuclideanSpace ℂ (FieldConfig K N)) : inner ℂ (((QuantumChaos.FloquetEvolution.ofUnitaryMatrix (U * W)).iterate n) ψ) (((QuantumChaos.FloquetEvolution.ofUnitaryMatrix (U * W)).iterate n) φ) = inner ℂ ψ φ

Every global overlap is exactly conserved under the perturbed drive, at every period: what a perturbation does to a carrier is relocation, never loss. Instantiates the Floquet-interface conservation law at the perturbed CV drive.