From 0b3363840081baee55881dbfdf0ae606f57c594d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Thu, 8 Oct 2026 02:29:35 +0000 Subject: [PATCH 1/2] reviews: add W3 SIDE24 source-only proposal (unregistered, unreviewed draft) Co-authored-by: Dylan Roy --- .../README.md | 129 ++++++ .../W3Scratch/D2SchurLinks.lean | 387 ++++++++++++++++++ .../W3Scratch/Side24Law.lean | 286 +++++++++++++ .../W3Scratch/Side24Poisson.lean | 337 +++++++++++++++ 4 files changed, 1139 insertions(+) create mode 100644 reviews/w3_side24_source_proposal_20261008/README.md create mode 100644 reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean create mode 100644 reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean create mode 100644 reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean diff --git a/reviews/w3_side24_source_proposal_20261008/README.md b/reviews/w3_side24_source_proposal_20261008/README.md new file mode 100644 index 000000000..3d0ab1113 --- /dev/null +++ b/reviews/w3_side24_source_proposal_20261008/README.md @@ -0,0 +1,129 @@ +# W3 SIDE24 source proposal (unregistered, unreviewed): SCRATCH / ENGINEERING ONLY + +credit 0; sci NONE; eng≠discharge; no flags; OBL OPEN + +**A Lean lemma ≠ alignment acceptance ≠ discharge.** + +## Boundary + +- This directory is an **unregistered, unreviewed, source-only proposal**. Its only purpose is to make the complete proof bodies public so that a separate nonauthor source/alignment reader can read them. +- It was published under option **B only** of the decision [main#229 6050818585](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050818585), routed by [6050894775](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050894775). +- That decision does **not** accept R1–R4, the spectral-law interpretation, any theorem or alignment claim, or option A's formal registration. Nothing here changes that. +- Nothing under `formal/`, no lakefile, manifest, root import, test, workflow, GRAPH or STATUS file is touched. These modules are **not** part of `ResearchFormalCoreR1`, are **not** built by any workflow, and ordinary PR CI does **not** certify them. +- No status field (lemma_closed, prizes_solved, discharges_OBL_H5_JETMOD, certified_C_H, freeze, inventable_attempt_accepted, alignment) is changed or proposed to change. OBL OPEN. +- All evidence below is the author's own, box-local, and **UNVERIFIED** by any nonauthor. + +## Author and exposure + +- Author: Grok Bot agent 13 (Grok Bot support agent; non-Claude, nonauthor lane), tasks W3d–W3g, Oct 7 2026 (CT). +- The author wrote all three `.lean` files and has read the sources cited below. +- Reports: W3d [6050271678](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050271678), W3e [6050351089](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050351089), W3f [6050458079](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050458079), W3g [6050559869](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050559869). CoS decision request: [6050565322](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050565322). + +## Identities + +### Files (bytes and namespaces unchanged from the reported W3e/W3f/W3g sources) + +| Path (under this directory) | sha256 | bytes | lines | namespace | task | +|---|---|---|---|---|---| +| `W3Scratch/D2SchurLinks.lean` | `06b28be4725a72f7915a7fe3077f2d562c809c63c4a5acbd1c79bcc923d9dbda` | 19449 | 387 | `W3Scratch` | W3d + W3e | +| `W3Scratch/Side24Law.lean` | `8678ddd4d58e123d4e0b1bb829a56d00eb7c281c95ba0eef45efa3086d7756d7` | 14497 | 286 | `W3Scratch.Side24` | W3f | +| `W3Scratch/Side24Poisson.lean` | `47b65188977a251ebd8ae92d14e4b1109b6695b5e0daf48d6f50ee26554fcb86` | 18074 | 337 | `W3Scratch.Side24` | W3g | + +All three end in a single LF; none contains CR. + +### Base and dependencies + +- Math- base: main `7014efec8fb68cc926350caa8fa65dcd296f7f63`. +- The `formal/` tree is `d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14`, identical at `9fd261135b41daf1e377f9ef2db193fee6ec36be` (W3d–W3f base), `8d70baa798c61d3c259285fcc93b3dfc2415793c` (W3g base) and `7014efec`. +- Read-only input: `formal/ResearchFormalCoreR1/D2Schur.lean`, blob `b95460c0d263a32ea274b347079cca6aaab3d2e9`. +- Toolchain: `leanprover/lean4:v4.34.1` (from `formal/lean-toolchain`). +- mathlib `d13f23b723b8a846827a245b89c10fc7d3f11612` (from `formal/lake-manifest.json`; also batteries `f2effa3d`, aesop `355695d5`, Qq `6a489d9a`, proofwidgets `106ff4fa`, plausible `118aa17e`, LeanSearchClient `ddf04cf3`, importGraph `e928b725`, Cli `e92c9f15`). + +### Imports + +- `D2SchurLinks.lean`: `ResearchFormalCoreR1.D2Schur`, `Mathlib.LinearAlgebra.Matrix.Determinant.Basic`, `Mathlib.LinearAlgebra.Matrix.Notation`, `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse`. +- `Side24Law.lean`: `W3Scratch.D2SchurLinks`, `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable`, `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation`, `Mathlib.RingTheory.Polynomial.Hermite.Gaussian`. +- `Side24Poisson.lean`: `W3Scratch.Side24Law`. + +### Sources formalized (Math- blobs) + +- N = `reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md`, blob `852f7403a8a06a1ef061e363df9502ae16f7a341` (L21, L22, L23, L26, L30, L53, L54). +- C = `reviews/side24_d2_certified_small_L_claude_20261005/certified_d2.py`, blob `6fd5b751cc4157136ae92225838c12d33dc997f3` (L8, L111–122, L137–153, L156–178). +- Math-#302 comment 6005199919 (body sha256 `28f5d504...`), as cited in `D2SchurLinks.lean`. + +## Declaration inventory + +### `W3Scratch/D2SchurLinks.lean` (namespace `W3Scratch`): 12 defs, 35 theorems + +- defs: `k2`, `k4`, `k6`, `srcAlpha`, `srcGamma`, `srcQ`, `srcE`, `srcDet`, `srcSchur`, `srcTau`, `srcQTheta`, `finMoment`. +- theorems: `d2Alpha_eq_src`, `d2Gamma_eq_src`, `srcE_sq`, `d2DetV_eq_alpha_gamma_q`, `d2DetV_eq_srcDet`, `d2DetV_eq_alpha_gamma_e`, `d2DetV_eq_det_varV`, `d2DetV_eq_note_linear`, `d2DetV_eq_alpha_gamma_e_needs_unit`, `srcQ_mem_Icc`, `exists_unit_of_mem_Icc`, `unit_q_range`, `unit_q_image`, `srcQTheta_eq`, `srcQTheta_range`, `d2_schur_endpoint_isLeast`, `d2_schur_endpoint_sInf`, `d2_schur_min_over_unit_directions`, `d2_schur_min_over_angles`, `moments_of_cumulants`, `cumulants_of_moments`, `gaussian_cumulants_iff`, `k4_sq_div`, `d2Tau_eq_srcTau`, `d2Schur_eq_srcSchur`, `d2Numerator_eq_comment`, `src_delta_cumulant`, `restrict_all_q`, `note_section2_every_direction`, `gaussian_control_on_Icc`, `positivity_every_direction`, `lagrange_weighted`, `double_sum_pos`, `finite_law_moment_hyps`, `finite_law_positivity_every_direction`. + +### `W3Scratch/Side24Law.lean` (namespace `W3Scratch.Side24`): 9 defs, 16 theorems + +- defs: `rawSum`, `lawMoment`, `atom`, `weight`, `dualZ`, `dualMoment`, `theta`, `imageSum`, `imageMoment`. +- theorems: `residual4_tsum`, `residual6_tsum`, `sq_pos_of_ne`, `countable_law_moment_hyps`, `weight_pos`, `summable_weight_mul_atom_pow`, `summable_sixth`, `dualZ_pos`, `dual_normalized`, `dual_odd_moment_zero`, `dual_moment_hyps`, `dual_positivity_every_direction`, `imageSum_zero`, `theta_zero_eq_dual`, `theta_term_iteratedDeriv`, `imageSum_even_eq_tsum_termwise`. + +### `W3Scratch/Side24Poisson.lean` (namespace `W3Scratch.Side24`): 3 defs, 26 theorems + +- defs: `gauss`, `thetaD`, `cosD`. +- theorems: `theta_eq_cos_series`, `contDiff_gauss`, `hasDerivAt_iterate_deriv_gauss`, `poly_exp_bound`, `abs_sub_sq_le`, `iterate_deriv_gauss_bound`, `summable_majorant`, `summable_thetaD_terms`, `hasDerivAt_thetaD`, `summable_abs_weight_mul_atom_pow`, `cosD_term_bound`, `hasDerivAt_cosD`, `thetaD_zero`, `cosD_zero`, `iteratedDeriv_theta`, `iteratedDeriv_theta_termwise`, `iteratedDeriv_cos_series`, `thetaD_eq_cosD`, `imageSum_even_eq_thetaD`, `iteratedDeriv_theta_zero_even`, `cosD_even_zero`, `imageSum_even_eq`, `imageMoment_even_eq_dualMoment`, `imageMoment_eq_dualMoment`, `image_moment_hyps`, `image_positivity_every_direction`. + +## Portable isolated build (scratch copy only; never commit these edits) + +1. Clone Math- and check out `7014efec8fb68cc926350caa8fa65dcd296f7f63` in a throwaway directory. +2. Copy this directory's `W3Scratch/` folder to `formal/W3Scratch/`. +3. In that throwaway copy only, append to `formal/lakefile.toml`: + + [[lean_lib]] + name = "W3Scratch" + roots = ["W3Scratch.D2SchurLinks", "W3Scratch.Side24Law", "W3Scratch.Side24Poisson"] + +4. `cd formal && lake exe cache get && lake build W3Scratch`. +5. Optional axiom check: a file that imports `W3Scratch.Side24Poisson` and runs `#print axioms` on each declaration above, built with `lake env lean `. + +This edits `formal/lakefile.toml` and adds unregistered modules, so in that copy `python3 formal/gate.py` is expected to fail (W3e saw `source hash mismatch: lakefile.toml`). That is why these steps must stay in a scratch copy. + +## Existing evidence and failures (author's own, box-local, UNVERIFIED) + +Each build ran under a process-tree RSS watchdog with a 6.5 GB limit. No build in W3d–W3g was killed by it. + +### Builds + +- **W3d** (prototype `W3dScratch.lean`, sha256 `3846f5bf...`; not included here; its D2Schur results reappear in `D2SchurLinks.lean`): run 1 failed (wrong import path, 0.59 GB); run 2 exit 0 (2.87 GB, 20 s); run 3 exit 0 (2.91 GB, 15.1 s). +- **W3e** (`D2SchurLinks.lean`): dev run 1 exit 1 (2 `positivity` errors, 3.05 GB, 22.0 s); dev run 2 exit 0 (3.08 GB, 19.0 s). `lake build W3Scratch` on a fresh clone at `9fd26113` with the W3e patch: exit 0 (3.84 GB, 48.1 s). +- **W3f** (`Side24Law.lean`): dev runs 1–5. Runs 1 and 4 failed on ordinary Lean errors (run 1: `No goals` after `field_simp`, a `rw` pattern; run 4: a `rw` pattern). Runs 2, 3 and 5 passed; run 5 is the final file (4.21 GB, 13.0 s). Gate-tree `lake build W3Scratch`: exit 0 (4.24 GB, 30.0 s). +- **W3g** (`Side24Poisson.lean`), **corrected history**: dev runs 1–6. **Runs 1, 2 and 4 failed on ordinary Lean errors; runs 3, 5 and 6 passed.** Run 6 is the final file (4.25 GB, 18.0 s). Gate-tree `lake build W3Scratch`: exit 0 (4.28 GB, 80.2 s). The build line in the W3g report 6050559869 was wrong; CoS recorded this erratum in 6050565322. No result is affected. + +### Axioms + +The only axioms allowed were propext, Classical.choice and Quot.sound. A text search of all three files found no `sorry`, `admit`, `native_decide` or `axiom`. + +- **W3e**: `AxiomsW3e.lean` exit 0 (3.31 GB). All 47 user declarations use `[propext, Classical.choice, Quot.sound]`; auxiliary constants use subsets of these. +- **W3f**: `AxiomsW3f.lean` exit 0 (3.77 GB). 35 constants: 27 user constants (25 declarations plus 2 equation lemmas), all `[propext, Classical.choice, Quot.sound]`; 8 auxiliary constants (7 `[propext]`, 1 the full set). +- **W3g**: `AxiomsW3g.lean` exit 0 (3.72 GB). 38 constants: 29 user declarations, all `[propext, Classical.choice, Quot.sound]`; auxiliary constants: 7 `[propext]`, 1 `[propext, Quot.sound]`, 1 the full set. + +### Gate and registration status (failures stay visible) + +- **Source-only gate.** A dry run on a local clone at `8d70baa7` (the modules under `formal/W3Scratch`, plus lakefile roots, root imports and manifest entries) gave `SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance)` (`be6d2121...`). W3f's dry run at `9fd26113` gave `217dc64f...`. This is a source-identity check only, not a Lean build and not acceptance. +- **Registration-test failure.** In those dry runs the unit suite had 133 tests and 1 failure, in normal and `-O` modes: `test_d2_schur` `test_manifest_exact_extension`. +- **Namespace mismatch.** The gate expects every target to be `ResearchFormalCoreR1.`, but these declarations live in `W3Scratch` and `W3Scratch.Side24`. W3f's `NameCheck.lean` showed that the gate's target names are unknown constants. So `gate.py --execute` is **not** satisfied by these files as published. +- **`gate.py --execute` was never satisfied.** + - Separately, a box-local option A variant (the same mathematics moved into `ResearchFormalCoreR1`, registered with 140 targets) passed the 139-test suite and the source check. + - Its `gate.py --execute` did **not** pass: `lake build` hit gate.py's hard-coded 900 s timeout under box load, and a second attempt was stopped when this decision arrived. + - That variant is **not** proposed here. + +## Open questions for the reader (unaccepted) + +The decision accepts none of these. + +- **R1.** k ∈ ℤ for the dual law (N L54 gives no range; C L156–178 sums k = 0 plus 2× k ≥ 1, the symmetric ℤ-sum). +- **R2.** The sign (−1)^(j/2) in the θ-route moment follows C L153 (`moments_image`), not N. +- **R3.** c² + s² = 1 for the direction u = (c, s) (N L26 does not write it). Without it the `d2DetV`-in-e identity fails, and `d2DetV_eq_alpha_gamma_e_needs_unit` gives a counterexample. +- **R4.** N L53's unsigned formula θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2} is proved as written for even j only (`iteratedDeriv_theta_zero_even`). For odd j the termwise derivative carries (−1)^j; that case is not stated. +- **Analytic correspondence.** + - (a) Is the W3f dual law (`atom`, `weight`, `dualZ`) the NOTE's "spectral law" (N L22, L54)? + - (b) Do the literal source objects (`k2`/`k4`/`k6`, `srcAlpha`, `srcGamma`, `srcQ`, `srcE`, `srcSchur`, `srcTau`, `theta`, `imageSum`, `imageMoment`) faithfully transcribe N and C? + - (c) Does "positivity in every direction for every L ≠ 0" (`dual_positivity_every_direction`, `image_positivity_every_direction`) correspond to anything the source certifies? The source certifies numerically at specific L only. + - A box-local follow-up compares the dual law with the moment characterization in `reviews/iba1_periodic_jet_claude_20261005/NOTE.md` L26–32. It is not part of this proposal, and the measure-level identification is open. + +— Grok Bot agent 13 (Grok Bot support agent; non-Claude, nonauthor lane) diff --git a/reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean b/reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean new file mode 100644 index 000000000..904fdd2c6 --- /dev/null +++ b/reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean @@ -0,0 +1,387 @@ +import ResearchFormalCoreR1.D2Schur +import Mathlib.LinearAlgebra.Matrix.Determinant.Basic +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse + +/-! +# W3Scratch.D2SchurLinks — SCRATCH / ENGINEERING ONLY + +Grok Bot agent 13, tasks W3d + W3e (Oct 7, 2026). Not reviewed, not aligned, not a discharge. +A Lean lemma ≠ alignment acceptance ≠ discharge. + +Links between `ResearchFormalCoreR1.D2Schur` (raw moments m2, m4, m6; parameter q) and +the source objects of reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md +(blob 852f7403, cumulants k2, k4, k6; direction u = (c, s)) and of Math-#302 comment +6005199919 (body sha256 28f5d504...). + +Readings used (stated, not claimed as the author's intent): +* NOTE L23 cumulant formulas are those of a symmetric coordinate law (odd moments zero). +* NOTE L26: u = (c, s) is a unit direction, c² + s² = 1 (not written in the NOTE). +-/ + +noncomputable section +namespace W3Scratch +open ResearchFormalCoreR1 + +/-! ## Source objects, written literally -/ + +/-- NOTE L23. -/ +def k2 (m2 : ℝ) : ℝ := m2 +/-- NOTE L23. -/ +def k4 (m2 m4 : ℝ) : ℝ := m4 - 3 * m2 ^ 2 +/-- NOTE L23. -/ +def k6 (m2 m4 m6 : ℝ) : ℝ := m6 - 15 * m4 * m2 + 30 * m2 ^ 3 +/-- NOTE L30, in cumulants. -/ +def srcAlpha (m2 m4 q : ℝ) : ℝ := 3 * k2 m2 ^ 2 + k4 m2 m4 - 2 * k4 m2 m4 * q +/-- NOTE L30, in cumulants. -/ +def srcGamma (m2 m4 q : ℝ) : ℝ := k2 m2 ^ 2 + 2 * k4 m2 m4 * q +/-- NOTE L26. -/ +def srcQ (c s : ℝ) : ℝ := c ^ 2 * s ^ 2 +/-- NOTE L26. -/ +def srcE (c s : ℝ) : ℝ := c * s * (c ^ 2 - s ^ 2) +/-- NOTE L34, first form, with e² = q(1 − 4q) (L28). -/ +def srcDet (m2 m4 q : ℝ) : ℝ := + srcAlpha m2 m4 q * srcGamma m2 m4 q - k4 m2 m4 ^ 2 * (q * (1 - 4 * q)) +/-- NOTE L35, with e² = q(1 − 4q). -/ +def srcSchur (m2 m4 q : ℝ) : ℝ := + srcAlpha m2 m4 q - + (srcGamma m2 m4 q ^ 3 + (2 * srcGamma m2 m4 q + srcAlpha m2 m4 q) * k4 m2 m4 ^ 2 * + (q * (1 - 4 * q))) / srcDet m2 m4 q +/-- NOTE L36, in cumulants (division is Lean's total division). -/ +def srcTau (m2 m4 m6 q : ℝ) : ℝ := + 6 * k2 m2 ^ 3 + 9 * k2 m2 * k4 m2 m4 * (1 - 2 * q) + + (k6 m2 m4 m6 - k4 m2 m4 ^ 2 / k2 m2) * (1 - 3 * q) +/-- NOTE L43: q(θ) = (1 − cos 4θ)/8. -/ +def srcQTheta (θ : ℝ) : ℝ := (1 - Real.cos (4 * θ)) / 8 + +/-! ## W3d (b): the missing link det V = αγ − k4² e² -/ + +theorem d2Alpha_eq_src (m2 m4 q : ℝ) : d2Alpha m2 m4 q = srcAlpha m2 m4 q := by + unfold d2Alpha srcAlpha k2 k4; ring + +theorem d2Gamma_eq_src (m2 m4 q : ℝ) : d2Gamma m2 m4 q = srcGamma m2 m4 q := by + unfold d2Gamma srcGamma k2 k4; ring + +theorem srcE_sq (c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + srcE c s ^ 2 = srcQ c s * (1 - 4 * srcQ c s) := by + unfold srcE srcQ + have h : (c ^ 2 - s ^ 2) ^ 2 = (c ^ 2 + s ^ 2) ^ 2 - 4 * (c ^ 2 * s ^ 2) := by ring + rw [mul_pow, h, hu]; ring + +theorem d2DetV_eq_alpha_gamma_q (m2 m4 q : ℝ) : + d2DetV m2 m4 q = d2Alpha m2 m4 q * d2Gamma m2 m4 q - k4 m2 m4 ^ 2 * (q * (1 - 4 * q)) := by + unfold d2DetV d2Alpha d2Gamma k4; ring + +theorem d2DetV_eq_srcDet (m2 m4 q : ℝ) : d2DetV m2 m4 q = srcDet m2 m4 q := by + unfold srcDet; rw [d2DetV_eq_alpha_gamma_q, d2Alpha_eq_src, d2Gamma_eq_src] + +theorem d2DetV_eq_alpha_gamma_e (m2 m4 c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + d2DetV m2 m4 (srcQ c s) = + srcAlpha m2 m4 (srcQ c s) * srcGamma m2 m4 (srcQ c s) - k4 m2 m4 ^ 2 * srcE c s ^ 2 := by + rw [srcE_sq c s hu, ← d2Alpha_eq_src, ← d2Gamma_eq_src] + exact d2DetV_eq_alpha_gamma_q m2 m4 (srcQ c s) + +theorem d2DetV_eq_det_varV (m2 m4 c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + d2DetV m2 m4 (srcQ c s) = + Matrix.det !![srcAlpha m2 m4 (srcQ c s), -(k4 m2 m4 * srcE c s); + -(k4 m2 m4 * srcE c s), srcGamma m2 m4 (srcQ c s)] := by + rw [Matrix.det_fin_two_of, d2DetV_eq_alpha_gamma_e m2 m4 c s hu]; ring + +theorem d2DetV_eq_note_linear (m2 m4 q : ℝ) : + d2DetV m2 m4 q = + k2 m2 ^ 2 * (3 * k2 m2 ^ 2 + k4 m2 m4) + k4 m2 m4 * (4 * k2 m2 ^ 2 + k4 m2 m4) * q := by + unfold d2DetV k2 k4; ring + +/-- The unit-norm hypothesis cannot be dropped (c = s = 1, m2 = 1, m4 = 2). -/ +theorem d2DetV_eq_alpha_gamma_e_needs_unit : + d2DetV 1 2 (srcQ 1 1) ≠ + srcAlpha 1 2 (srcQ 1 1) * srcGamma 1 2 (srcQ 1 1) - k4 1 2 ^ 2 * srcE 1 1 ^ 2 := by + unfold d2DetV srcAlpha srcGamma srcQ srcE k2 k4; norm_num + +/-! ## W3e (a): sweep lemma — q = c²s² over the unit circle is exactly [0, 1/4] -/ + +theorem srcQ_mem_Icc (c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : srcQ c s ∈ Set.Icc (0 : ℝ) (1 / 4) := by + unfold srcQ + constructor + · positivity + · have h : (c ^ 2 + s ^ 2) ^ 2 - 4 * (c ^ 2 * s ^ 2) = (c ^ 2 - s ^ 2) ^ 2 := by ring + rw [hu] at h + nlinarith [sq_nonneg (c ^ 2 - s ^ 2)] + +theorem exists_unit_of_mem_Icc (q : ℝ) (hq : q ∈ Set.Icc (0 : ℝ) (1 / 4)) : + ∃ c s : ℝ, c ^ 2 + s ^ 2 = 1 ∧ srcQ c s = q := by + obtain ⟨hq0, hq1⟩ := hq + set r := Real.sqrt (1 - 4 * q) with hr + have hr0 : 0 ≤ r := Real.sqrt_nonneg _ + have hr2 : r ^ 2 = 1 - 4 * q := Real.sq_sqrt (by linarith) + have hr1 : r ≤ 1 := by nlinarith + refine ⟨Real.sqrt ((1 + r) / 2), Real.sqrt ((1 - r) / 2), ?_, ?_⟩ + · rw [Real.sq_sqrt (by linarith), Real.sq_sqrt (by linarith)]; ring + · unfold srcQ + rw [Real.sq_sqrt (by linarith), Real.sq_sqrt (by linarith)] + nlinarith + +/-- (a) Sweep lemma as a set equality. -/ +theorem unit_q_range : + {q : ℝ | ∃ c s : ℝ, c ^ 2 + s ^ 2 = 1 ∧ q = srcQ c s} = Set.Icc (0 : ℝ) (1 / 4) := by + ext q + constructor + · rintro ⟨c, s, hu, rfl⟩; exact srcQ_mem_Icc c s hu + · intro hq + obtain ⟨c, s, hu, h⟩ := exists_unit_of_mem_Icc q hq + exact ⟨c, s, hu, h.symm⟩ + +/-- (a) Same, as an image of the unit circle. -/ +theorem unit_q_image : + (fun p : ℝ × ℝ => srcQ p.1 p.2) '' {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 = 1} = + Set.Icc (0 : ℝ) (1 / 4) := by + rw [← unit_q_range] + ext q + constructor + · rintro ⟨⟨c, s⟩, hu, rfl⟩; exact ⟨c, s, hu, rfl⟩ + · rintro ⟨c, s, hu, rfl⟩; exact ⟨⟨c, s⟩, hu, rfl⟩ + +/-- NOTE L43's angle parameterization agrees with q = c²s² at (c, s) = (cos θ, sin θ). -/ +theorem srcQTheta_eq (θ : ℝ) : srcQTheta θ = srcQ (Real.cos θ) (Real.sin θ) := by + unfold srcQTheta srcQ + have h4 : Real.cos (4 * θ) = 2 * Real.cos (2 * θ) ^ 2 - 1 := by + rw [show 4 * θ = 2 * (2 * θ) by ring, Real.cos_two_mul] + have h2 : Real.cos (2 * θ) = 2 * Real.cos θ ^ 2 - 1 := Real.cos_two_mul θ + have hs : Real.sin θ ^ 2 = 1 - Real.cos θ ^ 2 := by + have := Real.sin_sq_add_cos_sq θ; linarith + rw [h4, h2, hs]; ring + +/-- (a) Angle form: the range of q(θ) = (1 − cos 4θ)/8 is exactly [0, 1/4]. -/ +theorem srcQTheta_range : Set.range srcQTheta = Set.Icc (0 : ℝ) (1 / 4) := by + ext q + constructor + · rintro ⟨θ, rfl⟩ + rw [srcQTheta_eq] + exact srcQ_mem_Icc _ _ (by rw [add_comm]; exact Real.sin_sq_add_cos_sq θ) + · rintro ⟨hq0, hq1⟩ + refine ⟨Real.arccos (1 - 8 * q) / 4, ?_⟩ + unfold srcQTheta + rw [show 4 * (Real.arccos (1 - 8 * q) / 4) = Real.arccos (1 - 8 * q) by ring, + Real.cos_arccos (by linarith) (by linarith)] + ring + +/-! ## W3d (c) + W3e (a): the endpoint minimum, over q and over unit directions -/ + +theorem d2_schur_endpoint_isLeast (m2 m4 : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4) : + IsLeast (d2Schur m2 m4 '' Set.Icc (0 : ℝ) (1 / 4)) + (d2Numerator m2 m4 / max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4)) := by + constructor + · rcases le_total ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4) (m2 ^ 2 * m4) with h | h + · refine ⟨0, ⟨le_refl _, by norm_num⟩, ?_⟩ + have hD := d2_det_pos m2 m4 0 hm2 hm4 (le_refl _) (by norm_num) + rw [d2_schur_ratio m2 m4 0 (ne_of_gt hD), d2_det_axis, max_eq_left h] + · refine ⟨1 / 4, ⟨by norm_num, le_refl _⟩, ?_⟩ + have hD := d2_det_pos m2 m4 (1 / 4) hm2 hm4 (by norm_num) (le_refl _) + rw [d2_schur_ratio m2 m4 (1 / 4) (ne_of_gt hD), d2_det_diagonal, max_eq_right h] + · rintro _ ⟨q, ⟨hq0, hq1⟩, rfl⟩ + exact d2_schur_endpoint_lower m2 m4 q hm2 hm4 hq0 hq1 + +theorem d2_schur_endpoint_sInf (m2 m4 : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4) : + sInf (d2Schur m2 m4 '' Set.Icc (0 : ℝ) (1 / 4)) = + d2Numerator m2 m4 / max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4) := + (d2_schur_endpoint_isLeast m2 m4 hm2 hm4).csInf_eq + +/-- (a) The comment's L33 minimum, stated directly over unit directions u = (c, s). -/ +theorem d2_schur_min_over_unit_directions (m2 m4 : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4) : + IsLeast {σ : ℝ | ∃ c s : ℝ, c ^ 2 + s ^ 2 = 1 ∧ σ = d2Schur m2 m4 (srcQ c s)} + (d2Numerator m2 m4 / max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4)) := by + have h : {σ : ℝ | ∃ c s : ℝ, c ^ 2 + s ^ 2 = 1 ∧ σ = d2Schur m2 m4 (srcQ c s)} = + d2Schur m2 m4 '' Set.Icc (0 : ℝ) (1 / 4) := by + rw [← unit_q_range] + ext σ + constructor + · rintro ⟨c, s, hu, rfl⟩; exact ⟨srcQ c s, ⟨c, s, hu, rfl⟩, rfl⟩ + · rintro ⟨q, ⟨c, s, hu, rfl⟩, rfl⟩; exact ⟨c, s, hu, rfl⟩ + rw [h]; exact d2_schur_endpoint_isLeast m2 m4 hm2 hm4 + +/-- (a) The same minimum over the NOTE's angle θ ∈ ℝ (q(θ) = (1 − cos 4θ)/8). -/ +theorem d2_schur_min_over_angles (m2 m4 : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4) : + IsLeast (Set.range fun θ : ℝ => d2Schur m2 m4 (srcQTheta θ)) + (d2Numerator m2 m4 / max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4)) := by + have h : (Set.range fun θ : ℝ => d2Schur m2 m4 (srcQTheta θ)) = + d2Schur m2 m4 '' Set.Icc (0 : ℝ) (1 / 4) := by + rw [← srcQTheta_range, ← Set.range_comp]; rfl + rw [h]; exact d2_schur_endpoint_isLeast m2 m4 hm2 hm4 + +/-! ## W3e (b)1: cumulants ↔ raw moments -/ + +/-- Inverse map (symmetric law): m4 = k4 + 3k2², m6 = k6 + 15 k2 k4 + 15 k2³. -/ +theorem moments_of_cumulants (m2 m4 m6 : ℝ) : + m2 = k2 m2 ∧ m4 = k4 m2 m4 + 3 * k2 m2 ^ 2 ∧ + m6 = k6 m2 m4 m6 + 15 * k2 m2 * k4 m2 m4 + 15 * k2 m2 ^ 3 := by + unfold k2 k4 k6; refine ⟨rfl, by ring, by ring⟩ + +/-- Round trip from cumulants: any (K2, K4, K6) is hit by exactly the moments above. -/ +theorem cumulants_of_moments (K2 K4 K6 : ℝ) : + k2 K2 = K2 ∧ k4 K2 (K4 + 3 * K2 ^ 2) = K4 ∧ + k6 K2 (K4 + 3 * K2 ^ 2) (K6 + 15 * K2 * K4 + 15 * K2 ^ 3) = K6 := by + unfold k2 k4 k6; refine ⟨rfl, by ring, by ring⟩ + +/-- NOTE L48 Gaussian reference: (k2, k4, k6) = (1, 0, 0) iff (m2, m4, m6) = (1, 3, 15). -/ +theorem gaussian_cumulants_iff (m2 m4 m6 : ℝ) : + (k2 m2 = 1 ∧ k4 m2 m4 = 0 ∧ k6 m2 m4 m6 = 0) ↔ (m2 = 1 ∧ m4 = 3 ∧ m6 = 15) := by + unfold k2 k4 k6 + constructor + · rintro ⟨h2, h4, h6⟩ + subst h2 + have h4' : m4 = 3 := by linarith + subst h4' + exact ⟨rfl, rfl, by linarith⟩ + · rintro ⟨rfl, rfl, rfl⟩; norm_num + +/-- Helper: (m4 − 3m2²)²/m2 = m4²/m2 − 6 m4 m2 + 9 m2³ for ALL real m2 (both sides 0 at m2 = 0). -/ +theorem k4_sq_div (m2 m4 : ℝ) : + k4 m2 m4 ^ 2 / k2 m2 = m4 ^ 2 / m2 - 6 * m4 * m2 + 9 * m2 ^ 3 := by + unfold k2 k4 + rcases eq_or_ne m2 0 with h | h + · subst h; simp + · field_simp; ring + +/-- The NOTE's τ² in cumulants equals the Lean `d2Tau` with NO hypothesis on m2 +(the existing `d2_tau_cumulant_eq` assumes m2 ≠ 0; it is not needed). -/ +theorem d2Tau_eq_srcTau (m2 m4 m6 q : ℝ) : d2Tau m2 m4 m6 q = srcTau m2 m4 m6 q := by + unfold srcTau + rw [k4_sq_div] + unfold d2Tau d2Delta k2 k4 k6 + ring + +/-- The NOTE's Σ_{A|V} in cumulants equals the Lean `d2Schur`, all real q, no hypotheses. -/ +theorem d2Schur_eq_srcSchur (m2 m4 q : ℝ) : d2Schur m2 m4 q = srcSchur m2 m4 q := by + unfold d2Schur srcSchur + rw [← d2DetV_eq_srcDet, ← d2Alpha_eq_src, ← d2Gamma_eq_src] + unfold k4; ring + +/-- Comment 6005199919 L15/L17 right-hand side: x(2x+b)(4x+b), x = m2², b = k4. -/ +theorem d2Numerator_eq_comment (m2 m4 : ℝ) : + d2Numerator m2 m4 = m2 ^ 2 * (2 * m2 ^ 2 + k4 m2 m4) * (4 * m2 ^ 2 + k4 m2 m4) := by + unfold d2Numerator k4; ring + +/-- Comment L29: Δ = m6 − m4²/m2 is literally `d2Delta`. NOTE's k6 − k4²/k2 in moments. -/ +theorem src_delta_cumulant (m2 m4 m6 : ℝ) : + k6 m2 m4 m6 - k4 m2 m4 ^ 2 / k2 m2 = d2Delta m2 m4 m6 - 9 * m4 * m2 + 21 * m2 ^ 3 := by + rw [k4_sq_div]; unfold k6 d2Delta; ring + +/-! ## W3e (b)3: all-q identities specialize to the source's restricted statements -/ + +/-- Generic: an all-q statement restricts to [0, 1/4] and to every unit direction. -/ +theorem restrict_all_q {P : ℝ → Prop} (h : ∀ q, P q) : + (∀ q ∈ Set.Icc (0 : ℝ) (1 / 4), P q) ∧ (∀ c s : ℝ, c ^ 2 + s ^ 2 = 1 → P (srcQ c s)) := + ⟨fun q _ => h q, fun c s _ => h (srcQ c s)⟩ + +/-- NOTE §2 L34–36 in every unit direction, obtained from the all-q identities by specialization. -/ +theorem note_section2_every_direction (m2 m4 m6 c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + srcQ c s ∈ Set.Icc (0 : ℝ) (1 / 4) ∧ + d2DetV m2 m4 (srcQ c s) = + srcAlpha m2 m4 (srcQ c s) * srcGamma m2 m4 (srcQ c s) - k4 m2 m4 ^ 2 * srcE c s ^ 2 ∧ + d2DetV m2 m4 (srcQ c s) = k2 m2 ^ 2 * (3 * k2 m2 ^ 2 + k4 m2 m4) + + k4 m2 m4 * (4 * k2 m2 ^ 2 + k4 m2 m4) * srcQ c s ∧ + d2Schur m2 m4 (srcQ c s) = srcSchur m2 m4 (srcQ c s) ∧ + d2Tau m2 m4 m6 (srcQ c s) = srcTau m2 m4 m6 (srcQ c s) ∧ + d2Alpha m2 m4 (srcQ c s) * d2DetV m2 m4 (srcQ c s) - d2Gamma m2 m4 (srcQ c s) ^ 3 - + (2 * d2Gamma m2 m4 (srcQ c s) + d2Alpha m2 m4 (srcQ c s)) * + (m4 - 3 * m2 ^ 2) ^ 2 * srcQ c s * (1 - 4 * srcQ c s) = d2Numerator m2 m4 := + ⟨srcQ_mem_Icc c s hu, d2DetV_eq_alpha_gamma_e m2 m4 c s hu, d2DetV_eq_note_linear _ _ _, + d2Schur_eq_srcSchur _ _ _, d2Tau_eq_srcTau _ _ _ _, d2_schur_numerator _ _ _⟩ + +/-- NOTE L48 Gaussian controls hold on [0, 1/4] (specialization of `d2_gaussian_control`). -/ +theorem gaussian_control_on_Icc : + ∀ q ∈ Set.Icc (0 : ℝ) (1 / 4), d2DetV 1 3 q = 3 ∧ d2Schur 1 3 q = 8 / 3 ∧ d2Tau 1 3 15 q = 6 := + (restrict_all_q d2_gaussian_control).1 + +/-! ## W3e (b)2: positivity in every direction, general form -/ + +/-- NOTE L59/L78 "positive in every direction", as a general real-variable statement: +any moments with 0 < m2, m2² < m4, 0 < Δ give τ², det V, Σ_{A|V} > 0 for every unit u. -/ +theorem positivity_every_direction (m2 m4 m6 : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4) + (hΔ : 0 < d2Delta m2 m4 m6) (c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + 0 < d2DetV m2 m4 (srcQ c s) ∧ 0 < d2Schur m2 m4 (srcQ c s) ∧ + 0 < d2Tau m2 m4 m6 (srcQ c s) := by + obtain ⟨h0, h1⟩ := srcQ_mem_Icc c s hu + exact ⟨d2_det_pos _ _ _ hm2 hm4 h0 h1, d2_schur_pos _ _ _ hm2 hm4 h0 h1, + d2_tau_pos _ _ _ _ hm2 hm4 hΔ h0 h1⟩ + +/-- Weighted Lagrange identity (finite sums). -/ +theorem lagrange_weighted {ι : Type*} [Fintype ι] (p f g : ι → ℝ) : + 2 * ((∑ i, p i * f i ^ 2) * (∑ i, p i * g i ^ 2) - (∑ i, p i * (f i * g i)) ^ 2) = + ∑ i, ∑ j, p i * p j * (f i * g j - f j * g i) ^ 2 := by + have e : ∀ i j, p i * p j * (f i * g j - f j * g i) ^ 2 = + (p i * f i ^ 2) * (p j * g j ^ 2) + (p i * g i ^ 2) * (p j * f j ^ 2) - + (2 * (p i * (f i * g i))) * (p j * (f j * g j)) := by intro i j; ring + simp only [e, Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.mul_sum, + ← Finset.sum_mul] + ring + +/-- Raw moment of a finite weighted law. -/ +def finMoment {ι : Type*} [Fintype ι] (p x : ι → ℝ) (n : ℕ) : ℝ := ∑ i, p i * x i ^ n + +theorem double_sum_pos {ι : Type*} [Fintype ι] (F : ι → ι → ℝ) (hF : ∀ i j, 0 ≤ F i j) + (a b : ι) (hab : 0 < F a b) : 0 < ∑ i, ∑ j, F i j := by + apply Finset.sum_pos' (fun i _ => Finset.sum_nonneg (fun j _ => hF i j)) + exact ⟨a, Finset.mem_univ _, Finset.sum_pos' (fun j _ => hF a j) ⟨b, Finset.mem_univ _, hab⟩⟩ + +/-- Moment hypotheses for any finite probability law with two nonzero atoms of distinct squares +(a finite-support analogue of D2MomentBridge's two-atom lemmas; self-contained). -/ +theorem finite_law_moment_hyps {ι : Type*} [Fintype ι] (p x : ι → ℝ) (hp : ∀ i, 0 ≤ p i) + (hsum : ∑ i, p i = 1) (a b : ι) (hpa : 0 < p a) (hpb : 0 < p b) (ha0 : x a ≠ 0) + (hb0 : x b ≠ 0) (hab : x a ^ 2 ≠ x b ^ 2) : + 0 < finMoment p x 2 ∧ finMoment p x 2 ^ 2 < finMoment p x 4 ∧ + 0 < d2Delta (finMoment p x 2) (finMoment p x 4) (finMoment p x 6) := by + have hm2 : 0 < finMoment p x 2 := by + unfold finMoment + exact Finset.sum_pos' (fun i _ => mul_nonneg (hp i) (sq_nonneg _)) + ⟨a, Finset.mem_univ _, mul_pos hpa (by positivity)⟩ + -- m4 − m2² via f = 1, g = x² + have L1 := lagrange_weighted p (fun _ => (1 : ℝ)) (fun i => x i ^ 2) + have hpos1 : 0 < ∑ i, ∑ j, p i * p j * ((fun _ => (1 : ℝ)) i * (fun i => x i ^ 2) j - + (fun _ => (1 : ℝ)) j * (fun i => x i ^ 2) i) ^ 2 := by + apply double_sum_pos _ (fun i j => mul_nonneg (mul_nonneg (hp i) (hp j)) (sq_nonneg _)) a b + have : x b ^ 2 - x a ^ 2 ≠ 0 := sub_ne_zero.mpr (Ne.symm hab) + simp only [one_mul] + exact mul_pos (mul_pos hpa hpb) (by positivity) + have hm4 : finMoment p x 2 ^ 2 < finMoment p x 4 := by + have e1 : (∑ i, p i * (fun _ => (1 : ℝ)) i ^ 2) = 1 := by simpa using hsum + have e2 : (∑ i, p i * (fun i => x i ^ 2) i ^ 2) = finMoment p x 4 := by + unfold finMoment; refine Finset.sum_congr rfl (fun i _ => ?_); ring + have e3 : (∑ i, p i * ((fun _ => (1 : ℝ)) i * (fun i => x i ^ 2) i)) = finMoment p x 2 := by + unfold finMoment; refine Finset.sum_congr rfl (fun i _ => ?_); ring + rw [e1, e2, e3] at L1 + linarith + -- m2 m6 − m4² via f = x, g = x³ + have L2 := lagrange_weighted p x (fun i => x i ^ 3) + have hpos2 : 0 < ∑ i, ∑ j, p i * p j * (x i * (fun i => x i ^ 3) j - + x j * (fun i => x i ^ 3) i) ^ 2 := by + apply double_sum_pos _ (fun i j => mul_nonneg (mul_nonneg (hp i) (hp j)) (sq_nonneg _)) a b + have h1 : x a * x b ^ 3 - x b * x a ^ 3 = x a * x b * (x b ^ 2 - x a ^ 2) := by ring + have : x b ^ 2 - x a ^ 2 ≠ 0 := sub_ne_zero.mpr (Ne.symm hab) + simp only [] + rw [h1] + exact mul_pos (mul_pos hpa hpb) (by positivity) + have hm6 : finMoment p x 4 ^ 2 < finMoment p x 2 * finMoment p x 6 := by + have e1 : (∑ i, p i * x i ^ 2) = finMoment p x 2 := rfl + have e2 : (∑ i, p i * (fun i => x i ^ 3) i ^ 2) = finMoment p x 6 := by + unfold finMoment; refine Finset.sum_congr rfl (fun i _ => ?_); ring + have e3 : (∑ i, p i * (x i * (fun i => x i ^ 3) i)) = finMoment p x 4 := by + unfold finMoment; refine Finset.sum_congr rfl (fun i _ => ?_); ring + rw [e1, e2, e3] at L2 + linarith + refine ⟨hm2, hm4, ?_⟩ + unfold d2Delta + rw [sub_pos, div_lt_iff₀ hm2] + linarith + +/-- (b)2 general statement for finite laws: positivity of τ², det V, Σ_{A|V} in every direction. -/ +theorem finite_law_positivity_every_direction {ι : Type*} [Fintype ι] (p x : ι → ℝ) + (hp : ∀ i, 0 ≤ p i) (hsum : ∑ i, p i = 1) (a b : ι) (hpa : 0 < p a) (hpb : 0 < p b) + (ha0 : x a ≠ 0) (hb0 : x b ≠ 0) (hab : x a ^ 2 ≠ x b ^ 2) (c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + 0 < d2DetV (finMoment p x 2) (finMoment p x 4) (srcQ c s) ∧ + 0 < d2Schur (finMoment p x 2) (finMoment p x 4) (srcQ c s) ∧ + 0 < d2Tau (finMoment p x 2) (finMoment p x 4) (finMoment p x 6) (srcQ c s) := by + obtain ⟨h2, h4, h6⟩ := finite_law_moment_hyps p x hp hsum a b hpa hpb ha0 hb0 hab + exact positivity_every_direction _ _ _ h2 h4 h6 c s hu + +end W3Scratch diff --git a/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean new file mode 100644 index 000000000..26b35e0ac --- /dev/null +++ b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean @@ -0,0 +1,286 @@ +import W3Scratch.D2SchurLinks +import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable +import Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation +import Mathlib.RingTheory.Polynomial.Hermite.Gaussian + +/-! +# W3Scratch.Side24Law — SCRATCH / ENGINEERING ONLY + +Grok Bot agent 13, task W3f (Oct 7, 2026). Not reviewed, not aligned, not a discharge. +A Lean lemma ≠ alignment acceptance ≠ discharge. + +Merged sources only, Math- main @ 9fd261135b41daf1e377f9ef2db193fee6ec36be: +* N = reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md, blob 852f7403a8a06a1ef061e363df9502ae16f7a341 + - N L21: `θ_L(t) = Σ_n e^{−(t+Ln)²/2}`, `q_L = θ_L/θ_L(0)`. + - N L22: one coordinate of the spectral law has raw moments m2, m4, m6. + - N L53: `θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2}` (image sums). + - N L54: Poisson-dual law `P(X = 2πk/L) ∝ e^{−(2πk/L)²/2}`. +* C = reviews/side24_d2_certified_small_L_claude_20261005/certified_d2.py, blob 6fd5b751cc4157136ae92225838c12d33dc997f3 + - C L8: same θ_L as N L21. C L111-122: He_2, He_4, He_6 (probabilists' Hermite). + - C L137-153 `moments_image`: returns `(-θ2/θ0, θ4/θ0, -θ6/θ0)`, i.e. m_j = (-1)^(j/2) θ^{(j)}(0)/θ(0). + - C L156-178 `moments_dual`: weights 1 (k = 0) and 2 e^{−(hk)²/2} (k ≥ 1), h = 2π/L; m_j = Σ w ω^j / Σ w. + +Readings (flagged): k ranges over ℤ (N L54 gives no range; C sums k = 0 plus 2× k ≥ 1, which is +the symmetric ℤ-sum). The θ-route moment formula with the sign (-1)^(j/2) is from C L153, not N. +-/ + +noncomputable section +namespace W3Scratch.Side24 +open ResearchFormalCoreR1 W3Scratch Real + +/-! ## Generic countable discrete law -/ + +section Generic +variable {ι : Type*} (w a : ι → ℝ) + +/-- Unnormalized moment sum Σ w_i a_i^n. -/ +def rawSum (n : ℕ) : ℝ := ∑' i, w i * a i ^ n +/-- Normalized raw moment m_n = Σ w a^n / Σ w. -/ +def lawMoment (n : ℕ) : ℝ := rawSum w a n / rawSum w a 0 + +variable {w a} + +theorem residual4_tsum (hs : ∀ n : ℕ, Summable fun i => w i * a i ^ n) (m : ℝ) : + Summable (fun i => w i * (a i ^ 2 - m) ^ 2) ∧ + ∑' i, w i * (a i ^ 2 - m) ^ 2 = rawSum w a 4 - 2 * m * rawSum w a 2 + m ^ 2 * rawSum w a 0 := by + have e : (fun i => w i * (a i ^ 2 - m) ^ 2) = + fun i => (w i * a i ^ 4 - 2 * m * (w i * a i ^ 2)) + m ^ 2 * (w i * a i ^ 0) := by + funext i; ring + have h1 : Summable fun i => w i * a i ^ 4 - 2 * m * (w i * a i ^ 2) := + (hs 4).sub ((hs 2).mul_left _) + have h2 : Summable fun i => m ^ 2 * (w i * a i ^ 0) := (hs 0).mul_left _ + refine ⟨e ▸ h1.add h2, ?_⟩ + rw [e, h1.tsum_add h2, (hs 4).tsum_sub ((hs 2).mul_left _), tsum_mul_left, tsum_mul_left] + rfl + +theorem residual6_tsum (hs : ∀ n : ℕ, Summable fun i => w i * a i ^ n) (c : ℝ) : + Summable (fun i => w i * (a i ^ 3 - c * a i) ^ 2) ∧ + ∑' i, w i * (a i ^ 3 - c * a i) ^ 2 = + rawSum w a 6 - 2 * c * rawSum w a 4 + c ^ 2 * rawSum w a 2 := by + have e : (fun i => w i * (a i ^ 3 - c * a i) ^ 2) = + fun i => (w i * a i ^ 6 - 2 * c * (w i * a i ^ 4)) + c ^ 2 * (w i * a i ^ 2) := by + funext i; ring + have h1 : Summable fun i => w i * a i ^ 6 - 2 * c * (w i * a i ^ 4) := + (hs 6).sub ((hs 4).mul_left _) + have h2 : Summable fun i => c ^ 2 * (w i * a i ^ 2) := (hs 2).mul_left _ + refine ⟨e ▸ h1.add h2, ?_⟩ + rw [e, h1.tsum_add h2, (hs 6).tsum_sub ((hs 4).mul_left _), tsum_mul_left, tsum_mul_left] + rfl + +theorem sq_pos_of_ne {x : ℝ} (hx : x ≠ 0) : 0 < x ^ 2 := + lt_of_le_of_ne (sq_nonneg _) (Ne.symm (pow_ne_zero 2 hx)) + +/-- Countable-support analogue of `finite_law_moment_hyps`: two nonzero atoms with distinct squares +give 0 < m2, m2² < m4 and Δ > 0. -/ +theorem countable_law_moment_hyps (hw : ∀ i, 0 ≤ w i) + (hs : ∀ n : ℕ, Summable fun i => w i * a i ^ n) (i j : ι) (hwi : 0 < w i) (hwj : 0 < w j) + (hai : a i ≠ 0) (haj : a j ≠ 0) (hij : a i ^ 2 ≠ a j ^ 2) : + 0 < lawMoment w a 2 ∧ lawMoment w a 2 ^ 2 < lawMoment w a 4 ∧ + 0 < d2Delta (lawMoment w a 2) (lawMoment w a 4) (lawMoment w a 6) := by + have hZ : 0 < rawSum w a 0 := + (hs 0).tsum_pos (fun k => by rw [pow_zero, mul_one]; exact hw k) i + (by rw [pow_zero, mul_one]; exact hwi) + have hS2 : 0 < rawSum w a 2 := + (hs 2).tsum_pos (fun k => mul_nonneg (hw k) (sq_nonneg _)) i (mul_pos hwi (sq_pos_of_ne hai)) + -- pick an atom whose square differs from a given value + have pick : ∀ v : ℝ, ∃ k, 0 < w k ∧ a k ≠ 0 ∧ a k ^ 2 ≠ v := by + intro v + by_cases h : a i ^ 2 = v + · exact ⟨j, hwj, haj, fun h' => hij (h.trans h'.symm)⟩ + · exact ⟨i, hwi, hai, h⟩ + set Z := rawSum w a 0 with hZdef + set S2 := rawSum w a 2 + set S4 := rawSum w a 4 + set S6 := rawSum w a 6 + -- m4 − m2² > 0 + obtain ⟨k, hwk, -, hk⟩ := pick (S2 / Z) + obtain ⟨hsum4, heq4⟩ := residual4_tsum hs (S2 / Z) + have hpos4 : 0 < ∑' i, w i * (a i ^ 2 - S2 / Z) ^ 2 := + hsum4.tsum_pos (fun i => mul_nonneg (hw i) (sq_nonneg _)) k + (mul_pos hwk (sq_pos_of_ne (sub_ne_zero.mpr hk))) + rw [heq4] at hpos4 + have h4 : 0 < S4 * Z - S2 ^ 2 := by + have e : S4 - 2 * (S2 / Z) * S2 + (S2 / Z) ^ 2 * Z = (S4 * Z - S2 ^ 2) / Z := by + field_simp; ring + rw [e] at hpos4 + exact (div_pos_iff_of_pos_right hZ).mp hpos4 + -- m2 m6 − m4² > 0 + obtain ⟨k', hwk', hak', hk'⟩ := pick (S4 / S2) + obtain ⟨hsum6, heq6⟩ := residual6_tsum hs (S4 / S2) + have hpos6 : 0 < ∑' i, w i * (a i ^ 3 - S4 / S2 * a i) ^ 2 := by + refine hsum6.tsum_pos (fun i => mul_nonneg (hw i) (sq_nonneg _)) k' (mul_pos hwk' ?_) + have : a k' ^ 3 - S4 / S2 * a k' = a k' * (a k' ^ 2 - S4 / S2) := by ring + rw [this] + exact sq_pos_of_ne (mul_ne_zero hak' (sub_ne_zero.mpr hk')) + rw [heq6] at hpos6 + have h6 : 0 < S6 * S2 - S4 ^ 2 := by + have e : S6 - 2 * (S4 / S2) * S4 + (S4 / S2) ^ 2 * S2 = (S6 * S2 - S4 ^ 2) / S2 := by + field_simp; ring + rw [e] at hpos6 + exact (div_pos_iff_of_pos_right hS2).mp hpos6 + refine ⟨div_pos hS2 hZ, ?_, ?_⟩ + · unfold lawMoment + rw [div_pow, div_lt_div_iff₀ (by positivity) hZ] + nlinarith [mul_pos h4 hZ] + · unfold lawMoment d2Delta + have e : S6 / Z - (S4 / Z) ^ 2 / (S2 / Z) = (S6 * S2 - S4 ^ 2) / (Z * S2) := by + field_simp + rw [e]; exact div_pos h6 (mul_pos hZ hS2) + +end Generic + +/-! ## The SIDE24 Poisson-dual law (N L54; C L156-178) -/ + +/-- Atom 2πk/L (N L54). -/ +def atom (L : ℝ) (k : ℤ) : ℝ := 2 * π * k / L +/-- Unnormalized weight e^{−(2πk/L)²/2} (N L54). -/ +def weight (L : ℝ) (k : ℤ) : ℝ := Real.exp (-(atom L k) ^ 2 / 2) +/-- Normalizer Σ_k e^{−(2πk/L)²/2}. -/ +def dualZ (L : ℝ) : ℝ := rawSum (weight L) (atom L) 0 +/-- Raw moment m_n(L) of the dual law (C L178: w[j]/w[0]). -/ +def dualMoment (L : ℝ) (n : ℕ) : ℝ := lawMoment (weight L) (atom L) n + +theorem weight_pos (L : ℝ) (k : ℤ) : 0 < weight L k := Real.exp_pos _ + +/-- Summability of Σ_k w_k · atom_k^n for every n (in particular n = 6: X⁶ integrability). -/ +theorem summable_weight_mul_atom_pow {L : ℝ} (hL : L ≠ 0) (n : ℕ) : + Summable fun k : ℤ => weight L k * atom L k ^ n := by + have hT : 0 < 2 * π / L ^ 2 := by positivity + have hb := (summable_pow_mul_jacobiTheta₂_term_bound 0 hT n).mul_left ((2 * π / |L|) ^ n) + refine Summable.of_norm_bounded hb (fun k => le_of_eq ?_) + have hexp : -(atom L k) ^ 2 / 2 = -π * (2 * π / L ^ 2 * (k : ℝ) ^ 2 - 2 * 0 * |(k : ℝ)|) := by + unfold atom; field_simp; ring + have habs : |atom L k| = 2 * π / |L| * |(k : ℝ)| := by + unfold atom + rw [abs_div, abs_mul, abs_mul, abs_two, abs_of_pos pi_pos] + ring + rw [Real.norm_eq_abs, abs_mul, abs_pow, weight, abs_of_pos (Real.exp_pos _), habs, hexp, + mul_pow] + simp only [Int.cast_abs] + ring + +/-- X⁶ integrability of the dual law, stated as summability. -/ +theorem summable_sixth {L : ℝ} (hL : L ≠ 0) : Summable fun k : ℤ => weight L k * atom L k ^ 6 := + summable_weight_mul_atom_pow hL 6 + +theorem dualZ_pos {L : ℝ} (hL : L ≠ 0) : 0 < dualZ L := + (summable_weight_mul_atom_pow hL 0).tsum_pos + (fun k => by rw [pow_zero, mul_one]; exact (weight_pos L k).le) 0 + (by rw [pow_zero, mul_one]; exact weight_pos L 0) + +/-- Normalization: the probabilities w_k / Z sum to 1. -/ +theorem dual_normalized {L : ℝ} (hL : L ≠ 0) : ∑' k : ℤ, weight L k / dualZ L = 1 := by + have h := dualZ_pos hL + rw [tsum_div_const] + have : ∑' k : ℤ, weight L k = dualZ L := by + unfold dualZ rawSum; simp only [pow_zero, mul_one] + rw [this, div_self (ne_of_gt h)] + +/-- Symmetry: odd raw moments vanish (atom(−k) = −atom(k), weight even). -/ +theorem dual_odd_moment_zero (L : ℝ) (m : ℕ) : rawSum (weight L) (atom L) (2 * m + 1) = 0 := by + unfold rawSum + have hneg : ∀ k : ℤ, weight L (-k) * atom L (-k) ^ (2 * m + 1) = + -(weight L k * atom L k ^ (2 * m + 1)) := by + intro k + have ha : atom L (-k) = -atom L k := by unfold atom; push_cast; ring + rw [weight, weight, ha, neg_sq, Odd.neg_pow ⟨m, rfl⟩]; ring + have h := tsum_comp_neg (fun k : ℤ => weight L k * atom L k ^ (2 * m + 1)) + simp only [hneg, tsum_neg] at h + linarith + +/-- Moment hypotheses for the SIDE24 dual law at EVERY nonzero period L (atoms k = 1, 2). -/ +theorem dual_moment_hyps {L : ℝ} (hL : L ≠ 0) : + 0 < dualMoment L 2 ∧ dualMoment L 2 ^ 2 < dualMoment L 4 ∧ + 0 < d2Delta (dualMoment L 2) (dualMoment L 4) (dualMoment L 6) := by + have h1 : atom L 1 ≠ 0 := by + unfold atom; push_cast; exact div_ne_zero (by positivity) hL + have h2 : atom L 2 ≠ 0 := by + unfold atom; push_cast; exact div_ne_zero (by positivity) hL + have h12 : atom L 1 ^ 2 ≠ atom L 2 ^ 2 := by + unfold atom; push_cast + intro h + have hpi : (2 * π / L) ^ 2 ≠ 0 := pow_ne_zero 2 (div_ne_zero (by positivity) hL) + apply hpi + have : (2 * π * 2 / L) ^ 2 = 4 * (2 * π / L) ^ 2 := by ring + have : (2 * π * 1 / L) ^ 2 = (2 * π / L) ^ 2 := by ring + linarith + exact countable_law_moment_hyps (fun k => (weight_pos L k).le) (summable_weight_mul_atom_pow hL) + 1 2 (weight_pos L 1) (weight_pos L 2) h1 h2 h12 + +/-- The NOTE's "positive in every direction" (N L59, L78; certified numerically at six L) holds for +the dual-law moments at EVERY nonzero L. -/ +theorem dual_positivity_every_direction {L : ℝ} (hL : L ≠ 0) (c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + 0 < d2DetV (dualMoment L 2) (dualMoment L 4) (srcQ c s) ∧ + 0 < d2Schur (dualMoment L 2) (dualMoment L 4) (srcQ c s) ∧ + 0 < d2Tau (dualMoment L 2) (dualMoment L 4) (dualMoment L 6) (srcQ c s) := by + obtain ⟨h2, h4, h6⟩ := dual_moment_hyps hL + exact positivity_every_direction _ _ _ h2 h4 h6 c s hu + +/-! ## The θ-series route (N L21, L53; C L137-153) -/ + +/-- θ_L(t) = Σ_n e^{−(t+Ln)²/2} (N L21). -/ +def theta (L t : ℝ) : ℝ := ∑' n : ℤ, Real.exp (-(t + L * n) ^ 2 / 2) +/-- Image sum Σ_n He_j(Ln) e^{−(Ln)²/2} (N L53), probabilists' Hermite `Polynomial.hermite`. -/ +def imageSum (L : ℝ) (j : ℕ) : ℝ := + ∑' n : ℤ, Polynomial.aeval (L * n) (Polynomial.hermite j) * Real.exp (-(L * n) ^ 2 / 2) +/-- θ-route moment m_j = (−1)^(j/2) θ^{(j)}(0)/θ(0), via image sums (C L153). -/ +def imageMoment (L : ℝ) (j : ℕ) : ℝ := (-1) ^ (j / 2) * imageSum L j / imageSum L 0 + +theorem imageSum_zero (L : ℝ) : imageSum L 0 = theta L 0 := by + unfold imageSum theta + simp [Polynomial.hermite_zero] + +/-- Poisson link, j = 0 (closed): θ_L(0) = (L²/(2π))^{−1/2} · Σ_k e^{−(2πk/L)²/2}, from +Mathlib's `Real.tsum_exp_neg_mul_int_sq`. -/ +theorem theta_zero_eq_dual {L : ℝ} (hL : L ≠ 0) : + theta L 0 = 1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) * dualZ L := by + have ha : 0 < L ^ 2 / (2 * π) := by positivity + have h := Real.tsum_exp_neg_mul_int_sq ha + have e1 : ∀ n : ℤ, Real.exp (-π * (L ^ 2 / (2 * π)) * (n : ℝ) ^ 2) = + Real.exp (-((0 : ℝ) + L * n) ^ 2 / 2) := by + intro n; congr 1; field_simp; ring + have e2 : ∀ n : ℤ, Real.exp (-π / (L ^ 2 / (2 * π)) * (n : ℝ) ^ 2) = weight L n * atom L n ^ 0 := by + intro n; rw [pow_zero, mul_one, weight, atom]; congr 1; field_simp + simp only [e1, e2] at h + exact h + +/-- Step (iii) of the Poisson link, closed: the j-th t-derivative at 0 of one θ-term is +(−1)^j He_j(y) e^{−y²/2} (Mathlib `deriv_gaussian_eq_hermite_mul_gaussian`). -/ +theorem theta_term_iteratedDeriv (y : ℝ) (j : ℕ) : + iteratedDeriv j (fun t => Real.exp (-(t + y) ^ 2 / 2)) 0 = + (-1 : ℝ) ^ j * Polynomial.aeval y (Polynomial.hermite j) * Real.exp (-y ^ 2 / 2) := by + have h := congrFun (iteratedDeriv_comp_add_const j (fun z : ℝ => Real.exp (-(z ^ 2 / 2))) y) 0 + simp only [zero_add] at h + have hf : (fun t : ℝ => Real.exp (-(t + y) ^ 2 / 2)) = fun z => Real.exp (-((z + y) ^ 2 / 2)) := by + funext t; congr 1; ring + rw [hf, h, iteratedDeriv_eq_iterate, Polynomial.deriv_gaussian_eq_hermite_mul_gaussian] + congr 2; ring + +/-- N L53 holds termwise: the image sum of even order is the sum of the termwise 2m-th +derivatives of θ_L at 0. (Exchanging Σ and d/dt is NOT proved here.) -/ +theorem imageSum_even_eq_tsum_termwise (L : ℝ) (m : ℕ) : + imageSum L (2 * m) = + ∑' n : ℤ, iteratedDeriv (2 * m) (fun t => Real.exp (-(t + L * n) ^ 2 / 2)) 0 := by + unfold imageSum + congr 1; funext n + rw [theta_term_iteratedDeriv, pow_mul, neg_one_sq, one_pow, one_mul] + +/- +Poisson link, j = 2, 4, 6 (NOT CLOSED; kept as a statement only): + + theorem imageMoment_eq_dualMoment {L : ℝ} (hL : 0 < L) (j : ℕ) (hj : j = 2 ∨ j = 4 ∨ j = 6) : + imageMoment L j = dualMoment L j + +Route: (i) θ_L(t) = (L²/(2π))^{−1/2} Σ_k e^{−(2πk/L)²/2} cos(2πkt/L) for all t, from +`Complex.tsum_exp_neg_quadratic` with a = L²/(2π), b = −tL/(2π)·(scaling), then real parts; +(ii) differentiate both series j times at t = 0 termwise (`iteratedFDeriv_tsum` / +`hasDerivAt_tsum` in Mathlib.Analysis.Calculus.SmoothSeries, with summable derivative bounds +from `summable_pow_mul_jacobiTheta₂_term_bound`); (iii) identify the image-side j-th derivative +with He_j via `Polynomial.deriv_gaussian_eq_hermite_mul_gaussian` (sign (−1)^j = 1 for even j); +(iv) the dual side gives (−1)^{j/2} Σ w_k ω_k^j. Step (iii) is closed above +(`theta_term_iteratedDeriv`, `imageSum_even_eq_tsum_termwise`). Blocker: steps (i), (ii) are +not formalized here (general-t real form of the Poisson identity; uniform bounds for termwise +j-fold differentiation of both series; step (iv) likewise needs (ii)). Nothing in this comment is claimed proved. +-/ + +end W3Scratch.Side24 diff --git a/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean new file mode 100644 index 000000000..e95ee437d --- /dev/null +++ b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean @@ -0,0 +1,337 @@ +import W3Scratch.Side24Law + +/-! +# W3Scratch.Side24Poisson — SCRATCH / ENGINEERING ONLY + +Grok Bot agent 13, task W3g (Oct 7, 2026). Not reviewed, not aligned, not a discharge. +A Lean lemma ≠ alignment acceptance ≠ discharge. + +Extends `W3Scratch.Side24Law` (W3f). Sources as there (Math- main @ 9fd26113, unchanged at +8d70baa7): N = NOTE.md blob 852f7403 (L21, L53, L54), C = certified_d2.py blob 6fd5b751 +(L137-153, L156-178). Readings R1 (k ∈ ℤ), R2 (sign (-1)^(j/2) from C L153), R3 (c²+s²=1) as in W3f. +New reading R4: N L53 writes θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2} with no sign. Here it is proved +as written for even j (`iteratedDeriv_theta_zero_even`); for odd j the termwise derivative carries +(−1)^j (Mathlib `deriv_gaussian_eq_hermite_mul_gaussian`), which is not used or stated here. +The W3f commented target `imageMoment_eq_dualMoment` (0 < L) is proved below under L ≠ 0. +-/ + +noncomputable section +namespace W3Scratch.Side24 +open ResearchFormalCoreR1 W3Scratch Real +open scoped ContDiff + +/-! ## (a) General-t real θ cosine identity (Poisson summation) -/ + +/-- θ_L(t) = (L²/(2π))^{-1/2} Σ_k w_k cos(2πkt/L) for every real t, L ≠ 0. -/ +theorem theta_eq_cos_series {L : ℝ} (hL : L ≠ 0) (t : ℝ) : + theta L t = 1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) * + ∑' k : ℤ, weight L k * Real.cos (atom L k * t) := by + have ha0 : 0 < L ^ 2 / (2 * π) := by positivity + set a : ℂ := ((L ^ 2 / (2 * π) : ℝ) : ℂ) with ha_def + set b : ℂ := ((-(t * L / (2 * π)) : ℝ) : ℂ) with hb_def + have ha : 0 < a.re := by rw [ha_def, Complex.ofReal_re]; exact ha0 + have h := Complex.tsum_exp_neg_quadratic ha b + have hL1 : ∀ n : ℤ, Complex.exp (-((π : ℝ) : ℂ) * a * (n : ℂ) ^ 2 + 2 * ((π : ℝ) : ℂ) * b * (n : ℂ)) + = ((Real.exp (t ^ 2 / 2) * Real.exp (-(t + L * n) ^ 2 / 2) : ℝ) : ℂ) := by + intro n + rw [Complex.ofReal_mul, Complex.ofReal_exp, Complex.ofReal_exp, ← Complex.exp_add] + congr 1 + rw [ha_def, hb_def]; push_cast + field_simp + ring + have hR1 : ∀ n : ℤ, Complex.exp (-((π : ℝ) : ℂ) / a * ((n : ℂ) + Complex.I * b) ^ 2) + = ((Real.exp (t ^ 2 / 2) : ℝ) : ℂ) * + (((weight L n : ℝ) : ℂ) * Complex.exp (((atom L n * t : ℝ) : ℂ) * Complex.I)) := by + intro n + rw [weight, Complex.ofReal_exp, Complex.ofReal_exp, ← Complex.exp_add, ← Complex.exp_add] + congr 1 + have hLc : (L : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr hL + have hπc : ((π : ℝ) : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr Real.pi_ne_zero + rw [ha_def, hb_def, atom]; push_cast + field_simp + linear_combination (-(L : ℂ) ^ 2 * (t : ℂ) ^ 2) * Complex.I_sq + have hS : Summable fun n : ℤ => + ((weight L n : ℝ) : ℂ) * Complex.exp (((atom L n * t : ℝ) : ℂ) * Complex.I) := by + refine Summable.of_norm ?_ + have : (fun n : ℤ => ‖((weight L n : ℝ) : ℂ) * Complex.exp (((atom L n * t : ℝ) : ℂ) * Complex.I)‖) + = fun n : ℤ => weight L n * atom L n ^ 0 := by + funext n + rw [norm_mul, Complex.norm_exp_ofReal_mul_I, Complex.norm_real, Real.norm_eq_abs, + abs_of_pos (weight_pos L n), pow_zero] + rw [this]; exact summable_weight_mul_atom_pow hL 0 + have hre : (∑' n : ℤ, ((weight L n : ℝ) : ℂ) * + Complex.exp (((atom L n * t : ℝ) : ℂ) * Complex.I)).re = + ∑' k : ℤ, weight L k * Real.cos (atom L k * t) := by + rw [Complex.re_tsum hS] + congr 1; funext n + rw [Complex.re_ofReal_mul, Complex.exp_ofReal_mul_I_re] + have hcp : (1 : ℂ) / a ^ (1 / 2 : ℂ) = (((1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ)) : ℝ) : ℂ) := by + rw [Complex.ofReal_div, Complex.ofReal_one, Complex.ofReal_cpow ha0.le, ha_def] + push_cast; rfl + have hl : ∑' n : ℤ, Complex.exp (-((π : ℝ) : ℂ) * a * (n : ℂ) ^ 2 + 2 * ((π : ℝ) : ℂ) * b * (n : ℂ)) + = ((Real.exp (t ^ 2 / 2) * theta L t : ℝ) : ℂ) := by + rw [tsum_congr hL1, ← Complex.ofReal_tsum, tsum_mul_left]; rfl + have hr : ∑' n : ℤ, Complex.exp (-((π : ℝ) : ℂ) / a * ((n : ℂ) + Complex.I * b) ^ 2) + = ((Real.exp (t ^ 2 / 2) : ℝ) : ℂ) * ∑' n : ℤ, + (((weight L n : ℝ) : ℂ) * Complex.exp (((atom L n * t : ℝ) : ℂ) * Complex.I)) := by + rw [tsum_congr hR1, tsum_mul_left] + rw [hl, hr, hcp] at h + have h2 := congrArg Complex.re h + rw [Complex.ofReal_re, Complex.re_ofReal_mul, Complex.re_ofReal_mul, hre] at h2 + have hE := Real.exp_pos (t ^ 2 / 2) + exact mul_left_cancel₀ hE.ne' (by rw [h2]; ring) + +/-! ## (b) Term-by-term differentiation of both series -/ + +/-- Standard Gaussian e^{-x²/2}, in the form used by Mathlib's Hermite lemma. -/ +def gauss : ℝ → ℝ := fun y => Real.exp (-(y ^ 2 / 2)) + +theorem contDiff_gauss : ContDiff ℝ ∞ gauss := by unfold gauss; fun_prop + +theorem hasDerivAt_iterate_deriv_gauss (j : ℕ) (x : ℝ) : + HasDerivAt (deriv^[j] gauss) (deriv^[j + 1] gauss x) x := by + rw [Function.iterate_succ_apply'] + exact ((contDiff_gauss.iterate_deriv j).differentiable (by simp)).differentiableAt.hasDerivAt + +/-- Every real polynomial is bounded by B e^{|x|}. -/ +theorem poly_exp_bound (p : Polynomial ℤ) : + ∃ B : ℝ, 0 ≤ B ∧ ∀ x : ℝ, |Polynomial.aeval x p| ≤ B * Real.exp |x| := by + induction p using Polynomial.induction_on' with + | add p q hp hq => + obtain ⟨B1, hB1, h1⟩ := hp + obtain ⟨B2, hB2, h2⟩ := hq + refine ⟨B1 + B2, add_nonneg hB1 hB2, fun x => ?_⟩ + rw [map_add] + calc |Polynomial.aeval x p + Polynomial.aeval x q| + ≤ |Polynomial.aeval x p| + |Polynomial.aeval x q| := abs_add_le _ _ + _ ≤ B1 * Real.exp |x| + B2 * Real.exp |x| := add_le_add (h1 x) (h2 x) + _ = (B1 + B2) * Real.exp |x| := by ring + | monomial n c => + refine ⟨|(c : ℝ)| * n.factorial, by positivity, fun x => ?_⟩ + simp only [Polynomial.aeval_monomial, algebraMap_int_eq, Int.coe_castRingHom] + rw [abs_mul, abs_pow, mul_assoc] + refine mul_le_mul_of_nonneg_left ?_ (abs_nonneg _) + have h := Real.pow_div_factorial_le_exp (x := |x|) (abs_nonneg x) n + rw [div_le_iff₀ (by positivity)] at h + linarith [mul_comm (Real.exp |x|) (n.factorial : ℝ)] + +theorem abs_sub_sq_le {L R t : ℝ} (ht : |t| ≤ R) (n : ℤ) : + |t + L * n| - (t + L * n) ^ 2 / 2 ≤ + R + -π * (L ^ 2 / (2 * π) * (n : ℝ) ^ 2 - 2 * ((R + 1) * |L| / (2 * π)) * |(n : ℝ)|) := by + have e : -π * (L ^ 2 / (2 * π) * (n : ℝ) ^ 2 - 2 * ((R + 1) * |L| / (2 * π)) * |(n : ℝ)|) + = -(L * n) ^ 2 / 2 + (R + 1) * |L * n| := by + rw [abs_mul]; field_simp; ring + rw [e] + set m := L * (n : ℝ) + have h1 : |t + m| ≤ |t| + |m| := abs_add_le t m + have h2 : -(t * m) ≤ |t| * |m| := by rw [← abs_mul]; exact neg_le_abs _ + have h3 : |t| * |m| ≤ R * |m| := mul_le_mul_of_nonneg_right ht (abs_nonneg m) + nlinarith [sq_nonneg t, abs_nonneg m] + +/-- Uniform majorant for g^{(j)}(t + Ln) on |t| ≤ R. -/ +theorem iterate_deriv_gauss_bound (j : ℕ) : ∃ B : ℝ, 0 ≤ B ∧ ∀ (L R t : ℝ), |t| ≤ R → ∀ n : ℤ, + ‖deriv^[j] gauss (t + L * n)‖ ≤ B * (Real.exp R * + Real.exp (-π * (L ^ 2 / (2 * π) * (n : ℝ) ^ 2 - 2 * ((R + 1) * |L| / (2 * π)) * |(n : ℝ)|))) := by + obtain ⟨B, hB, hb⟩ := poly_exp_bound (Polynomial.hermite j) + refine ⟨B, hB, fun L R t ht n => ?_⟩ + unfold gauss + rw [Polynomial.deriv_gaussian_eq_hermite_mul_gaussian, Real.norm_eq_abs, abs_mul, abs_mul, + abs_pow, abs_neg, abs_one, one_pow, one_mul, abs_of_pos (Real.exp_pos _)] + calc |Polynomial.aeval (t + L * n) (Polynomial.hermite j)| * Real.exp (-((t + L * n) ^ 2 / 2)) + ≤ B * Real.exp |t + L * n| * Real.exp (-((t + L * n) ^ 2 / 2)) := + mul_le_mul_of_nonneg_right (hb _) (Real.exp_pos _).le + _ = B * Real.exp (|t + L * n| - (t + L * n) ^ 2 / 2) := by + rw [sub_eq_add_neg, Real.exp_add]; ring + _ ≤ B * Real.exp (R + -π * (L ^ 2 / (2 * π) * (n : ℝ) ^ 2 - + 2 * ((R + 1) * |L| / (2 * π)) * |(n : ℝ)|)) := + mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr (abs_sub_sq_le ht n)) hB + _ = _ := by rw [Real.exp_add] + +theorem summable_majorant {L : ℝ} (hL : L ≠ 0) (B R : ℝ) : + Summable fun n : ℤ => B * (Real.exp R * + Real.exp (-π * (L ^ 2 / (2 * π) * (n : ℝ) ^ 2 - 2 * ((R + 1) * |L| / (2 * π)) * |(n : ℝ)|))) := by + have hT : 0 < L ^ 2 / (2 * π) := by positivity + have h := summable_pow_mul_jacobiTheta₂_term_bound ((R + 1) * |L| / (2 * π)) hT 0 + simp only [pow_zero, one_mul, Int.cast_abs] at h + exact (h.mul_left _).mul_left _ + +/-- Termwise j-th derivative series of θ_L: Σ_n g^{(j)}(t + Ln). -/ +def thetaD (L : ℝ) (j : ℕ) (t : ℝ) : ℝ := ∑' n : ℤ, deriv^[j] gauss (t + L * n) + +theorem summable_thetaD_terms {L : ℝ} (hL : L ≠ 0) (j : ℕ) (t : ℝ) : + Summable fun n : ℤ => deriv^[j] gauss (t + L * n) := by + obtain ⟨B, -, hb⟩ := iterate_deriv_gauss_bound j + exact Summable.of_norm_bounded (summable_majorant hL B |t|) (fun n => hb L |t| t le_rfl n) + +theorem hasDerivAt_thetaD {L : ℝ} (hL : L ≠ 0) (j : ℕ) (y : ℝ) : + HasDerivAt (thetaD L j) (thetaD L (j + 1) y) y := by + obtain ⟨B, -, hb⟩ := iterate_deriv_gauss_bound (j + 1) + show HasDerivAt (fun t => ∑' n : ℤ, deriv^[j] gauss (t + L * n)) + (∑' n : ℤ, deriv^[j + 1] gauss (y + L * n)) y + refine hasDerivAt_tsum_of_isPreconnected (g := fun (n : ℤ) t => deriv^[j] gauss (t + L * n)) + (g' := fun (n : ℤ) t => deriv^[j + 1] gauss (t + L * n)) + (summable_majorant hL B (|y| + 1)) Metric.isOpen_ball + (convex_ball y 1).isPreconnected (fun n z _ => ?_) (fun n z hz => ?_) + (Metric.mem_ball_self one_pos) (summable_thetaD_terms hL j y) (Metric.mem_ball_self one_pos) + · have h2 := (hasDerivAt_iterate_deriv_gauss j (z + L * n)).comp z + ((hasDerivAt_id' z).add_const (L * n)) + rw [mul_one] at h2 + exact h2 + · refine hb L (|y| + 1) z ?_ n + rw [Metric.mem_ball, Real.dist_eq] at hz + have := abs_sub_abs_le_abs_sub z y + linarith + +/-- Termwise j-th derivative series of the cosine side: Σ_k w_k ω_k^j cos(ω_k t + jπ/2). -/ +def cosD (L : ℝ) (j : ℕ) (t : ℝ) : ℝ := + ∑' k : ℤ, weight L k * (atom L k ^ j * Real.cos (atom L k * t + j * (π / 2))) + +theorem summable_abs_weight_mul_atom_pow {L : ℝ} (hL : L ≠ 0) (j : ℕ) : + Summable fun k : ℤ => weight L k * |atom L k| ^ j := by + refine (summable_weight_mul_atom_pow hL j).abs.congr (fun k => ?_) + rw [abs_mul, abs_of_pos (weight_pos L k), abs_pow] + +theorem cosD_term_bound (L : ℝ) (j : ℕ) (k : ℤ) (t : ℝ) : + ‖weight L k * (atom L k ^ j * Real.cos (atom L k * t + j * (π / 2)))‖ ≤ + weight L k * |atom L k| ^ j := by + rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_pos (weight_pos L k), abs_pow] + exact mul_le_mul_of_nonneg_left + (mul_le_of_le_one_right (by positivity) (Real.abs_cos_le_one _)) (weight_pos L k).le + +theorem hasDerivAt_cosD {L : ℝ} (hL : L ≠ 0) (j : ℕ) (y : ℝ) : + HasDerivAt (cosD L j) (cosD L (j + 1) y) y := by + show HasDerivAt + (fun t => ∑' k : ℤ, weight L k * (atom L k ^ j * Real.cos (atom L k * t + j * (π / 2)))) + (∑' k : ℤ, weight L k * + (atom L k ^ (j + 1) * Real.cos (atom L k * y + ((j + 1 : ℕ) : ℝ) * (π / 2)))) y + refine hasDerivAt_tsum + (g := fun k t => weight L k * (atom L k ^ j * Real.cos (atom L k * t + j * (π / 2)))) + (g' := fun k t => weight L k * + (atom L k ^ (j + 1) * Real.cos (atom L k * t + ((j + 1 : ℕ) : ℝ) * (π / 2)))) + (summable_abs_weight_mul_atom_pow hL (j + 1)) (fun k z => ?_) + (fun k z => cosD_term_bound L (j + 1) k z) + (Summable.of_norm_bounded (summable_abs_weight_mul_atom_pow hL j) + (fun k => cosD_term_bound L j k y)) y + have h := ((((hasDerivAt_id' z).const_mul (atom L k)).add_const ((j : ℝ) * (π / 2))).cos.const_mul + (atom L k ^ j)).const_mul (weight L k) + convert h using 1 + have e : ((j + 1 : ℕ) : ℝ) * (π / 2) = (j : ℝ) * (π / 2) + π / 2 := by push_cast; ring + rw [e, ← add_assoc, Real.cos_add_pi_div_two] + ring + +theorem thetaD_zero (L t : ℝ) : thetaD L 0 t = theta L t := by + unfold thetaD theta gauss + congr 1; funext n + simp only [Function.iterate_zero, id] + congr 1; ring + +theorem cosD_zero (L t : ℝ) : cosD L 0 t = ∑' k : ℤ, weight L k * Real.cos (atom L k * t) := by + unfold cosD; simp + +/-- Term-by-term differentiation, θ side: iteratedDeriv j θ_L = Σ_n g^{(j)}(· + Ln). -/ +theorem iteratedDeriv_theta {L : ℝ} (hL : L ≠ 0) (j : ℕ) : iteratedDeriv j (theta L) = thetaD L j := by + induction j with + | zero => funext t; rw [iteratedDeriv_zero, thetaD_zero] + | succ j ih => funext t; rw [iteratedDeriv_succ, ih]; exact (hasDerivAt_thetaD hL j t).deriv + +/-- Same, stated as "derivative of the sum = sum of the derivatives". -/ +theorem iteratedDeriv_theta_termwise {L : ℝ} (hL : L ≠ 0) (j : ℕ) (t : ℝ) : + iteratedDeriv j (theta L) t = + ∑' n : ℤ, iteratedDeriv j (fun s => Real.exp (-(s + L * n) ^ 2 / 2)) t := by + rw [iteratedDeriv_theta hL] + unfold thetaD + congr 1; funext n + have h := congrFun (iteratedDeriv_comp_add_const j gauss (L * n)) t + have hf : (fun s : ℝ => Real.exp (-(s + L * n) ^ 2 / 2)) = fun s => gauss (s + L * n) := by + funext s; unfold gauss; congr 1; ring + rw [hf, h, iteratedDeriv_eq_iterate] + +/-- Term-by-term differentiation, cosine side. -/ +theorem iteratedDeriv_cos_series {L : ℝ} (hL : L ≠ 0) (j : ℕ) : + iteratedDeriv j (fun t => ∑' k : ℤ, weight L k * Real.cos (atom L k * t)) = cosD L j := by + induction j with + | zero => funext t; rw [iteratedDeriv_zero, cosD_zero] + | succ j ih => funext t; rw [iteratedDeriv_succ, ih]; exact (hasDerivAt_cosD hL j t).deriv + +/-- Poisson identity for every termwise derivative (all j, all t). -/ +theorem thetaD_eq_cosD {L : ℝ} (hL : L ≠ 0) (j : ℕ) (t : ℝ) : + thetaD L j t = 1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) * cosD L j t := by + induction j generalizing t with + | zero => rw [thetaD_zero, cosD_zero]; exact theta_eq_cos_series hL t + | succ j ih => + have h1 := hasDerivAt_thetaD hL j t + have hf : thetaD L j = fun s => 1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) * cosD L j s := funext ih + rw [hf] at h1 + exact h1.unique ((hasDerivAt_cosD hL j t).const_mul _) + +/-! ## (c) θ-route moments = dual-law moments -/ + +theorem imageSum_even_eq_thetaD (L : ℝ) (m : ℕ) : imageSum L (2 * m) = thetaD L (2 * m) 0 := by + unfold imageSum thetaD gauss + congr 1; funext n + rw [Polynomial.deriv_gaussian_eq_hermite_mul_gaussian, zero_add, pow_mul, neg_one_sq, one_pow, + one_mul, neg_div] + +/-- N L53 as written, for even order: θ_L^{(2m)}(0) = Σ_n He_{2m}(Ln) e^{−(Ln)²/2}. -/ +theorem iteratedDeriv_theta_zero_even {L : ℝ} (hL : L ≠ 0) (m : ℕ) : + iteratedDeriv (2 * m) (theta L) 0 = imageSum L (2 * m) := by + rw [iteratedDeriv_theta hL, imageSum_even_eq_thetaD] + +theorem cosD_even_zero (L : ℝ) (m : ℕ) : + cosD L (2 * m) 0 = (-1) ^ m * rawSum (weight L) (atom L) (2 * m) := by + unfold cosD rawSum + have hc : Real.cos (((2 * m : ℕ) : ℝ) * (π / 2)) = (-1) ^ m := by + rw [show ((2 * m : ℕ) : ℝ) * (π / 2) = (m : ℝ) * π by push_cast; ring] + exact Real.cos_nat_mul_pi m + simp only [mul_zero, zero_add, hc] + rw [← tsum_mul_left]; congr 1; funext k; ring + +theorem imageSum_even_eq {L : ℝ} (hL : L ≠ 0) (m : ℕ) : + imageSum L (2 * m) = 1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) * + ((-1) ^ m * rawSum (weight L) (atom L) (2 * m)) := by + rw [imageSum_even_eq_thetaD, thetaD_eq_cosD hL, cosD_even_zero] + +/-- The link: θ-route moment (N L53 / C L153) = dual-law moment (N L54 / C L156-178), every even +order, every L ≠ 0. -/ +theorem imageMoment_even_eq_dualMoment {L : ℝ} (hL : L ≠ 0) (m : ℕ) : + imageMoment L (2 * m) = dualMoment L (2 * m) := by + have hA0 : (1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) : ℝ) ≠ 0 := by + have : 0 < (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) := Real.rpow_pos_of_pos (by positivity) _ + positivity + have h2m := imageSum_even_eq hL m + have h0 := imageSum_even_eq hL 0 + rw [mul_zero, pow_zero, one_mul] at h0 + have hs : ((-1 : ℝ) ^ m) ^ 2 = 1 := by rw [← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow] + unfold imageMoment dualMoment lawMoment + rw [show 2 * m / 2 = m by omega, h2m, h0] + rw [show (-1 : ℝ) ^ m * (1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) * + ((-1) ^ m * rawSum (weight L) (atom L) (2 * m))) = + ((-1 : ℝ) ^ m) ^ 2 * (1 / (L ^ 2 / (2 * π)) ^ (1 / 2 : ℝ) * + rawSum (weight L) (atom L) (2 * m)) by ring, hs, one_mul, mul_div_mul_left _ _ hA0] + +/-- j = 2, 4, 6 (the W3f commented target, now with L ≠ 0 instead of 0 < L). -/ +theorem imageMoment_eq_dualMoment {L : ℝ} (hL : L ≠ 0) (j : ℕ) (hj : j = 2 ∨ j = 4 ∨ j = 6) : + imageMoment L j = dualMoment L j := by + rcases hj with rfl | rfl | rfl + · exact imageMoment_even_eq_dualMoment hL 1 + · exact imageMoment_even_eq_dualMoment hL 2 + · exact imageMoment_even_eq_dualMoment hL 3 + +/-- Corollary: the θ-route moments satisfy 0 < m2, m2² < m4, Δ > 0 for every L ≠ 0. -/ +theorem image_moment_hyps {L : ℝ} (hL : L ≠ 0) : + 0 < imageMoment L 2 ∧ imageMoment L 2 ^ 2 < imageMoment L 4 ∧ + 0 < d2Delta (imageMoment L 2) (imageMoment L 4) (imageMoment L 6) := by + rw [imageMoment_eq_dualMoment hL 2 (Or.inl rfl), imageMoment_eq_dualMoment hL 4 (Or.inr (Or.inl rfl)), + imageMoment_eq_dualMoment hL 6 (Or.inr (Or.inr rfl))] + exact dual_moment_hyps hL + +/-- Corollary: every-direction positivity for the θ-route moments, every L ≠ 0 (R3: c²+s²=1). -/ +theorem image_positivity_every_direction {L : ℝ} (hL : L ≠ 0) (c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : + 0 < d2DetV (imageMoment L 2) (imageMoment L 4) (srcQ c s) ∧ + 0 < d2Schur (imageMoment L 2) (imageMoment L 4) (srcQ c s) ∧ + 0 < d2Tau (imageMoment L 2) (imageMoment L 4) (imageMoment L 6) (srcQ c s) := by + rw [imageMoment_eq_dualMoment hL 2 (Or.inl rfl), imageMoment_eq_dualMoment hL 4 (Or.inr (Or.inl rfl)), + imageMoment_eq_dualMoment hL 6 (Or.inr (Or.inr rfl))] + exact dual_positivity_every_direction hL c s hu + +end W3Scratch.Side24 From 5735c10e6e327efc0423df1e69c0a16eb09d50ee Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Thu, 8 Oct 2026 03:20:38 +0000 Subject: [PATCH 2/2] reviews: W3 SIDE24 proposal amend 1 (README and Lean comments only, per Math-#403 reader 6051288028) Co-authored-by: Dylan Roy --- .../README.md | 63 ++++++++++++++----- .../W3Scratch/D2SchurLinks.lean | 5 +- .../W3Scratch/Side24Law.lean | 40 +++++------- .../W3Scratch/Side24Poisson.lean | 17 +++-- 4 files changed, 77 insertions(+), 48 deletions(-) diff --git a/reviews/w3_side24_source_proposal_20261008/README.md b/reviews/w3_side24_source_proposal_20261008/README.md index 3d0ab1113..c195a4b3a 100644 --- a/reviews/w3_side24_source_proposal_20261008/README.md +++ b/reviews/w3_side24_source_proposal_20261008/README.md @@ -11,23 +11,27 @@ credit 0; sci NONE; eng≠discharge; no flags; OBL OPEN - That decision does **not** accept R1–R4, the spectral-law interpretation, any theorem or alignment claim, or option A's formal registration. Nothing here changes that. - Nothing under `formal/`, no lakefile, manifest, root import, test, workflow, GRAPH or STATUS file is touched. These modules are **not** part of `ResearchFormalCoreR1`, are **not** built by any workflow, and ordinary PR CI does **not** certify them. - No status field (lemma_closed, prizes_solved, discharges_OBL_H5_JETMOD, certified_C_H, freeze, inventable_attempt_accepted, alignment) is changed or proposed to change. OBL OPEN. -- All evidence below is the author's own, box-local, and **UNVERIFIED** by any nonauthor. +- The build, axiom and gate evidence under "Existing evidence and failures" is the author's own, box-local, and **UNVERIFIED** by any nonauthor. One Grok-Bot-on-Grok-Bot reader verdict exists for the previous head (see "Amend 1" below); organizational-independence credit 0, nothing accepted. ## Author and exposure -- Author: Grok Bot agent 13 (Grok Bot support agent; non-Claude, nonauthor lane), tasks W3d–W3g, Oct 7 2026 (CT). +- Author: Grok Bot agent 13 (Grok Bot support agent; W3 scratch author), tasks W3d–W3g, Oct 7 2026 (CT). Earlier footers that read "non-Claude, nonauthor lane" were inaccurate; the factual correction, covering those footers and the actual publication order (push, then readback, then pickup 6050962170), is [403/6051150390](https://github.com/d6g8k5htny-coder/Math-/pull/403#issuecomment-6051150390). The order stands as it happened and is not redone. - The author wrote all three `.lean` files and has read the sources cited below. - Reports: W3d [6050271678](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050271678), W3e [6050351089](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050351089), W3f [6050458079](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050458079), W3g [6050559869](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050559869). CoS decision request: [6050565322](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6050565322). ## Identities -### Files (bytes and namespaces unchanged from the reported W3e/W3f/W3g sources) +### Files (amend 1: comment-only diffs from the reported W3e/W3f/W3g sources) -| Path (under this directory) | sha256 | bytes | lines | namespace | task | +Since amend 1 the three `.lean` files are **no longer byte-identical** to agent 13's reported scratch copies. The diffs are confined to comments and docstrings: no Lean statement, proof term, declaration name, import or namespace changed. A mechanical check strips all comments and docstrings from the old and new files, drops blank lines, and finds the remaining code byte-identical in all three files (stripped-code sha256: D2SchurLinks `fe3e63e2…`, Side24Law `0dde2848…`, Side24Poisson `2cc80313…`, the same before and after). + +| Path (under this directory) | sha256 (amend 1) | bytes | lines | namespace | task | |---|---|---|---|---|---| -| `W3Scratch/D2SchurLinks.lean` | `06b28be4725a72f7915a7fe3077f2d562c809c63c4a5acbd1c79bcc923d9dbda` | 19449 | 387 | `W3Scratch` | W3d + W3e | -| `W3Scratch/Side24Law.lean` | `8678ddd4d58e123d4e0b1bb829a56d00eb7c281c95ba0eef45efa3086d7756d7` | 14497 | 286 | `W3Scratch.Side24` | W3f | -| `W3Scratch/Side24Poisson.lean` | `47b65188977a251ebd8ae92d14e4b1109b6695b5e0daf48d6f50ee26554fcb86` | 18074 | 337 | `W3Scratch.Side24` | W3g | +| `W3Scratch/D2SchurLinks.lean` | `628260ba01ae2cedf2f89478faddb4426ebbfb054aa7d64d983da237c124f00e` | 19735 | 390 | `W3Scratch` | W3d + W3e | +| `W3Scratch/Side24Law.lean` | `97dd915fdcdc78b8242f60bd93005ba854f1fc24c2db9da5df6bedfd20eef0a7` | 13899 | 274 | `W3Scratch.Side24` | W3f | +| `W3Scratch/Side24Poisson.lean` | `45377ccfd156d4342d9e5aee0f90843f46f015436e7f2aa80779c1ed1a02a87d` | 18488 | 342 | `W3Scratch.Side24` | W3g | + +Previous head `0b3363840081baee55881dbfdf0ae606f57c594d` (the reported scratch bytes): D2SchurLinks `06b28be4725a72f7915a7fe3077f2d562c809c63c4a5acbd1c79bcc923d9dbda` (19449 B, 387 lines), Side24Law `8678ddd4d58e123d4e0b1bb829a56d00eb7c281c95ba0eef45efa3086d7756d7` (14497 B, 286 lines), Side24Poisson `47b65188977a251ebd8ae92d14e4b1109b6695b5e0daf48d6f50ee26554fcb86` (18074 B, 337 lines). All three end in a single LF; none contains CR. @@ -47,8 +51,10 @@ All three end in a single LF; none contains CR. ### Sources formalized (Math- blobs) -- N = `reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md`, blob `852f7403a8a06a1ef061e363df9502ae16f7a341` (L21, L22, L23, L26, L30, L53, L54). -- C = `reviews/side24_d2_certified_small_L_claude_20261005/certified_d2.py`, blob `6fd5b751cc4157136ae92225838c12d33dc997f3` (L8, L111–122, L137–153, L156–178). +- N = `reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md`, blob `852f7403a8a06a1ef061e363df9502ae16f7a341`. Lines cited in the modules (amend 1, each checked against the blob at `7014efec`): L17, L21, L22, L23, L24, L26, L27, L28, L30, L34, L35, L36, L43, L48, L53, L54, L59, L65–73, L78. Of these, L17, L24, L27 and L65–73 are first cited in amend 1. +- C = `reviews/side24_d2_certified_small_L_claude_20261005/certified_d2.py`, blob `6fd5b751cc4157136ae92225838c12d33dc997f3` (L8, L12, L13, L111–121, L137–153, L144, L153, L156–177, L176–177). + - Pin erratum fixed in amend 1: `Side24Law.lean` cited `C L178` for `dualMoment`; C's `return w[2]/w[0]…` is at L176–177 (L178 is blank). The ranges L156–178 and L111–122 likewise ended on blank lines and now read L156–177 and L111–121. +- iba1 NOTE = `reviews/iba1_periodic_jet_claude_20261005/NOTE.md`, blob `e36e341f4f7b2781ef3bbcb0df8580ac17f85f8b` (L29, L32; cited in amend 1). - Math-#302 comment 6005199919 (body sha256 `28f5d504...`), as cited in `D2SchurLinks.lean`. ## Declaration inventory @@ -68,6 +74,10 @@ All three end in a single LF; none contains CR. - defs: `gauss`, `thetaD`, `cosD`. - theorems: `theta_eq_cos_series`, `contDiff_gauss`, `hasDerivAt_iterate_deriv_gauss`, `poly_exp_bound`, `abs_sub_sq_le`, `iterate_deriv_gauss_bound`, `summable_majorant`, `summable_thetaD_terms`, `hasDerivAt_thetaD`, `summable_abs_weight_mul_atom_pow`, `cosD_term_bound`, `hasDerivAt_cosD`, `thetaD_zero`, `cosD_zero`, `iteratedDeriv_theta`, `iteratedDeriv_theta_termwise`, `iteratedDeriv_cos_series`, `thetaD_eq_cosD`, `imageSum_even_eq_thetaD`, `iteratedDeriv_theta_zero_even`, `cosD_even_zero`, `imageSum_even_eq`, `imageMoment_even_eq_dualMoment`, `imageMoment_eq_dualMoment`, `image_moment_hyps`, `image_positivity_every_direction`. +### Stale comments removed (amend 1) + +Previous head: `Side24Law.lean` L259–260 ("Exchanging Σ and d/dt is NOT proved here") and L268–284 (the "NOT CLOSED" commented target `imageMoment_eq_dualMoment`) recorded the W3f state, which `Side24Poisson.lean` closes (`iteratedDeriv_theta`, `iteratedDeriv_theta_zero_even`, and `imageMoment_eq_dualMoment` under L ≠ 0). Amend 1 replaces the first with a pointer to those theorems and deletes the second block. Both were comments, so no declaration changed. + ## Portable isolated build (scratch copy only; never commit these edits) 1. Clone Math- and check out `7014efec8fb68cc926350caa8fa65dcd296f7f63` in a throwaway directory. @@ -87,6 +97,8 @@ This edits `formal/lakefile.toml` and adds unregistered modules, so in that copy Each build ran under a process-tree RSS watchdog with a 6.5 GB limit. No build in W3d–W3g was killed by it. +The W3d–W3g runs below used the previous (pre-amend) bytes; the amend-1 build and axiom check of the current bytes is under "Amend 1". + ### Builds - **W3d** (prototype `W3dScratch.lean`, sha256 `3846f5bf...`; not included here; its D2Schur results reappear in `D2SchurLinks.lean`): run 1 failed (wrong import path, 0.59 GB); run 2 exit 0 (2.87 GB, 20 s); run 3 exit 0 (2.91 GB, 15.1 s). @@ -116,14 +128,35 @@ The only axioms allowed were propext, Classical.choice and Quot.sound. A text se The decision accepts none of these. -- **R1.** k ∈ ℤ for the dual law (N L54 gives no range; C L156–178 sums k = 0 plus 2× k ≥ 1, the symmetric ℤ-sum). -- **R2.** The sign (−1)^(j/2) in the θ-route moment follows C L153 (`moments_image`), not N. -- **R3.** c² + s² = 1 for the direction u = (c, s) (N L26 does not write it). Without it the `d2DetV`-in-e identity fails, and `d2DetV_eq_alpha_gamma_e_needs_unit` gives a counterexample. -- **R4.** N L53's unsigned formula θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2} is proved as written for even j only (`iteratedDeriv_theta_zero_even`). For odd j the termwise derivative carries (−1)^j; that case is not stated. +Amend 1 reframes R2–R4 per reader verdict [403/6051288028](https://github.com/d6g8k5htny-coder/Math-/pull/403#issuecomment-6051288028) (items A1–A3) and CoS correction [main#229 6051296820](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6051296820). Only R1 and the analytic-correspondence questions stand as open questions. + +- **R1 (open).** k ∈ ℤ for the dual law (N L54 gives no range; C L156–177 sums k = 0 plus 2× k ≥ 1, the symmetric ℤ-sum). +- **R2 (source-stated, not a free reading).** The sign (−1)^(j/2) in the θ-route moment is stated in C L153 (`moments_image`) and in iba1 NOTE (blob `e36e341f`) L32 (`m2 = -q2, m4 = q4, m6 = -q6`), whose conventions N L24 and C L13 adopt. N does not write it directly. +- **R3 (source-supported).** c² + s² = 1 for u = (c, s). N L26 does not write it, but C L12 states `u = (cos t, sin t)`, N L43 parametrizes u by angle, and N L27's `Σu⁴ = 1 − 2q` holds iff c² + s² = 1 (residual (c² + s² − 1)(c² + s² + 1)). Without it the `d2DetV`-in-e identity fails, and `d2DetV_eq_alpha_gamma_e_needs_unit` gives a counterexample. +- **R4 (not a discrepancy).** N L53's unsigned formula θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2} is formalized for even j only (`iteratedDeriv_theta_zero_even`). For odd j it also holds as written (not formalized): reindexing n → −n with He_j(−x) = (−1)^j He_j(x) removes the termwise (−1)^j, and both sides vanish because θ_L is even. N and C use only j = 0, 2, 4, 6 (C L144; iba1 NOTE L29). - **Analytic correspondence.** - (a) Is the W3f dual law (`atom`, `weight`, `dualZ`) the NOTE's "spectral law" (N L22, L54)? - (b) Do the literal source objects (`k2`/`k4`/`k6`, `srcAlpha`, `srcGamma`, `srcQ`, `srcE`, `srcSchur`, `srcTau`, `theta`, `imageSum`, `imageMoment`) faithfully transcribe N and C? - - (c) Does "positivity in every direction for every L ≠ 0" (`dual_positivity_every_direction`, `image_positivity_every_direction`) correspond to anything the source certifies? The source certifies numerically at specific L only. + - (c) Does "positivity in every direction for every L ≠ 0" (`dual_positivity_every_direction`, `image_positivity_every_direction`) correspond to anything the source certifies? The source certifies numerically, by interval enclosures, at the six values L ∈ {24, 8, 2π, 4, 3, 2} only (N L17, L59, L65–73, L78). Amend 1 rescopes the `dual_positivity_every_direction` docstring (previously `Side24Law.lean` L210–211, which called the all-L statement "the NOTE's" positivity) accordingly; do not cite that docstring as a source-backed claim. - A box-local follow-up compares the dual law with the moment characterization in `reviews/iba1_periodic_jet_claude_20261005/NOTE.md` L26–32. It is not part of this proposal, and the measure-level identification is open. -— Grok Bot agent 13 (Grok Bot support agent; non-Claude, nonauthor lane) +## Amend 1 (after reader verdict 403/6051288028) + +Reader: Grok Bot agent 3, verdict AMEND (README/comments only) at previous head `0b336384`: isolated `lake build W3Scratch` exit 0, `#print axioms` on all 101 declarations gave only `[propext, Classical.choice, Quot.sound]`, transcriptions faithful. This is a Grok-Bot-on-Grok-Bot read: organizational-independence credit 0; it accepts none of R1–R4, the spectral-law interpretation, registration, status or integration. Routed by CoS [main#229 6051296820](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6051296820); pause notice [403/6051309079](https://github.com/d6g8k5htny-coder/Math-/pull/403#issuecomment-6051309079). + +| Item | Where | Done in amend 1 | +|---|---|---| +| A1 (R2) | README R2; `Side24Law.lean` header; `Side24Poisson.lean` header | Cites C L153 and iba1 NOTE L32, adopted via N L24 / C L13 | +| A2 (R3) | README R3; `D2SchurLinks.lean` header; `Side24Poisson.lean` header | Cites C L12, N L43, N L27 residual | +| A3 (R4) | README R4; `Side24Poisson.lean` header | Odd j holds as written (not formalized); not a discrepancy | +| A4 (pin) | `Side24Law.lean` `dualMoment` docstring; README C pins | C L178 → C L176–177 (also L156–178 → L156–177, L111–122 → L111–121) | +| A5 (N lines) | README N pins | Complete list, each line checked against blob `852f7403` | +| A6 (stale blocks) | `Side24Law.lean` | Removed (see "Stale comments removed") | +| A7 (footer) | README author line and footer | "W3 scratch author"; correction 403/6051150390 referenced | +| Docstring scope | `Side24Law.lean` `dual_positivity_every_direction` | Scoped: N certifies six L values only; the all-L statement is new | + +Author's amend-1 check (box-local, UNVERIFIED by any nonauthor): in a scratch copy of `formal/` (Lean 4.34.1, mathlib `d13f23b7`; lakefile root appended in the copy only), `lake build` of `W3Scratch.D2SchurLinks`, `W3Scratch.Side24Law` and `W3Scratch.Side24Poisson`, one module at a time (`nice -n 10`, `LEAN_NUM_THREADS=1`, 6.5 GB RSS watchdog): each exit 0 (159 s / 3.69 GB, 135 s / 4.25 GB, 158 s / 4.20 GB), no warnings in W3Scratch, no watchdog kill. `#print axioms` on all 101 declarations above (`lake env lean`): exit 0, all 101 exactly `[propext, Classical.choice, Quot.sound]`. No `sorry`, `admit`, `native_decide` or `axiom` tokens. The comment-only code-identity check is the primary evidence that no declaration changed. + +credit 0; sci NONE; eng≠discharge; no flags; OBL OPEN + +— Grok Bot agent 13 (Grok Bot support agent; W3 scratch author) diff --git a/reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean b/reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean index 904fdd2c6..88d9bdeac 100644 --- a/reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean +++ b/reviews/w3_side24_source_proposal_20261008/W3Scratch/D2SchurLinks.lean @@ -16,7 +16,10 @@ the source objects of reviews/side24_d2_certified_small_L_claude_20261005/NOTE.m Readings used (stated, not claimed as the author's intent): * NOTE L23 cumulant formulas are those of a symmetric coordinate law (odd moments zero). -* NOTE L26: u = (c, s) is a unit direction, c² + s² = 1 (not written in the NOTE). +* NOTE L26: u = (c, s) is a unit direction, c² + s² = 1. The NOTE does not write it at L26, but the + sources support it: C (certified_d2.py, blob 6fd5b751) L12 states u = (cos t, sin t), NOTE L43 + parametrizes u by an angle, and NOTE L27's Σu⁴ = 1 − 2q holds iff c² + s² = 1 (the residual is + (c² + s² − 1)(c² + s² + 1)). Reader 403/6051288028 item A2. -/ noncomputable section diff --git a/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean index 26b35e0ac..f94945d12 100644 --- a/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean +++ b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Law.lean @@ -16,12 +16,15 @@ Merged sources only, Math- main @ 9fd261135b41daf1e377f9ef2db193fee6ec36be: - N L53: `θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2}` (image sums). - N L54: Poisson-dual law `P(X = 2πk/L) ∝ e^{−(2πk/L)²/2}`. * C = reviews/side24_d2_certified_small_L_claude_20261005/certified_d2.py, blob 6fd5b751cc4157136ae92225838c12d33dc997f3 - - C L8: same θ_L as N L21. C L111-122: He_2, He_4, He_6 (probabilists' Hermite). + - C L8: same θ_L as N L21. C L111-121: He_2, He_4, He_6 (probabilists' Hermite). - C L137-153 `moments_image`: returns `(-θ2/θ0, θ4/θ0, -θ6/θ0)`, i.e. m_j = (-1)^(j/2) θ^{(j)}(0)/θ(0). - - C L156-178 `moments_dual`: weights 1 (k = 0) and 2 e^{−(hk)²/2} (k ≥ 1), h = 2π/L; m_j = Σ w ω^j / Σ w. + - C L156-177 `moments_dual`: weights 1 (k = 0) and 2 e^{−(hk)²/2} (k ≥ 1), h = 2π/L; m_j = Σ w ω^j / Σ w. Readings (flagged): k ranges over ℤ (N L54 gives no range; C sums k = 0 plus 2× k ≥ 1, which is -the symmetric ℤ-sum). The θ-route moment formula with the sign (-1)^(j/2) is from C L153, not N. +the symmetric ℤ-sum). The θ-route moment formula with the sign (-1)^(j/2) is stated in C L153 +(`moments_image`) and in iba1 NOTE (reviews/iba1_periodic_jet_claude_20261005/NOTE.md, blob +e36e341f) L32 (m2 = −q2, m4 = q4, m6 = −q6), whose conventions N L24 and C L13 adopt; N does not +write it directly. Reader 403/6051288028 item A1. -/ noncomputable section @@ -129,7 +132,7 @@ theorem countable_law_moment_hyps (hw : ∀ i, 0 ≤ w i) end Generic -/-! ## The SIDE24 Poisson-dual law (N L54; C L156-178) -/ +/-! ## The SIDE24 Poisson-dual law (N L54; C L156-177) -/ /-- Atom 2πk/L (N L54). -/ def atom (L : ℝ) (k : ℤ) : ℝ := 2 * π * k / L @@ -137,7 +140,7 @@ def atom (L : ℝ) (k : ℤ) : ℝ := 2 * π * k / L def weight (L : ℝ) (k : ℤ) : ℝ := Real.exp (-(atom L k) ^ 2 / 2) /-- Normalizer Σ_k e^{−(2πk/L)²/2}. -/ def dualZ (L : ℝ) : ℝ := rawSum (weight L) (atom L) 0 -/-- Raw moment m_n(L) of the dual law (C L178: w[j]/w[0]). -/ +/-- Raw moment m_n(L) of the dual law (C L176-177: w[j]/w[0]). -/ def dualMoment (L : ℝ) (n : ℕ) : ℝ := lawMoment (weight L) (atom L) n theorem weight_pos (L : ℝ) (k : ℤ) : 0 < weight L k := Real.exp_pos _ @@ -207,8 +210,10 @@ theorem dual_moment_hyps {L : ℝ} (hL : L ≠ 0) : exact countable_law_moment_hyps (fun k => (weight_pos L k).le) (summable_weight_mul_atom_pow hL) 1 2 (weight_pos L 1) (weight_pos L 2) h1 h2 h12 -/-- The NOTE's "positive in every direction" (N L59, L78; certified numerically at six L) holds for -the dual-law moments at EVERY nonzero L. -/ +/-- Every-direction positivity for the exact dual-law moments, at every nonzero L. This is a new +all-L ≠ 0 statement. N certifies "positive in every direction" (N L59, L78) only numerically, by +interval enclosures, at the six values L ∈ {24, 8, 2π, 4, 3, 2} (N L17, L65-73); this theorem is +not that certificate, and identifying the two needs analytic question (a) of the README. -/ theorem dual_positivity_every_direction {L : ℝ} (hL : L ≠ 0) (c s : ℝ) (hu : c ^ 2 + s ^ 2 = 1) : 0 < d2DetV (dualMoment L 2) (dualMoment L 4) (srcQ c s) ∧ 0 < d2Schur (dualMoment L 2) (dualMoment L 4) (srcQ c s) ∧ @@ -257,7 +262,8 @@ theorem theta_term_iteratedDeriv (y : ℝ) (j : ℕ) : congr 2; ring /-- N L53 holds termwise: the image sum of even order is the sum of the termwise 2m-th -derivatives of θ_L at 0. (Exchanging Σ and d/dt is NOT proved here.) -/ +derivatives of θ_L at 0. (The exchange of Σ and d/dt, for L ≠ 0, is in `Side24Poisson`: +`iteratedDeriv_theta`, `iteratedDeriv_theta_zero_even`.) -/ theorem imageSum_even_eq_tsum_termwise (L : ℝ) (m : ℕ) : imageSum L (2 * m) = ∑' n : ℤ, iteratedDeriv (2 * m) (fun t => Real.exp (-(t + L * n) ^ 2 / 2)) 0 := by @@ -265,22 +271,4 @@ theorem imageSum_even_eq_tsum_termwise (L : ℝ) (m : ℕ) : congr 1; funext n rw [theta_term_iteratedDeriv, pow_mul, neg_one_sq, one_pow, one_mul] -/- -Poisson link, j = 2, 4, 6 (NOT CLOSED; kept as a statement only): - - theorem imageMoment_eq_dualMoment {L : ℝ} (hL : 0 < L) (j : ℕ) (hj : j = 2 ∨ j = 4 ∨ j = 6) : - imageMoment L j = dualMoment L j - -Route: (i) θ_L(t) = (L²/(2π))^{−1/2} Σ_k e^{−(2πk/L)²/2} cos(2πkt/L) for all t, from -`Complex.tsum_exp_neg_quadratic` with a = L²/(2π), b = −tL/(2π)·(scaling), then real parts; -(ii) differentiate both series j times at t = 0 termwise (`iteratedFDeriv_tsum` / -`hasDerivAt_tsum` in Mathlib.Analysis.Calculus.SmoothSeries, with summable derivative bounds -from `summable_pow_mul_jacobiTheta₂_term_bound`); (iii) identify the image-side j-th derivative -with He_j via `Polynomial.deriv_gaussian_eq_hermite_mul_gaussian` (sign (−1)^j = 1 for even j); -(iv) the dual side gives (−1)^{j/2} Σ w_k ω_k^j. Step (iii) is closed above -(`theta_term_iteratedDeriv`, `imageSum_even_eq_tsum_termwise`). Blocker: steps (i), (ii) are -not formalized here (general-t real form of the Poisson identity; uniform bounds for termwise -j-fold differentiation of both series; step (iv) likewise needs (ii)). Nothing in this comment is claimed proved. --/ - end W3Scratch.Side24 diff --git a/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean index e95ee437d..881e82f3a 100644 --- a/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean +++ b/reviews/w3_side24_source_proposal_20261008/W3Scratch/Side24Poisson.lean @@ -8,11 +8,16 @@ A Lean lemma ≠ alignment acceptance ≠ discharge. Extends `W3Scratch.Side24Law` (W3f). Sources as there (Math- main @ 9fd26113, unchanged at 8d70baa7): N = NOTE.md blob 852f7403 (L21, L53, L54), C = certified_d2.py blob 6fd5b751 -(L137-153, L156-178). Readings R1 (k ∈ ℤ), R2 (sign (-1)^(j/2) from C L153), R3 (c²+s²=1) as in W3f. -New reading R4: N L53 writes θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2} with no sign. Here it is proved -as written for even j (`iteratedDeriv_theta_zero_even`); for odd j the termwise derivative carries -(−1)^j (Mathlib `deriv_gaussian_eq_hermite_mul_gaussian`), which is not used or stated here. -The W3f commented target `imageMoment_eq_dualMoment` (0 < L) is proved below under L ≠ 0. +(L137-153, L156-177). Reading R1 (k ∈ ℤ) as in W3f. The sign (-1)^(j/2) is stated in C L153 and +iba1 NOTE (blob e36e341f) L32; c²+s²=1 is supported by C L12 (see W3f and reader 403/6051288028). +N L53 writes θ_L^{(j)}(0) = Σ_n He_j(Ln) e^{−(Ln)²/2} with no sign. Here it is formalized for even j +(`iteratedDeriv_theta_zero_even`). For odd j it also holds as written (not formalized here): +the termwise derivative carries (−1)^j (Mathlib `deriv_gaussian_eq_hermite_mul_gaussian`), and +reindexing n → −n with He_j(−x) = (−1)^j He_j(x) removes it; both sides vanish because θ_L is even. +So this is not a source discrepancy (reader 403/6051288028 item A3). N and C use only +j = 0, 2, 4, 6 (C L144; iba1 NOTE L29). +The W3f commented target `imageMoment_eq_dualMoment` (0 < L) is proved below under L ≠ 0. (That +stale W3f comment block was removed from Side24Law.lean in the Math-#403 amend.) -/ noncomputable section @@ -291,7 +296,7 @@ theorem imageSum_even_eq {L : ℝ} (hL : L ≠ 0) (m : ℕ) : ((-1) ^ m * rawSum (weight L) (atom L) (2 * m)) := by rw [imageSum_even_eq_thetaD, thetaD_eq_cosD hL, cosD_even_zero] -/-- The link: θ-route moment (N L53 / C L153) = dual-law moment (N L54 / C L156-178), every even +/-- The link: θ-route moment (N L53 / C L153) = dual-law moment (N L54 / C L156-177), every even order, every L ≠ 0. -/ theorem imageMoment_even_eq_dualMoment {L : ℝ} (hL : L ≠ 0) (m : ℕ) : imageMoment L (2 * m) = dualMoment L (2 * m) := by