research(cauchy-schwarz-oq-02-oq-03): S1 — complex polarization identity (Mathlib convention) + physics-convention bridge (build pending)

[rjwalters]

Summary

Session 1 — first proof of the complex polarization identity in Lean for slug cauchy-schwarz-oq-02-oq-03. New gallery entry; 12 theorems, 0 sorries, 0 axioms; 218 lines.

The slug's stated formula is in physics convention (linear in first argument):
$$\langle f, g \rangle = \tfrac{1}{4}\bigl(|f+g|^2 - |f-g|^2 + i|f+ig|^2 - i|f-ig|^2\bigr).$$

Mathlib uses math convention (sesquilinear in first argument: $\langle c!\cdot!x, y\rangle = \overline{c},\langle x, y\rangle$, linear in second). With Mathlib's convention, the same physics formula computes
$\langle y, x\rangle = \overline{\langle x, y\rangle}$, NOT $\langle x, y\rangle$. This file proves both formulas and the bridge.

Files

• proofs/Proofs/CauchySchwarzOQ02OQ03.lean — 218 lines, 12 theorems (full list below).
• proofs/Proofs.lean — import the new module (1 line added between OQ02OQ02 and OQ03).
• src/data/proofs/cauchy-schwarz-oq-02-oq-03/{meta.json,index.ts,annotations.json} — gallery entry; meta.json declares status verified, badge mathlib, lineCount 218, theoremCount 12, sorries 0, axiomCount 0; 7-section narrative with explicit convention-mismatch discussion.
• research/problems/cauchy-schwarz-oq-02-oq-03/{problem,state,knowledge}.md — research dir.
• src/data/research/problems/cauchy-schwarz-oq-02-oq-03.json — phase NEW→ACT, iteration 1→2, 12 builtItems, 4 insights.

Theorems (in dependency order)

1. norm_add_sq_complex — restate norm_add_sq for ℂ.
2. norm_sub_sq_complex — derive via $y \mapsto -y$ + inner_neg_right + norm_neg.
3. norm_add_sq_sub_norm_sub_sq_eq_four_re — $|x+y|^2 - |x-y|^2 = 4,\mathrm{re}\langle x,y\rangle$.
4. norm_smul_I_sq — $|I!\cdot!y|^2 = |y|^2$.
5. re_I_mul — $\mathrm{re}(I \cdot z) = -\mathrm{im}(z)$.
6. norm_add_smul_I_sq_sub_eq_neg_four_im — $|x+iy|^2 - |x-iy|^2 = -4,\mathrm{im}\langle x,y\rangle$ (sign flip from physics).
7. re_inner_eq_quarter_norm_diff — $\mathrm{re}\langle x,y\rangle = (|x+y|^2 - |x-y|^2)/4$.
8. im_inner_eq_quarter_norm_diff — $\mathrm{im}\langle x,y\rangle = (|x-iy|^2 - |x+iy|^2)/4$.
9. complex_polarization_mathlib (MAIN) — $\langle x,y\rangle_{\mathbb{C}} = (|x+y|^2 - |x-y|^2 + i(|x-iy|^2 - |x+iy|^2))/4$.
10. physics_polarization_eq_inner_swap (BRIDGE) — slug's physics formula $= \langle y, x\rangle_{\mathbb{C}}$.
11. physics_polarization_eq_conj — same restated as $= \overline{\langle x, y\rangle_{\mathbb{C}}}$.
12. mathlib_minus_physics — $\langle x,y\rangle - \langle y,x\rangle = 2i \cdot \mathrm{im}\langle x,y\rangle$.

Why this is real progress

• Convention-mismatch observation: stating the slug's formula uncritically gives the wrong inner product in Mathlib. The bridge theorems (physics_polarization_eq_inner_swap, physics_polarization_eq_conj) make the conversion mechanical for anyone porting from physics literature.
• Per-component recovery: re_inner_eq_quarter_norm_diff and im_inner_eq_quarter_norm_diff cleanly expose the real and imaginary parts as quarter-norms, useful for downstream applications (operator polarization, phase retrieval).
• Generalizes the parent OQ-02 real polarization: the real case is the imaginary-correction-vanishing specialization. (Future: unify via RCLike.)

Proof strategy (one paragraph)

Decompose $\langle x, y\rangle_{\mathbb{C}} = (\mathrm{re}\langle x,y\rangle : \mathbb{C}) + (\mathrm{im}\langle x,y\rangle : \mathbb{C}) \cdot i$ via Complex.re_add_im, then substitute the per-component formulas. The real part follows from the standard squared-norm expansion norm_add_sq (and the negation-derived norm_sub_sq_complex). For the imaginary part, replace $y$ by $i!\cdot!y$ in norm_add_sq and use $\langle x, iy\rangle = i,\langle x,y\rangle$ (inner_smul_right) plus $\mathrm{re}(I\cdot z) = -\mathrm{im}(z)$. Each subgoal closes with linarith or push_cast; ring. The convention-mismatch theorem physics_polarization_eq_inner_swap uses inner_conj_symm (which says $\langle y, x\rangle = \overline{\langle x, y\rangle}$) plus a small Complex.ext to handle the conjugate decomposition.

Build status: pending

The worktree's proofs/.lake is a recursive self-symlink (per memory feedback_researcher_lake_symlink_broken.md), forcing every Docker build to fresh-clone Mathlib (~10–15 min) + cache get (~10 min) ≈ ~45 min total. Following PR #16936's pattern (and other recent build-pending session-1 PRs), this PR is opened as draft.

The 12 theorems use only well-established Mathlib idioms verified from sibling files in the same directory:

• norm_add_sq (𝕜 := 𝕜) — used at CauchySchwarzOQ01OQ02.lean:145, CauchySchwarzOQ01.lean:121, CauchySchwarzOQ01OQ01OQ01.lean:154.
• inner_smul_right, inner_neg_right, inner_conj_symm — used throughout the OQ01* files.
• Complex.re_add_im — long-standing API in Mathlib.Data.Complex.Basic.

Risk factors and remediation if the build fails:

1. linarith in norm_sub_sq_complex after sub_eq_add_neg rewrite — fallback: omega or explicit rewriting.
2. The small simp set inside physics_polarization_eq_inner_swap for Complex.conj_re/im decomposition — well-established lemmas.
3. Complex.re_add_im exact name in Mathlib 4.26 — long-standing API, low risk.

Test plan

• Re-run ./proofs/scripts/docker-build.sh Proofs.CauchySchwarzOQ02OQ03 from a worktree with warm Mathlib cache.
• If build passes, mark PR ready-for-review.
• Confirm 12 #check directives at end of file resolve.
• Verify gallery entry renders in dev server.

Related

• Parent: cauchy-schwarz-oq-02 real polarization identity (CauchySchwarzOQ02.lean polarization_identity).
• Sibling: cauchy-schwarz-oq-02-oq-02 Bessel's inequality (same inner product framework).
• Memory note: feedback_researcher_lake_symlink_broken.md (build cost).
• Pattern: PR research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S5 — Easton non-examples + lt_apply corollary #16936 (cantor-diagonalization-oq-01-oq-01-oq-02-oq-01 S5, build pending draft).

🤖 Generated with Claude Code

[rjwalters]

Closing as abandoned: too stale.

This PR was opened 2026-05-08 and has not been updated in 16 days. It has been superseded by:

• PR research(cauchy-schwarz-oq-02-oq-03): S1 OBSERVE — complex polarization identity scaffold #18244 (merged 2026-05-12): research(cauchy-schwarz-oq-02-oq-03): S1 OBSERVE — complex polarization identity scaffold — carries the same S1 polarization scaffold work this PR proposed.

Additional evidence of supersession:

• The Lean file proofs/Proofs/CauchySchwarzOQ02OQ03.lean proposed here does not exist on main (different layout chosen).
• The gallery entry src/data/proofs/cauchy-schwarz-oq-02-oq-03/ proposed here does not exist on main.
• The repo HEAD has advanced ~3,000+ PRs past this one; rebasing 1,100 additions against substantial cauchy-schwarz restructuring (research(cauchy-schwarz-oq-02-oq-03): S1 OBSERVE — complex polarization identity scaffold #18244, Enrich Lp Riesz Sigma-Finite (cauchy-schwarz-integral-oq-...-incomplete-01): add 8 cross-references #18306, fix(meta): batch sync leanFile.lineCount drift in 41 entries #19622, fix(meta): batch sync CauchySchwarzIntegralOQ01OQ01OQ02OQ01OQ01.lean leanFiles in 33 cauchy-schwarz siblings #19797, fix(meta): batch sync CauchySchwarz.lean leanFiles lineCount 232→231 in 14 cauchy-schwarz siblings #20101, fix(meta): batch sync Derangements.lean leanFiles lineCount 228→227 in 8 derangements siblings #20106) would be infeasible.

If any portion of this work is still needed, please open a fresh PR against current main.