Mister-Meeseeks · Oct 20, 2026 · Oct 19, 2026
diff --git a/research/gaussian-expansion-headroom/INPUTS.json b/research/gaussian-expansion-headroom/INPUTS.json
@@ -0,0 +1,9 @@
+{
+  "schema_version": 1,
+  "sha256": {
+    "vendor/intervals.py": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df",
+    "vendor/NOTICE.md": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d",
+    "inputs/PR3763-PROOF.md": "92cccf922e0e79fcffc5b6883812c6c5f162565c926f9d807791f6b850ac0951",
+    "inputs/PR3851-README.md": "ce063e3796bdcea206959918915826ae75c1bcbd74736913e5b330aa04fb5791"
+  }
+}
diff --git a/research/gaussian-expansion-headroom/LIBRARY-BRIDGES.json b/research/gaussian-expansion-headroom/LIBRARY-BRIDGES.json
@@ -0,0 +1,174 @@
+{
+  "schema_version": 1,
+  "mathlib_revision": "db584cd6d46c92f209a44c0f1c829460d327499d",
+  "sources": [
+    {
+      "environment": "mathlib",
+      "module_path": "Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean",
+      "sha256": "eaae5fe1c1a674c2023ad71464e2534b11af0c29025b4c91078c36f3b684f8e8",
+      "declarations": [
+        "fourierIntegral_gaussian",
+        "fourier_gaussian_pi'"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "mathlib",
+      "module_path": "Mathlib/Analysis/Fourier/PoissonSummation.lean",
+      "sha256": "762870e46548e526fc0903e82cadd396bb6b3906ae4327d215e547baba370c22",
+      "declarations": [
+        "Real.tsum_eq_tsum_fourier"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "mathlib",
+      "module_path": "Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean",
+      "sha256": "3edb45218f7ef07955b8d192bda228d81d2435c591ef8d3c0cf1712c3f8858ff",
+      "declarations": [
+        "Complex.tsum_exp_neg_quadratic"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "mathlib",
+      "module_path": "Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean",
+      "sha256": "dcca1cfcf40d14c027c8403335b67d4b8d195cbb501e855fd306820f5ad825b8",
+      "declarations": [
+        "norm_jacobiTheta_sub_one_le"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "external",
+      "module_path": "ErdosProblems/Erdos230/GaussianPoisson.lean",
+      "sha256": "87e9f1c3426988934bb47bde9afbd84d652de90fc62bb4ab442a750c5dfc56b1",
+      "declarations": [
+        "norm_e",
+        "norm_cutoffChirpTerm",
+        "tsum_gaussianChirpAtom_eq_tsum_thetaAliasAtom"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "canonical",
+      "module_path": "Mathproof/Meta/RobustRealTIRecovery20261006.lean",
+      "sha256": "bffdfcd0b61f4f116c2f7e24566cbbef608fe127f2215fb3d225ad1218ce73d6",
+      "declarations": [
+        "indexEquiv",
+        "pack_index"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "canonical",
+      "module_path": "Mathproof/Meta/RobustRealTITensor20261006.lean",
+      "sha256": "3892ec68fe0bfd8f9c8ef600d15904c21ec617d6588667af8a2941a314a418f6",
+      "declarations": [
+        "three_mode_telescope"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "canonical",
+      "module_path": "Mathproof/External/IntegerMultBounds20261008/Matrix/GaussianTensorExecution.lean",
+      "sha256": "81edc5028577b6b16384c24ff1e529dc54d131873280cd471a62beb33c9ba91a",
+      "declarations": [
+        "cubeMap_zip"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "canonical",
+      "module_path": "Mathproof/Computability/MultitapeFrameRule20261014.lean",
+      "sha256": "e5aa9ec056340c67bc6e382eee0a859e6903d9944d3a0e021f2a24a12459cb66",
+      "declarations": [
+        "FootprintedRuns.frame"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    },
+    {
+      "environment": "canonical",
+      "module_path": "Mathproof/Computability/MultitapeLocality20261014.lean",
+      "sha256": "4e5df1bdd9764d335424acb2a3aad8364f647892e632d8b09aec85e45cfb5b31",
+      "declarations": [
+        "act_preserves_unscanned"
+      ],
+      "evidence": "Inspected source; no fresh Lean compile or compatible combined import asserted."
+    }
+  ],
+  "historical_dag_queries": [
+    {
+      "query": "\"norm_jacobiTheta_sub_one_le\"",
+      "results": [
+        {
+          "id": "source:327247",
+          "snapshot": "source-catalog",
+          "name": "norm_jacobiTheta_sub_one_le",
+          "module": "package:mathlib::Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable",
+          "type_node": null,
+          "axioms": null
+        },
+        {
+          "id": "source:3107667",
+          "snapshot": "source-catalog",
+          "name": "norm_jacobiTheta_sub_one_le_one",
+          "module": "project::Ripple.Number.Modular.CMEvaluation163",
+          "type_node": null,
+          "axioms": null
+        },
+        {
+          "id": "source:3539181",
+          "snapshot": "source-catalog",
+          "name": "norm_jacobiTheta_sub_one_le_one",
+          "module": "download:Ripple::Ripple.Number.Modular.CMEvaluation163",
+          "type_node": null,
+          "axioms": null
+        }
+      ]
+    },
+    {
+      "query": "\"tsum_exp_neg_quadratic\"",
+      "results": [
+        {
+          "id": "source:224954",
+          "snapshot": "source-catalog",
+          "name": "Complex.tsum_exp_neg_quadratic",
+          "module": "package:mathlib::Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation",
+          "type_node": null,
+          "axioms": null
+        }
+      ]
+    },
+    {
+      "query": "\"fourierIntegral_gaussian\"",
+      "results": [
+        {
+          "id": "source:224908",
+          "snapshot": "source-catalog",
+          "name": "fourierIntegral_gaussian",
+          "module": "package:mathlib::Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform",
+          "type_node": null,
+          "axioms": null
+        },
+        {
+          "id": "source:703793",
+          "snapshot": "source-catalog",
+          "name": "integrable_fourierIntegral_gaussian",
+          "module": "download:TauCeti::TauCeti.Analysis.Bochner.Fourier.Nonneg",
+          "type_node": null,
+          "axioms": null
+        },
+        {
+          "id": "source:703794",
+          "snapshot": "source-catalog",
+          "name": "integral_fourierIntegral_gaussian_eq_one",
+          "module": "download:TauCeti::TauCeti.Analysis.Bochner.Fourier.Nonneg",
+          "type_node": null,
+          "axioms": null
+        }
+      ]
+    }
+  ],
+  "coverage": "Bounded source searches and DAG name lookups; returned core hits are source-catalog rows with null typed proof fields."
+}
diff --git a/research/gaussian-expansion-headroom/LIBRARY-BRIDGES.md b/research/gaussian-expansion-headroom/LIBRARY-BRIDGES.md
@@ -0,0 +1,38 @@
+# Inspected library bridges and adaptations
+
+This is a retrieval and mathematical-use record, not a claim that the new
+result was Lean checked. Local paths and SHA-256 values are stored privately
+and in LIBRARY-BRIDGES.json; public entries use portable module names.
+Mathlib source revision: `db584cd6d46c92f209a44c0f1c829460d327499d`.
+All definitions and hypotheses were inspected before use.
+
+| Concept | Inspected source / declaration | Exact use and limit |
+|---|---|---|
+| Gaussian Fourier duality | `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform`, `fourierIntegral_gaussian`, `fourier_gaussian_pi'` | Supplies the Fourier transform of the normalized real Gaussian. We specialize to positive real width; no complex branch ambiguity remains. Sébastien Gouëzel's source and classical Gaussian analysis are credited. |
+| Periodization on the integer lattice | `Mathlib.Analysis.Fourier.PoissonSummation`, `Real.tsum_eq_tsum_fourier` | Turns the shifted positive row sum into an absolutely convergent Fourier series. Gaussian decay verifies both compact-uniform summability and sampled Fourier summability. David Loeffler's source is credited. |
+| Gaussian theta transformation | `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation`, `Complex.tsum_exp_neg_quadratic` | A second explicit Gaussian specialization of Poisson with positive real quadratic part. It confirms the width/reciprocal-width convention used in PROOF.md; it is an alternative derivation, not an independent new mechanism. |
+| Geometric theta tail | `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable`, `norm_jacobiTheta_sub_one_le` | Uses n² ≥ n to bound the dual tail by q/(1−q). We add the elementary rational certificate e³ > 20 and derive b(u), yielding a 0.6 contract. This is a source-bound application of classical estimates. |
+| Positive Gaussian majorants with unit-modulus phases | `ErdosProblems.Erdos230.GaussianPoisson`, `norm_e`, `norm_cutoffChirpTerm`, `tsum_gaussianChirpAtom_eq_tsum_thetaAliasAtom` | Boris Alexeev/Codex's source shows how to separate phase from Gaussian mass. Here arbitrary complex input phases are bounded by the triangle inequality and the positive row mass. Their smoothed chirp theorem is not asserted to equal this expansion map; the specialized proof is written explicitly. |
+| Tensor packing and axis isolation | `Mathproof.Meta.RobustRealTIRecovery20261006`, `indexEquiv`, `pack_index`; `Mathproof.External.IntegerMultBounds20261008.Matrix.GaussianTensorExecution`, `cubeMap_zip` | Motivates explicit coordinate enumeration and lifting scalar facts to every spectator line. We prove rectangular row-major completeness directly. The Gaussian-integer C tensor is a different map and is not a real-Gaussian norm theorem. |
+| Ordered tensor error telescoping | `Mathproof.Meta.RobustRealTITensor20261006`, `three_mode_telescope` | Motivates adding/subtracting one mode at a time. That theorem assumes orthogonal maps and uses Frobenius norms; these hypotheses do not apply here. PROOF.md instead proves a positive rectangular sup-norm recurrence retaining all contraction factors. |
+| Arbitrary exterior frames | `Mathproof.Computability.MultitapeFrameRule20261014`, `FootprintedRuns.frame`; `Mathproof.Computability.MultitapeLocality20261014`, `act_preserves_unscanned` | Motivates explicit disjoint read/write sets in the host window adapter. We prove the host frame property directly. A physical application still requires an actual run/footprint; no tape theorem is invoked on a dictionary. |
+
+The Mathlib Gaussian/theta declarations were also queried in the authoritative
+shared DAG. The returned rows have snapshot `source-catalog`, identifiers
+`source:224908`, `source:224954`, `source:327247` and null `type_node`/`axioms`.
+They are source evidence, not checked typed ports. Historical environments
+were not combined or imported into a new Lean environment.
+
+The complete bounded search packet includes 6 initial Mathproof queries
+(70 results per query at most), followed by 9 theta/Fourier/rounding/tensor
+queries (40 results per query at most), and 3 DAG name lookups (at most
+3 hits each). Some source queries return no hits. Limits and lexical
+ranking mean that unreturned results may exist. We inspected relevant
+actual source text and rejected unrelated permutation-padding, F₂-only
+and Euclidean-energy facts as substitutes for this sup-norm argument.
+
+The project already contains Gaussian periodization, norm accounting and
+inward rounding. Neither this search nor a missing PR-body match proves
+that a concept has never been applied. The useful deliverable is the
+complete specialized sufficient contract and executable reference, with
+the above attribution and scope limits.
diff --git a/research/gaussian-expansion-headroom/NOTICE.md b/research/gaussian-expansion-headroom/NOTICE.md
@@ -0,0 +1,45 @@
+# Attribution and scope
+
+New proof/application, downward coefficient reference, tensor/window adapters
+and controls: Dugongue, with substantial OpenAI Codex assistance. Apache-2.0.
+No independent human review or new formal-kernel verification is claimed.
+
+`vendor/intervals.py` and `vendor/NOTICE.md` are byte-identical to Mason
+Hale's `research/certified-gaussian-recovery/` at canonical main
+`20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The implementation and notice
+retain his OpenAI Codex assistance disclosure and Apache-2.0 attribution.
+Machin's formula, Taylor enclosures, inward rounding and the Gaussian
+integer caller are predecessor methods; only the interval module is run.
+
+`inputs/PR3851-README.md` is Jose Manuel (`jmbarrancoml`)'s exact public
+source at `7ab67b4a84d28cd562b9711aa315ca5b47822b37`.
+`inputs/PR3763-PROOF.md` is his exact public source at
+`6bb7dfdae182a69f7c8836a9ec1be0b2b747e124`. Both keep their existing
+credit and substantial OpenAI assistance disclosures. These define the
+immediate incomplete expansion/chirp join. Their physical executables are
+not imported or independently validated by this package.
+
+Retained predecessor credit includes Jose Manuel's PR2298 and PR2234/2287,
+Chafik Boukhalfa's PR481/486/489 local inverse and PR479 residue schedule,
+Ross Richardson's PR948 symbolic checks, corrected PR3709 and PR3787 word
+multiplier, RaD/hipotures' microbox/phase-cell/bulk reports, the source07/08
+OpenAI manuscript, Douglas Colkitt, eumemic, icekylinx, and all nested
+upstream contributors. The new contribution changes no predecessor word,
+review disposition or selected certificate. The PR371/684/902/1430 audit
+credit remains in the unmodified vendor notice.
+
+David Harvey and Joris van der Hoeven, *Integer Multiplication in Time
+O(n log n)*, Annals of Mathematics 193 (2021), 563–617,
+DOI 10.4007/annals.2021.193.2.4, provide the Gaussian resampling lineage.
+Poisson summation, Gaussian Fourier duality and theta tail majorization are
+classical. Mathlib's inspected Fourier source credits Sébastien Gouëzel;
+its Poisson and theta sources credit David Loeffler, under Apache-2.0.
+The inspected Erdős 230 Gaussian–Poisson source credits Boris Alexeev
+and Codex, under Apache-2.0. These Lean sources are cited as mathematical
+precedents, not copied as new code or represented as newly checked proofs.
+
+The shared MathProof tensor/packing/frame modules are further discovery
+precedents. Their exact declarations and adaptations are recorded in
+LIBRARY-BRIDGES.md and its JSON manifest. Source hashes provide traceability;
+they do not establish authorship beyond retained source notices, novelty,
+compatibility of all imports, or fresh kernel verification.