From 5e7bdfa3c53bbb5a8d6e81f0efe7005c89184e6a Mon Sep 17 00:00:00 2001 From: Dugongue <49054532+Dugongue@users.noreply.github.com> Date: Mon, 19 Oct 2026 01:20:12 +0000 Subject: [PATCH] Certify Gaussian expansion headroom for the physical chirp caller --- .../gaussian-expansion-headroom/INPUTS.json | 9 + .../LIBRARY-BRIDGES.json | 174 +++++++++++ .../LIBRARY-BRIDGES.md | 38 +++ .../gaussian-expansion-headroom/NOTICE.md | 45 +++ research/gaussian-expansion-headroom/PROOF.md | 271 ++++++++++++++++++ .../gaussian-expansion-headroom/README.md | 117 ++++++++ .../gaussian-expansion-headroom/RESULT.json | 118 ++++++++ .../gaussian-expansion-headroom/SOURCES.json | 67 +++++ .../gaussian-expansion-headroom/TASK.json | 79 +++++ .../gaussian-expansion-headroom/VERIFY.json | 37 +++ .../gaussian-expansion-headroom/expansion.py | 197 +++++++++++++ .../inputs/PR3763-PROOF.md | 225 +++++++++++++++ .../inputs/PR3851-README.md | 118 ++++++++ .../test_expansion.py | 91 ++++++ .../vendor/NOTICE.md | 39 +++ .../vendor/intervals.py | 229 +++++++++++++++ .../gaussian-expansion-headroom/verify.py | 170 +++++++++++ 17 files changed, 2024 insertions(+) create mode 100644 research/gaussian-expansion-headroom/INPUTS.json create mode 100644 research/gaussian-expansion-headroom/LIBRARY-BRIDGES.json create mode 100644 research/gaussian-expansion-headroom/LIBRARY-BRIDGES.md create mode 100644 research/gaussian-expansion-headroom/NOTICE.md create mode 100644 research/gaussian-expansion-headroom/PROOF.md create mode 100644 research/gaussian-expansion-headroom/README.md create mode 100644 research/gaussian-expansion-headroom/RESULT.json create mode 100644 research/gaussian-expansion-headroom/SOURCES.json create mode 100644 research/gaussian-expansion-headroom/TASK.json create mode 100644 research/gaussian-expansion-headroom/VERIFY.json create mode 100644 research/gaussian-expansion-headroom/expansion.py create mode 100644 research/gaussian-expansion-headroom/inputs/PR3763-PROOF.md create mode 100644 research/gaussian-expansion-headroom/inputs/PR3851-README.md create mode 100644 research/gaussian-expansion-headroom/test_expansion.py create mode 100644 research/gaussian-expansion-headroom/vendor/NOTICE.md create mode 100644 research/gaussian-expansion-headroom/vendor/intervals.py create mode 100644 research/gaussian-expansion-headroom/verify.py diff --git a/research/gaussian-expansion-headroom/INPUTS.json b/research/gaussian-expansion-headroom/INPUTS.json new file mode 100644 index 0000000000..1a2b91a11e --- /dev/null +++ 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 new file mode 100644 index 0000000000..9e5d713b01 --- /dev/null +++ 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 new file mode 100644 index 0000000000..a44eeae1b3 --- /dev/null +++ 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 new file mode 100644 index 0000000000..ceeb9b0baf --- /dev/null +++ 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. diff --git a/research/gaussian-expansion-headroom/PROOF.md b/research/gaussian-expansion-headroom/PROOF.md new file mode 100644 index 0000000000..c9844fedfb --- /dev/null +++ b/research/gaussian-expansion-headroom/PROOF.md @@ -0,0 +1,271 @@ +# Gaussian expansion with certified chirp headroom + +Prepared by Dugongue with substantial OpenAI Codex assistance. Apache-2.0. +This is an informal universal proof with executable rational corroboration. +It has not received independent human review or a new Lean kernel audit. + +## 1. The result and its exact interface + +For positive integers s, t and u, define the normalized periodic Gaussian map + + (A z)_k = 1/(2√u) ∑_{j∈ℤ} exp(−π(j−s k/t)²/u) z_{j mod s}, + 0 ≤ k < t. + +Thus A is the existing source-normalized expansion S/2, with α² = u. +No Fourier permutation or normalization is changed. Define + + b(u) = 1/2 + 1/(20^u − 1). + +**Theorem 1 (one axis).** For every such s, t, u, every p ≥ 1 and q ≥ 8, +and every complex p-grid input with max_j |z_j| ≤ 1, `prepare` followed by +`line` returns complex p-grid output y satisfying + + max_k |y_k| ≤ b(u) ≤ 21/38 < 3/5. + +If δ is the maximum `Row.deficit` returned by preparation, then also + + max_k |y_k − (A z)_k| ≤ δ + √2 · 2^(−p) + ≤ δ + 2 · 2^(−p). + +The construction is finite, uses nonnegative downward dyadic coefficients, +and certifies δ by exact rational arithmetic. The norm conclusion does not +require δ to be small. Accuracy requires the displayed, computable bound. + +**Theorem 2 (all tensor dimensions).** Let D ≥ 1 and let the axis parameters +be positive integer triples (s_i, t_i, u_i). Apply each axis once in the +declared row-major layout, rounding after each axis as in `tensor`. For every +unit sup-norm input tensor the returned tensor satisfies + + ||y||∞ ≤ M_D = ∏_{i=1}^D b(u_i) ≤ 21/38 < 3/5. + +Put M_0 = 1, E_0 = 0, and let δ_i be the maximum prepared row deficit on +axis i. Relative to the exact tensor product of the maps A_i, its error is +at most E_D, where + + M_i = b(u_i) M_{i−1}, + E_i = b(u_i) E_{i−1} + δ_i M_{i−1} + 2 · 2^(−p). + +No independence, orthogonality, equal axis lengths, or volume factor is +assumed. These two theorems are sufficient norm and error contracts. + +PR3763 requires an encoded p-grid input of norm at most 0.6 and p−A ≥ 13. +Theorems 1–2 establish the numerical norm clause for these expansion outputs; +the caller must separately establish p−A ≥ 13 and the actual encoded physical +handoff. An additional approximation of modulus at most 9/190 still satisfies +the norm clause, because 3/5 − 21/38 = 9/190. This is a handoff allowance, +not an assertion that unimplemented physical operations have zero error. + +## 2. Periodization and the theta bound + +We use the classical Gaussian Fourier formula and Poisson summation, present +in the linked Lean tree as `fourier_gaussian_pi'`, `Real.tsum_eq_tsum_fourier` +and `Complex.tsum_exp_neg_quadratic`. The exact source references and evidence +levels are in LIBRARY-BRIDGES.md. They are mathematical precedents, not new +formalization claims. + +Let g(x) = u^(−1/2) exp(−πx²/u). In the Fourier convention +ĝ(ξ) = ∫ g(x) exp(−2πiξx) dx, the Gaussian formula gives +ĝ(ξ) = exp(−πuξ²). Both g and ĝ have Gaussian decay. In particular, their +integer translates have summable sup norms on every compact interval, and +their sampled Fourier series converges absolutely. These verify Poisson's +hypotheses and justify + + u^(−1/2) ∑_{j∈ℤ} exp(−π(j−x)²/u) + = ∑_{n∈ℤ} exp(−πu n²) exp(2πinx) + = 1 + 2∑_{n≥1} exp(−πu n²) cos(2πnx). + +The series on the left is nonnegative. Taking absolute values on the right, +or using cos ≤ 1, bounds half of it by + + 1/2 + ∑_{n≥1} exp(−πu n²) + ≤ 1/2 + q0/(1−q0), q0 = exp(−πu). + +Here n² ≥ n and 0 < q0 < 1. This is the same geometric majorization used +by Mathlib's `norm_jacobiTheta_sub_one_le`; no new theta identity is claimed. +For an entirely rational universal constant, π > 3 and + + exp(3) > ∑_{n=0}^9 3^n/n! > 20 + +imply q0 < 20^(−u) for integer u ≥ 1. Since q/(1−q) is increasing on +(0,1), every normalized row mass is strictly below + + 1/2 + 1/(20^u−1) = b(u) ≤ b(1) = 21/38. + +All exchanges of sums below are justified by nonnegativity or absolute +convergence. Grouping j by j mod s partitions the full integer lattice; +every winding is included, even when several j have the same residue. +Consequently A has nonnegative real entries and row sums at most b(u), for +every center s k/t, including boundary, fractional and wrapped centers. + +For any complex vector v, the triangle inequality now proves + + |(A v)_k| ≤ ∑_r A_{k,r}|v_r| ≤ b(u)||v||∞. + +This is an induced sup-norm estimate. Frobenius or Euclidean tensor bounds +would introduce different dimension factors and are not substituted for it. + +## 3. A finite downward coefficient construction + +Fix one row center c = s k/t. The code chooses + + R = max(u, floor(√(u(q+16))) + 2) + +and retains all integers from floor(c)−R through ceil(c)+R, inclusive. This +contains every integer at distance at most R. On each omitted side the +first distance is at least R, and successive distances increase by one. +Thus the first Gaussian term is at most exp(−πR²/u), and the ratio of each +successive term to its predecessor is at most exp(−π(2R+1)/u). Put + + a = floor(3R²/u), b = floor(3(2R+1)/u). + +Because π > 3 and e > 2, the two omitted sides, after multiplication by +1/(2√u), have total mass at most + + T = 2^(−a)/(1−2^(−b)). + +We used √u ≥ 1. R ≥ u ensures b ≥ 6, so the denominator is positive. +The bound remains valid when the first omitted distance exceeds R; no +integer term at the endpoints is silently dropped. The chosen R also gives +a ≥ 3(q+16), so this tail is much smaller than one q-grid unit. + +For a retained j, let c_j = exp(−π(j−c)²/u)/(2√u). The credited outward +interval backend supplies q-grid endpoints l_j ≤ c_j ≤ h_j. The construction +uses w_j = max(0,l_j), also a q-grid value. Since c_j ≥ 0, + + 0 ≤ w_j ≤ c_j, c_j − w_j ≤ h_j − w_j. + +Sum w_j over retained j in each residue class to form the finite matrix B. +Then entrywise 0 ≤ B ≤ A and + + ∑_r (A_{k,r} − B_{k,r}) ≤ T + ∑_j (h_j−w_j) = δ_k. + +This is exactly the stored row deficit. It simultaneously bounds the +operator error ||A−B||∞ and prevents coefficient rounding from increasing +the analytic row mass. The implementation also checks the rational +inequality ∑_r B_{k,r} ≤ b(u). This finite check corroborates the universal +argument and rejects malformed coefficients; it is not a replacement for +the theta proof. + +For completeness, the interval arithmetic has the following justification. +Addition and negation use exact endpoint arithmetic; multiplication rounds +the extreme endpoint products outward. Positive reciprocation reverses +endpoints. Integer square root on u·2^(2q) brackets √u between consecutive +q-grid points. Machin's identity for π is evaluated with alternating +arctangent remainders before outward rounding. For exp(−x), x ≥ 0, the +backend reduces x by powers of two into [0,1/8], encloses the positive +Taylor series for exp(x) there with its geometric factorial tail, takes +the positive reciprocal and squares back outward. At q ≥ 8 the dyadic +division retains the [0,1/8] endpoint. If x ≥ q, exp(−x) < 2^(−q) follows +from e > 2 and justifies the backend's [0,2^(−q)] shortcut. These operations +enclose every coefficient; no floating-point exponential enters acceptance. +The full predecessor interval proof and authorship remain credited. + +`Row.check` verifies shape, positivity and the mass inequality. `line` also +compares each supplied row to canonical certified preparation, so changing +its center, deficit or weights cannot turn an arbitrary row into an +accepted approximation certificate. Source hashes are checked before the +vendored numerical module is imported. These guards assume an unchanged +trusted program and manifest, rather than claiming security against their +coordinated malicious replacement. + +## 4. Inward grid rounding preserves the hard disk bound + +For a real x define Q_p(x) = sign(x) floor(2^p|x|)/2^p, with Q_p(0)=0. +It satisfies |Q_p(x)| ≤ |x| and |Q_p(x)−x| < 2^(−p). Apply it separately +to the real and imaginary parts. For every complex z, + + |Q_p(z)|² ≤ |z|², |Q_p(z)−z| ≤ √2 · 2^(−p). + +`line` computes Bz exactly from integer numerators, then applies Q_p once +per component. Therefore + + |Q_p(Bz)| ≤ |Bz| ≤ b(u)||z||∞, + |Q_p(Bz)−Az| ≤ √2·2^(−p) + δ||z||∞. + +This proves Theorem 1, including arbitrary signed complex phases. Inward +rounding is nonlinear; we use only its pointwise modulus and error bounds, +not a false assertion that it is a linear or nonexpansive operator on +differences. Nearest-grid rounding can increase modulus, as the coarse-grid +control demonstrates. At production precision its small increase could +instead be charged against 9/190; the present construction preserves the +hard bound directly. + +## 5. Tensor composition, layout and error transport + +Lift A_i and B_i to the full tensor by acting along axis i and leaving +every spectator coordinate unchanged. Each lifted map has the same induced +sup-norm bound as its line map: every output coordinate belongs to exactly +one spectator line. The row-major index is + + (((k_1 s_2 + k_2)s_3 + k_3) ... )s_D + k_D + +before that axis is replaced by its target length. The code fixes spectator +coordinates, reads all source positions, and writes every target position +once. This is a bijective enumeration of the declared coordinate tuples. +It does not perform a CRT permutation or infer one from coordinate count. + +Suppose the implemented intermediate tensor has norm at most M_{i−1} and +error at most E_{i−1} relative to the exact intermediate tensor. Positivity +and inward rounding give its next norm bound b(u_i)M_{i−1}. For error, add +and subtract A_i applied to that same implemented intermediate tensor: + + Q_p(B_i y) − A_i x + = [Q_p(B_i y)−B_i y] + (B_i−A_i)y + A_i(y−x). + +The three terms are bounded respectively by 2·2^(−p), δ_i M_{i−1} and +b(u_i)E_{i−1}. This proves the recurrences and Theorem 2 by induction. +Equivalently, every earlier error is multiplied by the later contraction +factors. No independence assumption is used, and spectator multiplicity +does not multiply a sup-norm error. + +The exact Gaussian tensor execution, tensor packing and three-mode +telescope modules in the shared library suggested this decomposition. +Their Gaussian-integer or orthogonal/Frobenius hypotheses are different; +the positive rectangular sup-norm argument above proves what is needed +here directly. For the retained bulk caller, the number of actual resampled +axes is D = d−1. The inherited recovery exponent remains +γ = ∑_i (2u_i + j_i + 1). The factor 1/2 in each expansion is preserved, +and this norm improvement removes none of the required recovery scales. + +## 6. Explicit bounded windows and dirty exterior + +The host `window` adapter names injective source and output positions and +requires them to be disjoint. It reads exactly the source positions, uses +the certified line map, copies the finite storage map and writes exactly +the output positions. Hence every borrowed source and every other existing +storage entry retains its original value, with no condition on dirty +exterior contents. Theorem 1 holds on the returned output positions. +The proof is simply inspection of the read and write sets and injectivity. + +This instantiates an arithmetic frame contract inspired by +`FootprintedRuns.frame`. It is a host dictionary adapter. No multitape +transition table, physical head restoration, or tape running-time bound is +deduced from the Lean frame theorem without an actual run and footprint. + +## 7. Cost, finite evidence and remaining composition + +For one prepared axis there are t rows with at most 2R+2 retained integer +terms each. Coefficients can be prepared once and reused across all +spectator lines. The supplied dense reference retains s coefficients per +row, so its online arithmetic costs O(st) integer multiply-adds per line, +plus p-grid truncation; preparing transcendental enclosures and arbitrary +precision integer bit costs are additional. A tensor axis with current +volume N has N/s lines. Indexed arrays and complete dense coefficient rows +are used. These costs do not establish the desired fast physical expansion. + +The retained exact checks cover 34 rows, 340 complex line values and 80 +tensor output coordinates. They include u = 1, 2, 4, 10, nonsquare √u, +fractional centers, repeated periodic residues, complex signs, two and +three axes, and a p = 101 case. A separately indexed residue-first oracle +and a direct Kronecker matrix compare the results and their error bounds. +They share the credited interval transcendental backend; they are not an +independent transcendental implementation. Finite corroboration is not a +proof for all parameters; the preceding argument supplies that proof. + +The physical source-normalized expansion, protected page encoding, +catalogue/halo routing, sequential tape costs, complete outer tensor caller, +CRT conversions, and final integer recovery remain to be joined. PR3851's +compression core and PR3763's chirp consumer are not executed by this +package. Their other hypotheses are inherited only when a future caller +actually instantiates them. No new κ, complete multiplication theorem, +selected-frontier change, or practical speedup is claimed. diff --git a/research/gaussian-expansion-headroom/README.md b/research/gaussian-expansion-headroom/README.md new file mode 100644 index 0000000000..159f1aff75 --- /dev/null +++ b/research/gaussian-expansion-headroom/README.md @@ -0,0 +1,117 @@ +# Certified Gaussian expansion headroom for the physical chirp caller + +PR3851 leaves the source-normalized Gaussian expansion and its 0.6-norm +join to PR3763 unfinished. This package supplies one reusable numerical +component: for every positive integer source/target length and Gaussian +width squared u ≥ 1, it constructs downward dyadic expansion coefficients +and inward-rounded complex p-grid outputs whose sup norm is at most +**21/38 < 0.6** on every unit-disk input. The remaining norm margin is +exactly **9/190**. It also supplies a computable approximation-error bound. + +[PROOF.md](PROOF.md) proves this for every input and every tensor dimension, +including arbitrary complex signs, periodic windings, nonsquare √u and +unequal axis lengths. The actual bound is +`b(u) = 1/2 + 1/(20^u−1)` per axis and the product of these bounds over +the resampled axes. Earlier errors are discounted by later contractions. +Coefficient precision q must be at least 8; output precision p may be any +positive integer. The chirp caller must additionally meet its own +`p−A ≥ 13` and physical encoding/scheduling requirements. + +The contribution combines Gaussian Fourier duality, Poisson periodization, +theta-series majorization, positive operator domination, directed dyadic +rounding, tensor telescoping, coordinate packing and finite-window frames. +[LIBRARY-BRIDGES.md](LIBRARY-BRIDGES.md) maps these to inspected sources in +the shared Lean tree/DAG and states where a new argument is needed. +The classical mathematics and existing inward-rounding method are credited; +no claim of their invention or exhaustive first use in the project is made. + +## Evidence and use + +The standard-library reference checks 34 prepared rows, 340 complex line +values and 80 complete tensor output coordinates. A separate residue-first +oracle and a direct dense Kronecker evaluation check the finite outputs. +They share Mason Hale's credited interval backend. Seven semantic test +groups cover invalid domains, coefficient/center/error tampering, missing +periodic windings, coarse nearest-grid rounding, dirty exterior ownership, +source-hash corruption, and exported CLI/receipt corruption. The registered +replay includes these controls with Python assertions disabled. + +From the repository root with Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-expansion-headroom +``` + +For an extracted standalone package: + +```sh +python3.12 -B research/gaussian-expansion-headroom/verify.py +python3.12 -B research/gaussian-expansion-headroom/test_expansion.py +``` + +The first command ends with +`PASS_GAUSSIAN_EXPANSION_HEADROOM rows=34 line_values=340 tensor_coordinates=80 RECEIPT_MATCH`. +`expansion.prepare(s,t,u,q)` constructs reusable rows; +`expansion.line(values,rows,p)` consumes integer real/imaginary numerators +on the 2^(−p) grid. `tensor` applies all declared axes and returns the +shape, sufficient error bound and hard norm bound. `window` reads named +borrowed source positions and changes only disjoint named output positions. +Inputs outside the unit disk fail rather than silently being rescaled. + +This is an exact host reference and an informal universal sufficient proof. +The physical expansion, encoded handoff and complete caller remain open. +No new κ or selected-frontier change is claimed. There is no new Lean +formalization, independent human review or fresh kernel/axiom certification. + +## Source and overlap scope + +Base: canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority +revision 6. The `uniform-transfer-audit` card was selected and its positive +control returned `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; the selected cold +replay is unrelated to this additive package and was not rerun. + +The round scanned 578 open PR bodies, updated recent all-state records +through PR3875, the visible HTML of Discussions 1163, 1166 and 3664, and +actual related proof sources. Discussion HTML is partial coverage. Shared +library retrieval used bounded lexical/source queries and historical DAG +lookups, not exhaustive semantic retrieval. The relevant DAG hits for +Poisson/theta/Gaussian Fourier facts are source-catalog entries with no +typed proof node in the returned packet. This does not imply fresh kernel +verification or absence of other applications. + +Mason Hale's existing certified Gaussian recovery already implements +inward rounding and a dense finite complete integer caller. The RaD +reports already prove expansion norm below 3/4 and tensor error transport. +PR3851 and PR3763 provide the immediate physical producer/consumer contracts. +The added result is the explicit all-parameter 0.6 handoff bound together +with downward coefficient preparation, hard disk preservation, propagated +error, layout and dirty-exterior host interfaces. The existing dense +integer caller is not repackaged as a new multiplication algorithm. + +## Open next questions + +1. Can one physical expansion block implement these downward coefficients + and inward grid rounding at the existing paid cost? First freeze its + encoded source/output/page fields and compare the full output with this + reference. The missing pieces are the transition schedule, coefficient + producer and full tape invoice. +2. Can the expansion output be handed to PR3763 under one complete tensor + schedule? First check the actual p−A guard, target order, source/halo + ownership and D = d−1 axis count. Protected child returns and restoration + must be joined before claiming a complete physical caller. +3. How much of the 9/190 norm margin is consumed by the eventual page and + conversion interface? First bound every added approximation in modulus + and keep the two final S factors and γ normalization explicit. CRT + entrance/return and integer recovery are still separate obligations. + +## Credit + +Prepared by Dugongue with substantial OpenAI Codex assistance in source +retrieval, mathematics, implementation, verification and prose. +Jose Manuel (`jmbarrancoml`) supplies PR3851 and PR3763 and the PR2298 +handoff lineage. Mason Hale supplies the unmodified interval backend and +prior certified numerical caller. David Harvey and Joris van der Hoeven, +the retained OpenAI manuscript, Douglas Colkitt, RaD/hipotures, Chafik +Boukhalfa's PR481/486/489, the PR3709/3787 word lineage, PR479 and PR948, +and the linked library authors retain their credit. [NOTICE.md](NOTICE.md) +and the preserved upstream notices give the exact scope and attribution. diff --git a/research/gaussian-expansion-headroom/RESULT.json b/research/gaussian-expansion-headroom/RESULT.json new file mode 100644 index 0000000000..8554c38af8 --- /dev/null +++ b/research/gaussian-expansion-headroom/RESULT.json @@ -0,0 +1,118 @@ +{ + "cases": [ + { + "deficit_below_grid_units": "1922329606478882150378208287250534460483567284108231377464159026389400420353/31082702275611665131341397175782472531945132538956778505824355503004897003145384689664", + "max_mass": "39142939287540699/72057594037927936", + "p": 16, + "prepared_terms": 43, + "q": 56, + "s": 1, + "t": 2, + "u": 1, + "weights_sha256": "3ef8cfafda8382611680bb27e7a013cdbbb819d708f9e47b221af82a847f3a6f" + }, + { + "deficit_below_grid_units": "7950811791502729482262810011606070838397107333168236395761687149588512769/1942668892225729070708837323486404533246570783684798656614022218937806062696586543104", + "max_mass": "10020592457610422551/18446744073709551616", + "p": 20, + "prepared_terms": 86, + "q": 64, + "s": 2, + "t": 4, + "u": 1, + "weights_sha256": "36480eb680b3bf1bd79c1550db2ec0b6bee430c73440235468e83817640e9758" + }, + { + "deficit_below_grid_units": "39253682310813491034143145198120944660054233071838955423928319519752193/121416805651029854786649772083138891617603642427799750678198662288898720942597865472", + "max_mass": "2361199709943479859835/4722366482869645213696", + "p": 24, + "prepared_terms": 335, + "q": 72, + "s": 5, + "t": 8, + "u": 4, + "weights_sha256": "86f72e79d6d2062f743b2ba3468cca348237e79ce94f143db0b56b38dd027917" + }, + { + "deficit_below_grid_units": "5691412770192484757619359603227644045758665227393544092234151547439502837231386625/16687398718131872876512349055881398421956331288076066268282667329235938798529206090964888715264", + "max_mass": "2370001990457150272225/4722366482869645213696", + "p": 24, + "prepared_terms": 511, + "q": 72, + "s": 7, + "t": 16, + "u": 2, + "weights_sha256": "db4248746c5536561a3bc2a0cd978ede4480e599f16cd9a08404af0a789a1160" + }, + { + "deficit_below_grid_units": "13711897747698869363226124302080353762823106502753211930398348601608882129876658922830295494016324924050952213070086145/693167402872204690199334828788417549835014274206307801158831792508380474626225429625264044488872068283245151253125517175263592448", + "max_mass": "11150372599265818043230307199367823227895845/22300745198530623141535718272648361505980416", + "p": 101, + "prepared_terms": 343, + "q": 144, + "s": 3, + "t": 4, + "u": 10, + "weights_sha256": "46195a838f883a81090f7b624f350b22d1f14671fd4a21f02f971ab1f03100b7" + } + ], + "chirp_norm_limit": "3/5", + "complex_line_values": 340, + "coverage": "Finite exact-rational corroboration; universal proof is PROOF.md; no new kappa or physical implementation.", + "margin": "9/190", + "rows": 34, + "schema_version": 1, + "status": "PASS_GAUSSIAN_EXPANSION_HEADROOM", + "tensor_coordinates": 80, + "tensors": [ + { + "error": "40048396692303449366023337513860209159234857026860105575059222039262830788724739154186936880047208949423631616209/13974579863554114008170328679318904673144731523814778110446550379998037056546350286421666479145888409725473519726231552", + "norm_bound": "401/1444", + "output_sha256": "d24addcc873d222d7a85c3d52f46677865d70ac96052a34abbe8327a2578f1b1", + "shape": [ + 4, + 4 + ], + "specs": [ + [ + 2, + 4, + 1 + ], + [ + 3, + 4, + 2 + ] + ] + }, + { + "error": "763744217534677028475674094037452025129309326962846176895013404451369787560083491604393421397313034381212756001130956618639923/228647574499562985695198953814948519549885790612672611007281642331287669223597680081332860090501296813753154805389013651429364072448", + "norm_bound": "160001/1152312", + "output_sha256": "0de9acd76fc28ba72bcd38cccd3007b87e753493ebdaff07d46a475d6d7b55aa", + "shape": [ + 4, + 4, + 4 + ], + "specs": [ + [ + 2, + 4, + 1 + ], + [ + 2, + 4, + 2 + ], + [ + 3, + 4, + 4 + ] + ] + } + ], + "uniform_cap": "21/38" +} diff --git a/research/gaussian-expansion-headroom/SOURCES.json b/research/gaussian-expansion-headroom/SOURCES.json new file mode 100644 index 0000000000..93df4536d9 --- /dev/null +++ b/research/gaussian-expansion-headroom/SOURCES.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "research/certified-gaussian-recovery/intervals.py", + "usage": "provenance", + "git_blob": "91d458865aa026bdf0d59653a4ecbfe3a178ecbc", + "sha256": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df" + }, + { + "path": "research/certified-gaussian-recovery/NOTICE.md", + "usage": "provenance", + "git_blob": "5e3269b5afe5e11f044ffae45216c4731b42c7af", + "sha256": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d" + }, + { + "path": "research/certified-gaussian-recovery/PROOF.md", + "usage": "provenance", + "git_blob": "9dace009004a4336d6ce57764c255190fbf87e64", + "sha256": "65480dd23fb1aae314365aeea4aacbc146e160e5c8a7a4ac4f602f22ae4581de" + }, + { + "path": "references/semantic-bulk/rad20/reports/downstream-microbox-resampling.md", + "usage": "provenance", + "git_blob": "27f962de34b6943aee33cc0d40b8c7883ccf56f2", + "sha256": "9598c236eed7e44ac5eb41cc20f7c23249829e195247d15e2857a34e14222c49" + }, + { + "path": "references/semantic-bulk/rad20/reports/review-bulk-resampling.md", + "usage": "provenance", + "git_blob": "9731a03fdb7a1cecaddab737545befa238cb9ad3", + "sha256": "12aefaa9a0eee367fb71e8f910ed5f0094e1203d2caa29836b0c37887c446c29" + } + ], + "external_public_inputs": [ + { + "local_path": "inputs/PR3851-README.md", + "source_pr": 3851, + "source_head": "7ab67b4a84d28cd562b9711aa315ca5b47822b37", + "source_path": "research/physical-gaussian-core/README.md", + "sha256": "ce063e3796bdcea206959918915826ae75c1bcbd74736913e5b330aa04fb5791", + "coverage": "Exact vendored public source, checked by INPUTS.json; no foreign Git head required by replay and no physical predecessor executable is run." + }, + { + "local_path": "inputs/PR3763-PROOF.md", + "source_pr": 3763, + "source_head": "6bb7dfdae182a69f7c8836a9ec1be0b2b747e124", + "source_path": "research/physical-chirp-middle/PROOF.md", + "sha256": "92cccf922e0e79fcffc5b6883812c6c5f162565c926f9d807791f6b850ac0951", + "coverage": "Exact vendored public source, checked by INPUTS.json; no foreign Git head required by replay and no physical predecessor executable is run." + } + ], + "local_library_provenance": "LIBRARY-BRIDGES.json records exact inspected source hashes. This is discovery evidence, not new runtime imports or fresh kernel checks." +} diff --git a/research/gaussian-expansion-headroom/TASK.json b/research/gaussian-expansion-headroom/TASK.json new file mode 100644 index 0000000000..5c70d4d7e3 --- /dev/null +++ b/research/gaussian-expansion-headroom/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "scope_change_reason": "The donor requests extensive linked Lean-tree/DAG reuse. PR3851 explicitly leaves the expansion-to-PR3763 norm join open. This round proves a positive all-parameter numerical sufficient contract and supplies a certified host reference, retaining physical and recovery obligations.", + "actual_scope": "Universal normalized Gaussian expansion headroom, downward coefficients, inward complex grid rounding, tensor error transport and explicit host window frames.", + "bottleneck_link": "A Gaussian expansion producer must satisfy the existing physical chirp consumer norm <= 0.6; the source-level 3/4 bound alone does not establish it.", + "budget_minutes": 60, + "author": "Dugongue", + "ai_assistance": "Substantial OpenAI Codex assistance in retrieval, mathematical synthesis, implementation, verification and prose. No independent human review.", + "outcome": "completed", + "evidence": "Complete informal sufficient proof; exact host reference; 34 rows, 340 complex line values, 80 direct-Kronecker tensor output comparisons, 7 control groups and normal/optimized registered replays. No new kappa or kernel verification.", + "stop_rule": "Finish and verify one positive numerical norm/error interface. Stop before claiming a physical expansion, complete multiplier, new frontier or exhaustive novelty.", + "upstream_checkpoint": { + "utc": "2026-10-19T01:12:50.096Z", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "recent_pr_max": 3875, + "priority_revision": 6 + }, + "open_questions": [ + { + "question": "Can one physical expansion block implement the downward coefficients and inward rounding at the retained paid cost?", + "why_it_matters": "Would instantiate the sufficient numerical contract in the actual fixed-tape producer.", + "first_step": "Freeze source/output/page encodings and compare every returned coordinate with this reference, including coefficient preparation and scans.", + "blocked_by": "No physical expansion transition schedule or tape invoice is implemented here." + }, + { + "question": "Can the completed expansion hand off to PR3763 under a full tensor schedule?", + "why_it_matters": "Would close the actual producer/consumer norm join while preserving the declared input ABI.", + "first_step": "Check p-A >= 13, retained target order, source/halo ownership, protected returns and the actual D=d-1 axis count.", + "blocked_by": "The complete physical tensor and restoration caller has not been joined." + }, + { + "question": "How much of the 9/190 norm margin is consumed by page and conversion errors?", + "why_it_matters": "Prevents a valid numerical margin from hiding a missing physical conversion or recovery scale.", + "first_step": "Bound every added modulus error and keep both final S factors and gamma explicit.", + "blocked_by": "CRT entrance/return and final integer recovery remain separate interfaces." + } + ], + "overlap_coverage": "578 open PR bodies; recent all-state records refreshed through PR3875; actual related source comparisons; partial visible Discussion HTML. Bounded library searches and source-catalog DAG hits are not exhaustive semantic or typed proof coverage." +} diff --git a/research/gaussian-expansion-headroom/VERIFY.json b/research/gaussian-expansion-headroom/VERIFY.json new file mode 100644 index 0000000000..3dfb677fd6 --- /dev/null +++ b/research/gaussian-expansion-headroom/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "34 certified rows, 340 complex line values, 80 independently indexed direct tensor outputs, host frame, source hashes and exact result receipt." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_expansion.py" + ], + "timeout_seconds": 60, + "checks": "Seven semantic groups including domain/cache aliases, coefficient/center/deficit mutants, nearest-grid and missing-winding controls, dirty ownership, exported CLI/source/receipt corruptions." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/test_expansion.py" + ], + "timeout_seconds": 60, + "checks": "The same meaningful semantic/export controls with Python assertions disabled." + } + ] +} diff --git a/research/gaussian-expansion-headroom/expansion.py b/research/gaussian-expansion-headroom/expansion.py new file mode 100644 index 0000000000..36f22d1e6c --- /dev/null +++ b/research/gaussian-expansion-headroom/expansion.py @@ -0,0 +1,197 @@ +"""Certified downward Gaussian rows and a norm-preserving tensor reference. +Dugongue, with substantial OpenAI Codex assistance. Apache-2.0. +This is host arithmetic, not a physical multitape implementation. +""" +from dataclasses import dataclass +from fractions import Fraction as F +from functools import lru_cache +from itertools import product +from math import isqrt, prod +from pathlib import Path +import hashlib +import json +import sys + +ROOT = Path(__file__).resolve().parent + +def require(ok, message): + if not ok: + raise ValueError(message) + +def authenticate_inputs(): + manifest = json.loads((ROOT / 'INPUTS.json').read_text(encoding='utf-8')) + for name, digest in manifest['sha256'].items(): + path = (ROOT / name).resolve() + require(path.is_relative_to(ROOT) and path.is_file(), 'input path') + require(hashlib.sha256(path.read_bytes()).hexdigest() == digest, 'source hash: '+name) + +authenticate_inputs() +sys.path.insert(0, str(ROOT / 'vendor')) +from intervals import Interval, pi_interval, exp_negative + + +def integer(value, minimum, name): + require(type(value) is int and value >= minimum, name) + return value + + +def cap(u): + integer(u, 1, 'integer u >= 1') + return F(1, 2) + F(1, 20**u - 1) + + +def sqrt_interval(u, bits): + integer(u, 1, 'integer u >= 1') + integer(bits, 1, 'positive working precision') + square = u << (2*bits) + lower = isqrt(square) + return Interval(lower, lower if lower*lower == square else lower+1, bits) + + +def tail_bound(u, radius): + integer(u, 1, 'integer u >= 1') + integer(radius, 1, 'positive radius') + a, b = 3*radius*radius // u, 3*(2*radius+1) // u + require(b >= 1, 'geometric tail ratio') + return F(1, 1 << a) / (1-F(1, 1 << b)) + + +@dataclass(frozen=True) +class Row: + source: int + target: int + index: int + u: int + bits: int + radius: int + weights: tuple[int, ...] + deficit: F + terms: int + + @property + def mass(self): + return F(sum(self.weights), 1 << self.bits) + + def check(self): + for x, lo, name in [(self.source,1,'source'),(self.target,1,'target'), + (self.u,1,'u'),(self.bits,8,'bits >= 8'),(self.radius,1,'radius')]: + integer(x,lo,name) + require(type(self.index) is int and 0 <= self.index < self.target, 'row index') + require(len(self.weights) == self.source, 'row width') + require(all(type(x) is int and x >= 0 for x in self.weights), 'positive lower weights') + require(self.mass <= cap(self.u) < F(3,5), 'certified row mass') + require(self.deficit >= 0 and self.terms > 0, 'row error/terms') + + +@lru_cache(None, typed=True) +def prepare_row(source, target, index, u, bits): + for x,lo,name in [(source,1,'source'),(target,1,'target'),(u,1,'u'),(bits,8,'bits >= 8')]: + integer(x,lo,name) + require(type(index) is int and 0 <= index < target, 'row index') + center = F(source*index, target) + radius = max(u, isqrt(u*(bits+16))+2) + first = center.numerator // center.denominator - radius + last = -((-center.numerator)//center.denominator) + radius + denom = 2*sqrt_interval(u,bits) + pi = pi_interval(bits) + weights = [0]*source + deficit = tail_bound(u,radius) + for j in range(first,last+1): + argument = pi * ((F(j)-center)**2/u) + enclosure = exp_negative(argument) / denom + lower = max(0,enclosure.lo) + require(lower <= enclosure.hi, 'positive coefficient enclosure') + weights[j % source] += lower + deficit += F(enclosure.hi-lower, 1 << bits) + row = Row(source,target,index,u,bits,radius,tuple(weights),deficit,last-first+1) + row.check() + return row + + +def prepare(source,target,u,bits): + integer(target,1,'target') + return tuple(prepare_row(source,target,k,u,bits) for k in range(target)) + + +def truncate(numerator, denominator): + return numerator//denominator if numerator >= 0 else -((-numerator)//denominator) + + +def line(values, rows, precision): + integer(precision,1,'positive grid precision') + require(bool(rows), 'nonempty rows') + require(all(isinstance(z,tuple) and len(z)==2 and all(type(c) is int for c in z) + for z in values), 'encoded complex grid') + require(len(values)==rows[0].source, 'source length') + require(all(a*a+b*b <= 1 << (2*precision) for a,b in values), 'unit disk input') + out=[] + for row in rows: + row.check() + require(row == prepare_row(row.source,row.target,row.index,row.u,row.bits), + 'row differs from certified preparation') + require(row.source==len(values), 'row source agreement') + a=sum(w*z[0] for w,z in zip(row.weights,values)) + b=sum(w*z[1] for w,z in zip(row.weights,values)) + out.append((truncate(a,1 << row.bits),truncate(b,1 << row.bits))) + return out + + +def offset(coords, shape): + result=0 + for k,n in zip(coords,shape): + result=result*n+k + return result + + +def window(storage, source_positions, output_positions, rows, precision): + """Host frame adapter: read named sources, change only disjoint outputs.""" + require(len(set(source_positions))==len(source_positions), 'injective source positions') + require(len(set(output_positions))==len(output_positions), 'injective output positions') + require(set(source_positions).isdisjoint(output_positions), 'disjoint borrowed input') + require(len(output_positions)==len(rows), 'complete output window') + result=line([storage[k] for k in source_positions],rows,precision) + dest=storage.copy() + for key,value in zip(output_positions,result): + dest[key]=value + return dest + + +def tensor(values, specs, precision, bits): + """Expand each declared axis once, with independent spectator lines. + + specs is a nonempty tuple of (source, target, u). Returns grid values, + final row-major shape and a rigorously propagated sup-norm error bound. + """ + integer(precision,1,'positive grid precision') + integer(bits,8,'coefficient precision >= 8') + require(bool(specs), 'at least one expansion axis for chirp handoff') + for spec in specs: + require(len(spec)==3, 'axis triple') + for x in spec: integer(x,1,'positive axis parameter') + shape=[s for s,_,_ in specs] + require(len(values)==prod(shape), 'tensor source cardinality') + current=list(values) + norm_bound,error=F(1),F(0) + for axis,(s,t,u) in enumerate(specs): + rows=prepare(s,t,u,bits) + delta=max(r.deficit for r in rows) + nextshape=shape.copy();nextshape[axis]=t + dest=[None]*prod(nextshape) + spectator=[i for i in range(len(shape)) if i != axis] + for coords in product(*(range(shape[i]) for i in spectator)): + index=[0]*len(shape) + for i,k in zip(spectator,coords): index[i]=k + data=[] + for k in range(s): + index[axis]=k; data.append(current[offset(index,shape)]) + result=line(data,rows,precision) + for k,z in enumerate(result): + index[axis]=k;dest[offset(index,nextshape)]=z + error=cap(u)*error+delta*norm_bound+F(2,1 << precision) + norm_bound*=cap(u) + require(all(z is not None for z in dest), 'complete tensor output') + require(all((z[0]*z[0]+z[1]*z[1])*norm_bound.denominator**2 <= + (1 << (2*precision))*norm_bound.numerator**2 for z in dest), + 'tensor hard norm invariant') + current,shape=dest,nextshape + return current,tuple(shape),error,norm_bound diff --git a/research/gaussian-expansion-headroom/inputs/PR3763-PROOF.md b/research/gaussian-expansion-headroom/inputs/PR3763-PROOF.md new file mode 100644 index 0000000000..56b12bd4f0 --- /dev/null +++ b/research/gaussian-expansion-headroom/inputs/PR3763-PROOF.md @@ -0,0 +1,225 @@ +# Complete physical chirp middle map + +Jose Manuel (`jmbarrancoml`), with substantial OpenAI Codex assistance. +I supply an encoded numerical consumer for the retained chirp identity. +I credit Chafik Boukhalfa's PR479 additive residue schedule and Ross +Richardson's PR948 symbolic checks. I retain their source pins and distinguish +this algorithmic argument from the finite evidence in EVIDENCE.md. + +## Contract + +Put r=2^ell. The caller supplies d-1 axis flags; flag 0 means length r/2, +and flag 1 means length r. The final axis has length r. Write +M=product(t_i:i=16, 2<=ell=1, d>=2 and p-A>=13. + +For each axis, the caller supplies an odd integer 0i) < 2T + +axis records, because t_i>=2. The return traversal costs at most the same +order of record movement. Each visit uses O(ell) bit operations: modular +addition needs at most one modulus subtraction, and modular subtraction +uses an ordered difference. I charge O(CT ell) for complete residue walks. +I also charge descriptor validation, initial record reversal and the global +plan compilation; the conservative polynomial setup term below includes +the setup comparisons and encoded cardinality calculations. + +I validate complete binary packets before allocating decoded data roles. +That scan costs linear time in the packet size and permits cleanup after +ordinary malformed-input rejections. I do not claim transactional recovery +from arbitrary injected faults inside a child operation. + +## Numerical dyadic powers + +Let L=ell+1, h=2^-p and + + Q=p+ceil(log2 L)+4, h_Q=2^-Q. + +For the admitted range, 16<=Q<=2p and ell+1<=Q. I compile PR3709's +authenticated TwiddlePlan once at length 2r. I request only indices 2^k, +0<=k 0, "positive divisor") + return -((-a) // b) + + +@dataclass(frozen=True) +class Interval: + lo: int + hi: int + bits: int + + def __post_init__(self): + need(self.lo <= self.hi and self.bits > 0, "interval order/precision") + + @property + def scale(self): + return 1 << self.bits + + @classmethod + def rational(cls, x, bits): + x = F(x) + a = x.numerator * (1 << bits) + return cls(a // x.denominator, ceildiv(a, x.denominator), bits) + + def coerce(self, other): + value = other if isinstance(other, Interval) else self.rational(other, self.bits) + need(value.bits == self.bits, "one working grid") + return value + + def __add__(self, other): + other = self.coerce(other) + return Interval(self.lo + other.lo, self.hi + other.hi, self.bits) + + __radd__ = __add__ + + def __neg__(self): + return Interval(-self.hi, -self.lo, self.bits) + + def __sub__(self, other): + return self + -self.coerce(other) + + def __rsub__(self, other): + return self.coerce(other) - self + + def __mul__(self, other): + other = self.coerce(other) + values = (self.lo * other.lo, self.lo * other.hi, + self.hi * other.lo, self.hi * other.hi) + return Interval(min(values) // self.scale, ceildiv(max(values), self.scale), self.bits) + + __rmul__ = __mul__ + + def divide_integer(self, divisor): + need(divisor > 0, "positive integer denominator") + return Interval(self.lo // divisor, ceildiv(self.hi, divisor), self.bits) + + def reciprocal(self): + need(self.lo > 0, "positive reciprocal enclosure") + return Interval(self.scale**2 // self.hi, ceildiv(self.scale**2, self.lo), self.bits) + + def __truediv__(self, other): + if isinstance(other, int): + return self.divide_integer(other) + return self * self.coerce(other).reciprocal() + + def widen(self, units): + need(units >= 0, "nonnegative enclosure radius") + return Interval(self.lo - units, self.hi + units, self.bits) + + def contains(self, value): + value = F(value) * self.scale + return self.lo <= value <= self.hi + + def overlaps(self, other): + return self.lo <= other.hi and other.lo <= self.hi + + def absolute_upper(self): + return max(abs(self.lo), abs(self.hi)) + + +@lru_cache(None) +def pi_interval(bits): + """Machin identity with the alternating-series remainder, before rounding.""" + def arctan_inverse(q): + total = F(0) + n = 0 + while True: + term = F(1, (2*n+1) * q**(2*n+1)) + total += term if n % 2 == 0 else -term + n += 1 + tail = F(1, (2*n+1) * q**(2*n+1)) + if tail < F(1, 1 << (bits + 16)): + return (total, total + tail) if n % 2 == 0 else (total - tail, total) + a, b = arctan_inverse(5), arctan_inverse(239) + lower, upper = 16*a[0] - 4*b[1], 16*a[1] - 4*b[0] + return Interval(Interval.rational(lower, bits).lo, Interval.rational(upper, bits).hi, bits) + + +def exp_negative(x): + """Enclose exp(-x), x >= 0, by small positive Taylor sums and squaring.""" + need(x.lo >= 0, "nonnegative exponential argument") + scale = x.scale + if x.lo >= x.bits * scale: + # e > 2 and x >= bits: the answer lies strictly below one grid unit. + return Interval(0, 1, x.bits) + halves = 0 + while x.hi > (scale << halves) // 8: + halves += 1 + y = x / (1 << halves) + one = Interval.rational(1, x.bits) + total = term = one + n = 0 + # y <= 1/8, so the omitted positive Taylor tail is at most + # 2*(1/8)^(n+1)/(n+1)!; choose it smaller than one grid unit. + while True: + n += 1 + term = (term * y) / n + total += term + tail = F(2, 8**(n+1) * factorial(n+1)) + if tail < F(1, scale): + total = Interval(total.lo, total.hi + ceildiv(tail.numerator * scale, tail.denominator), x.bits) + break + result = total.reciprocal() + for _ in range(halves): + result = result * result + return Interval(max(0, result.lo), min(scale, result.hi), x.bits) + + +ComplexInterval = tuple[Interval, Interval] + + +def point(real, imag, bits): + return Interval.rational(real, bits), Interval.rational(imag, bits) + + +def cadd(a, b): + return a[0] + b[0], a[1] + b[1] + + +def cneg(a): + return -a[0], -a[1] + + +def cconj(a): + return a[0], -a[1] + + +def cmul(a, b): + return a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0] + + +def cscale(a, real): + return a[0]*real, a[1]*real + + +@lru_cache(None) +def root_of_unity(j, k, bits): + """exp(2 pi i j/k), via rational Taylor remainders; no binary floats.""" + need(k > 0, "positive phase denominator") + j %= k + quadrant = (8*j + k) // (2*k) + residual = F(j, k) - F(quadrant, 4) + x = pi_interval(bits) * (2 * residual) + x2 = x*x + one = Interval.rational(1, bits) + cosine, sine = one, x + cterm, sterm = one, x + n = 0 + while True: + n += 1 + cterm = -(cterm*x2) / ((2*n-1)*(2*n)) + sterm = -(sterm*x2) / ((2*n)*(2*n+1)) + cosine += cterm + sine += sterm + # |x| <= pi/4 < 4/5; alternating Taylor remainders. + ctail = F(4, 5)**(2*n+2) / factorial(2*n+2) + stail = F(4, 5)**(2*n+3) / factorial(2*n+3) + if max(ctail, stail) < F(1, (1 << bits)*16): + cosine = cosine.widen(1) + sine = sine.widen(1) + break + for _ in range(quadrant % 4): + cosine, sine = -sine, cosine + return cosine, sine + + +def inward_quantize(z, precision): + """A p-grid point whose component magnitudes do not exceed any z in box. + + Returns integer numerators and a rigorous l1 (hence modulus) error bound. + """ + bits = z[0].bits + need(bits >= precision and z[1].bits == bits, "quantization grids") + step = 1 << (bits - precision) + out, error = [], 0 + for component in z: + if component.lo > 0: + numerator = component.lo // step + elif component.hi < 0: + numerator = -((-component.hi) // step) + else: + numerator = 0 + encoded = numerator * step + error += max(abs(encoded-component.lo), abs(encoded-component.hi)) + out.append(numerator) + return tuple(out), F(error, 1 << bits) + + +def grid_point(z, precision, bits): + return point(F(z[0], 1 << precision), F(z[1], 1 << precision), bits) + + +def in_disk(z, precision): + return z[0]**2 + z[1]**2 <= 1 << (2*precision) diff --git a/research/gaussian-expansion-headroom/verify.py b/research/gaussian-expansion-headroom/verify.py new file mode 100644 index 0000000000..61c6a83e30 --- /dev/null +++ b/research/gaussian-expansion-headroom/verify.py @@ -0,0 +1,170 @@ +"""Exact finite corroboration of PROOF.md, with a separate dense oracle. +Dugongue, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F +from itertools import product +from math import factorial, isqrt, prod +from pathlib import Path +import argparse +import hashlib +import json + +from expansion import (Interval, cap, line, pi_interval, exp_negative, + prepare, require, tensor, window) + +ROOT=Path(__file__).resolve().parent + + +def oracle(s,t,k,u,bits): + """Independent residue-first enclosure; no prepare_row or tail_bound call. + + Uses the credited interval backend for transcendental enclosures, not an + independent transcendental implementation. The indexing, radius, grouping, + accumulation and dense tensor evaluation are separate. + """ + center=F(s*k,t) + radius=max(u, isqrt(u*(bits+40))+5) + lo=center.numerator//center.denominator-radius + hi=-((-center.numerator)//center.denominator)+radius + scale=1 << bits + root=isqrt(u*scale*scale) + sqrtu=Interval(root,root if root*root==u*scale*scale else root+1,bits) + pi=pi_interval(bits) + answer=[] + for residue in range(s): + total=Interval.rational(0,bits) + for j in range(lo,hi+1): + if (j-residue)%s==0: + x=pi*((F(j)-center)**2/u) + total+=exp_negative(x)/(sqrtu*2) + answer.append((F(total.lo,scale),F(total.hi,scale))) + a=3*radius*radius//u + b=3*(2*radius+1)//u + tail=F(1,1 << a)/(1-F(1,1 << b)) + # The omitted positive mass is at most tail, in total across residues. + return answer,tail + + +def vectors(s,p): + n=1 << p + compass=[(n,0),(-n,0),(0,n),(0,-n),(n//2,n//2), + (-n//2,n//2),(n//2,-n//2),(0,0)] + return [[compass[(3*j+shift)%len(compass)] for j in range(s)] + for shift in range(8)]+[[(n,0)]*s,[(0,-n)]*s] + + +def dense_tensor(data,specs,p,bits): + """One direct Kronecker matrix, without sequential-axis grid rounding.""" + sources=tuple(product(*(range(s) for s,_,_ in specs))) + targets=tuple(product(*(range(t) for _,t,_ in specs))) + matrices=[] + ref_error=F(1) + ideal_norm=F(1) + for s,t,u in specs: + matrix=[];delta=F(0) + for k in range(t): + cells,tail=oracle(s,t,k,u,bits) + matrix.append([(lo+hi)/2 for lo,hi in cells]) + delta=max(delta,tail+sum(hi-lo for lo,hi in cells)) + matrices.append(matrix) + ref_error*=cap(u)+delta + ideal_norm*=cap(u) + out=[] + for dest in targets: + real=imag=F(0) + for src,z in zip(sources,data): + weight=prod(matrices[i][dest[i]][src[i]] for i in range(len(specs))) + real+=weight*F(z[0],1 << p) + imag+=weight*F(z[1],1 << p) + out.append((real,imag)) + return out,ref_error-ideal_norm + + +def run(): + require(sum(F(3)**n/factorial(n) for n in range(10))>20,'e^3 lower certificate') + require(cap(1)==F(21,38) and F(3,5)-cap(1)==F(9,190),'exact headroom') + require(all(F(1,2)