P5-attainment: the linear price is attained — "costs at most" becomes "costs exactly"

Category: CV (continuous variables — the attainment half of P5; eft-pillars-plan.md P5).

Glossary: https://glossary.constraintsurfacedynamics.com/interaction-price/ Plain-language, CSD-role and formal statements of the interaction price, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

CV-9 priced locality violation from above: switching on a coupling λ moves an S-supported observable at most 2·|τ|·|λ|·C·‖A‖ from the S-supported subalgebra (heisenberg_interactingU_near_supported). Whether that linear price is attained was CV-9's declared boundary. This module closes it with a matching linear lower bound on a witness. Scoped first in specs/price-attainment-plan.md.

• norm_commutator_le_of_commute — the commutator functional: any S-supported B commutes with a disjointly supported probe (CV-2b), so ‖[X,P]‖ ≤ 2·‖X−B‖·‖P‖ — a commutator against a unit probe bounds the distance to the whole S-supported subalgebra from below.
• The K = N = 2 witness: priceObs = modeOp 0 (single 0 1), priceProbe = modeOp 1 (single 0 1), pair coupling priceV c = [c₀ = 1 ∧ c₁ = 1]. The interacting drive is a diagonal phase, so the commutator entry at (config 00, config 11) is computable exactly: the free phases cancel (energy is mode-additive), the coupling phases do not (the coupling reads both modes), and the entry has modulus 2·|sin(τλ/2)| (comm_entry_norm).
• ★★ price_lower_bound — for EVERY {0}-supported B: |sin(τλ/2)| ≤ ‖heisenberg (interactingU 2 2 τ λ priceV) priceObs − B‖. No supported operator is closer than the sine of the accumulated coupling phase.
• ★★ price_linear_attained — the sandwich (0 ≤ τλ ≤ π, Jordan): τλ/π ≤ dist(X, S-supported) ≤ 2·τλ. The price of locality violation is linear in the coupling on both sides: CV-9's "costs at most" is now "costs exactly", up to the constant gap [1/π, 2].

⚠️ Honest scope: attainment is an existence claim, and a witness is exactly what it needs — one drive, one coupling shape, K = N = 2. No claim that every drive saturates the bound, and the constants are not matched (on this witness the distance is 2|sin(τλ/2)|-shaped; the exact-distance identification is not claimed here).

References

specs/price-attainment-plan.md (scoping); specs/eft-pillars-plan.md (P5); specs/future-work.md; CV/InteractionPrice.lean (CV-9, the upper bound); CV/DynamicalLocality.lean (heisenberg_phaseDiagU_apply); CV/ModeLocality.lean (modeOp, commute_of_disjointSupport); CV/PowerCounting.lean (l2_opNorm_modeOp_le); Mathlib/Analysis/Matrix/L2OpNormEntry.lean (norm_entry_le_l2_opNorm).

The commutator functional: distance from below

theorem CSD.CV.norm_commutator_le_of_commute {K N : ℕ} [NeZero N] {X B P : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hBP : B * P = P * B) : ‖X * P - P * X‖ ≤ 2 * ‖X - B‖ * ‖P‖

The commutator functional: if B commutes with the probe P, the commutator of X with P is controlled by the distance from X to B. In use, B ranges over an S-supported subalgebra and P is a disjointly supported probe, so this bounds the distance to the WHOLE subalgebra from below by a single computable commutator.

Norm bricks

theorem CSD.CV.l2_opNorm_single_le_one : ‖Matrix.single 0 1 1‖ ≤ 1

The unit basis matrix has operator norm at most one.

theorem CSD.CV.norm_one_sub_exp_I_mul (θ : ℝ) : ‖1 - Complex.exp (Complex.I * ↑θ)‖ = 2 * |Real.sin (θ / 2)|

‖1 − e^{iθ}‖ = 2·|sin(θ/2)| — the exact chord length.

theorem CSD.CV.star_exp_neg_I_mul_real (x : ℝ) : star (Complex.exp (-(Complex.I * ↑x))) = Complex.exp (Complex.I * ↑x)

The conjugate of a diagonal phase is the inverse phase.

The witness

noncomputable def CSD.CV.priceV : FieldConfig 2 2 → ℝ

The witness pair coupling: v(c) = 1 exactly when both modes sit at level 1. Bounded by 1.

Equations

• CSD.CV.priceV c = if c 0 = 1 ∧ c 1 = 1 then 1 else 0

theorem CSD.CV.priceV_abs_le_one (c : FieldConfig 2 2) : |priceV c| ≤ 1

noncomputable def CSD.CV.priceObs : Matrix (FieldConfig 2 2) (FieldConfig 2 2) ℂ

The witness observable: the unit single-mode matrix at mode 0.

Equations

• CSD.CV.priceObs = CSD.CV.modeOp 0 (Matrix.single 0 1 1)

noncomputable def CSD.CV.priceProbe : Matrix (FieldConfig 2 2) (FieldConfig 2 2) ℂ

The probe: the unit single-mode matrix at mode 1.

Equations

• CSD.CV.priceProbe = CSD.CV.modeOp 1 (Matrix.single 0 1 1)

theorem CSD.CV.priceObs_supportedOn : SupportedOn {0} priceObs

theorem CSD.CV.priceProbe_supportedOn : SupportedOn {1} priceProbe

theorem CSD.CV.priceObs_norm_le_one : ‖priceObs‖ ≤ 1

theorem CSD.CV.priceProbe_norm_le_one : ‖priceProbe‖ ≤ 1

Entry evaluations: where each factor lives

theorem CSD.CV.priceObs_apply_c00 (e : FieldConfig 2 2) : priceObs ![0, 0] e = if e = ![1, 0] then 1 else 0

The witness observable out of config (0,0): only into config (1,0).

theorem CSD.CV.priceObs_apply_c11 (e : FieldConfig 2 2) : priceObs e ![1, 1] = if e = ![0, 1] then 1 else 0

The witness observable into config (1,1): only out of config (0,1).

theorem CSD.CV.priceProbe_apply_c11 (e : FieldConfig 2 2) : priceProbe e ![1, 1] = if e = ![1, 0] then 1 else 0

The probe into config (1,1): only out of config (1,0).

theorem CSD.CV.priceProbe_apply_c00 (e : FieldConfig 2 2) : priceProbe ![0, 0] e = if e = ![0, 1] then 1 else 0

The probe out of config (0,0): only into config (0,1).

The phase bookkeeping

noncomputable def CSD.CV.priceF (τ lam : ℝ) : FieldConfig 2 2 → ℝ

The diagonal phase function of the witness drive.

Equations

• CSD.CV.priceF τ lam c = τ * (CSD.CV.fieldEnergy c + lam * CSD.CV.priceV c)

theorem CSD.CV.interactingU_priceV (τ lam : ℝ) : interactingU 2 2 τ lam priceV = phaseDiagU (priceF τ lam)

theorem CSD.CV.priceF_cross (τ lam : ℝ) : priceF τ lam ![0, 1] - priceF τ lam ![1, 1] - (priceF τ lam ![0, 0] - priceF τ lam ![1, 0]) = -(τ * lam)

The cross-difference of the phases is exactly the coupling phase: the free (energy) parts cancel because energy is mode-additive, and the coupling survives because it reads both modes.

The commutator entry, exactly

theorem CSD.CV.XP_entry (τ lam : ℝ) : (heisenberg (interactingU 2 2 τ lam priceV) priceObs * priceProbe) ![0, 0] ![1, 1] = Complex.exp (Complex.I * ↑(priceF τ lam ![0, 0])) * Complex.exp (-(Complex.I * ↑(priceF τ lam ![1, 0])))

The (config 00, config 11) entry of X·P collapses to the single path through config (1,0).

theorem CSD.CV.PX_entry (τ lam : ℝ) : (priceProbe * heisenberg (interactingU 2 2 τ lam priceV) priceObs) ![0, 0] ![1, 1] = Complex.exp (Complex.I * ↑(priceF τ lam ![0, 1])) * Complex.exp (-(Complex.I * ↑(priceF τ lam ![1, 1])))

The (config 00, config 11) entry of P·X collapses to the single path through config (0,1).

theorem CSD.CV.comm_entry_norm (τ lam : ℝ) : ‖(heisenberg (interactingU 2 2 τ lam priceV) priceObs * priceProbe - priceProbe * heisenberg (interactingU 2 2 τ lam priceV) priceObs) ![0, 0] ![1, 1]‖ = 2 * |Real.sin (τ * lam / 2)|

★ The commutator entry has modulus 2·|sin(τλ/2)|, exactly. The free phases cancel between the two paths; the coupling phase does not.

The attainment theorems

theorem CSD.CV.price_lower_bound (τ lam : ℝ) {B : Matrix (FieldConfig 2 2) (FieldConfig 2 2) ℂ} (hB : SupportedOn {0} B) : |Real.sin (τ * lam / 2)| ≤ ‖heisenberg (interactingU 2 2 τ lam priceV) priceObs - B‖

★★ The linear price is attained from below: EVERY {0}-supported operator is at least |sin(τλ/2)| away from the interacting Heisenberg observable. CV-9's declared attainment boundary closes on this witness.

theorem CSD.CV.price_linear_attained (τ lam : ℝ) (h0 : 0 ≤ τ * lam) (hπ : τ * lam ≤ Real.pi) : (∀ (B : Matrix (FieldConfig 2 2) (FieldConfig 2 2) ℂ), SupportedOn {0} B → τ * lam / Real.pi ≤ ‖heisenberg (interactingU 2 2 τ lam priceV) priceObs - B‖) ∧ ∃ (B : Matrix (FieldConfig 2 2) (FieldConfig 2 2) ℂ), SupportedOn {0} B ∧ ‖heisenberg (interactingU 2 2 τ lam priceV) priceObs - B‖ ≤ 2 * (τ * lam)

★★ The sandwich — the price is linear on both sides. For 0 ≤ τλ ≤ π: every {0}-supported operator is at least τλ/π away (Jordan's inequality on the exact sine), and some {0}-supported operator is within 2τλ (CV-9's upper bound at C = 1, ‖A‖ ≤ 1). "Costs at most" is now "costs exactly", up to the constant gap [1/π, 2].