Full trace metric and acceleration
Abstract
The complete symmetric inverse metric and actual spectral acceleration identity.
Theorem 1.1 (Affine regularization).
Lean statement: D5/S3/Quantum/NormCompression/FinitePowerMetric.regularizedTable_affine
Proof. Machine-checked in Lean as D5/S3/Quantum/NormCompression/FinitePowerMetric.regularizedTable_affine (✓ std3). ∎
Source. Repository-derived.
Commentary.
Regularization commutes with every affine combination whose coefficients sum to one.
The private metric suppliers retain both diagonal coordinates and the off diagonal direction. They are consumed directly by full cone concavity and by the fixed support radial Hessian kernel.