Stage 3: exact real-exponent anchor norming vector

The source coordinate formula is identified with the normalized duality map, then its two norming identities are derived without adding them as hypotheses.

theorem O3.Stage3Anchor.conjugateExponent_conjugateExponent {p : ℝ} (hp : 1 < p) : conjugateExponent (conjugateExponent p) = p

theorem O3.Stage3Anchor.p_mul_conjugateExponent_sub_one {p : ℝ} (hp : 1 < p) : p * (conjugateExponent p - 1) = conjugateExponent p

theorem O3.Stage3Anchor.sign_mul_abs_rpow_sub_one {q a : ℝ} (hq : 1 < q) : ↑(SignType.sign a) * |a| ^ (q - 1) = |a| ^ (q - 2) * a

Coordinate identity behind the source sign-power formula. It covers a zero coordinate even when q - 2 is negative.

theorem O3.Stage3Anchor.inv_rpow_anchor_coefficient {q n : ℝ} (hn : 0 < n) : 1 / n ^ (q - 1) = n⁻¹ * n ^ (2 - q)

theorem O3.Stage3Anchor.anchorNormingVector_eq_inv_smul_dualityMap {q : ℝ} (hq : 1 < q) {d : ℕ} (g : Vec d) (hg : g ≠ 0) : anchorNormingVector q g = (lpNorm q g)⁻¹ • dualityMap q g

The explicit source vector is exactly J_q(g) / ||g||_q.

theorem O3.Stage3Anchor.anchorNormingVector_lpNorm {p : ℝ} (hp : 1 < p) {d : ℕ} (g : Vec d) (hg : g ≠ 0) : lpNorm p (anchorNormingVector (conjugateExponent p) g) = 1

First frozen norming identity, for genuine real conjugate exponents.

theorem O3.Stage3Anchor.pairing_anchorNormingVector {p : ℝ} (hp : 1 < p) {d : ℕ} (g : Vec d) (hg : g ≠ 0) : pairing g (anchorNormingVector (conjugateExponent p) g) = lpNorm (conjugateExponent p) g

Second frozen norming identity, with the exact source pairing order.