AdjointResponse

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The adjoint response identity

Source: ABK26. The proof of l.Dh.bound needs the energy of the adjoint half w* = ½ v(·, □₀, p, -q; aᵗ) expressed through the primal response functional. In the coarse-matrix coordinates the two response functionals differ only by the sign of the κ term, so

J(U, aᵗ, p, -q) = J(U, a, p, q) + 2 p · q .

Both sides are unconditional: the canonical coarse-matrix formula responseJ_eq_coarseMatrices_formula_canonical and the adjoint formula ResponseMagicIdentitiesTheory.adjoint_quadratic hold at every Chapter 2 domain and coefficient.

The identity is what converts the adjoint energy (P · 𝐀 P)/2 - 2J of the source proof into the frozen budget shape √J + √|p · q|.

Sign bookkeeping for the quadratic form

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.matVecMul_neg {d : ℕ} (M : HCPolySupport.Mat d) (v : HCPolySupport.Vec d) : HCPolySupport.matVecMul M (-v) = -HCPolySupport.matVecMul M v

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecDot_neg_neg {d : ℕ} (v w : HCPolySupport.Vec d) : HCPolySupport.vecDot (-v) (-w) = HCPolySupport.vecDot v w

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.vecDot_neg_right {d : ℕ} (v w : HCPolySupport.Vec d) : HCPolySupport.vecDot v (-w) = -HCPolySupport.vecDot v w

The adjoint response identity

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.responseJ_transpose_neg_right {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U a.transpose p (-q) = HCPolySupport.Book.Ch02.responseJ U a p q + 2 * HCPolySupport.vecDot p q

Adjoint response identity. Flipping the coefficient to its transpose and the second loading to its negative shifts the response functional by 2 p · q.