From fbe4214db81fc4ae5f7c1afb5cb9d431784996bc Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:54:26 -0700 Subject: [PATCH 1/2] Prove uniform production-scale Gaussian boundary conditioning --- .../PROOF.md | 224 ++++++++++++++++++ .../README.md | 63 +++++ .../SOURCES.json | 60 +++++ .../TASK.json | 80 +++++++ 4 files changed, 427 insertions(+) create mode 100644 research/production-gaussian-boundary-limit/PROOF.md create mode 100644 research/production-gaussian-boundary-limit/README.md create mode 100644 research/production-gaussian-boundary-limit/SOURCES.json create mode 100644 research/production-gaussian-boundary-limit/TASK.json diff --git a/research/production-gaussian-boundary-limit/PROOF.md b/research/production-gaussian-boundary-limit/PROOF.md new file mode 100644 index 0000000000..90262d4a23 --- /dev/null +++ b/research/production-gaussian-boundary-limit/PROOF.md @@ -0,0 +1,224 @@ +# A uniform production-scale Gaussian boundary limit + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +This is a scoped written theorem with exact finite corroboration, not a +formal-kernel or independent-human proof acceptance. + +## Quantifiers and exact source + +Let h=sqrt(theta), rho=1+theta, N=floor(1/theta), and n=N-1. For +0<=k,i=1}(1-exp(-2tr)), a_b=alpha exp(b/4) P(b)^-3, +and s=sqrt(b)*h. Split the indices at floor(N/2). Embed each left index +as the normalized indicator of [si,s(i+1)) in the first L² half-line; +embed right index i as the corresponding indicator at n-i in the second. +Call this isometry U_s. Let T have kernel +exp(-(y²-x²)) 1{x<=y} on L²(0,infinity). + +Uniformly for + + h -> 0, h^(1/5) <= b <= 1, (1) + +we prove + + || U_s (s A/a_b) U_s* - (T direct-sum T) || -> 0. (2) + +The retained half-line proof establishes ||T||=1/2 using the maximal +first-order operator -d/dx+2x and its Dirichlet adjoint; we retain that +endpoint-domain result. Thus (2) gives the uniform relative asymptotic + + ||K^-1||₂ = (1+o(1)) alpha exp(b/4) + / (2 sqrt(b theta) P(b)^3). (3) + +This extends the predecessor's fixed-alpha theorem to a specified joint +regime. The first retained source case remains alpha=3,theta=1/400,N=400; +that small fixture need not satisfy the eventual domain (1). Source geometry +is checked exactly, not used as evidence that an asymptotic quantifier holds. + +The actual PR4100 setup is alpha=ceil(sqrt((4/pi)log(16p))) and +1/(4p²)<=theta<=1/p². It satisfies (1) eventually, uniformly in theta. +Here p tends through positive integers, logarithms are natural, and the +ceil and floor in the displayed source are retained. This is the untruncated +full cell, not a claim that the existing capped RawGaussian API accepts it. + +## Relative q-product lemma + +Retain the exact q-LDU identity, credited through #1673, #4193, #5103 and +#5150 and the pinned half-line theorem. Set gamma=b/rho, Q=exp(-2gamma), +P_j=product_{r=1}^j(1-Q^r), P=P(gamma). For i<=j define L=N-1-j and + + F_ij=sum_{r=0}^L Q^r P_(j+r)/(P_i P_(j-i+r) P_j P_r). + +Then A_ij=alpha exp(E_ij)F_ij, with + + E_ij=b(theta*j-1/2)²/rho²-gamma*theta*(j²-i²). (4) + +For i>j reflect both indices: i'=n-i,j'=n-j, with i'=1 put + + eps_m=Q^(m+1)/((1-Q)(1-Q^(m+1))). + +If i>=m, j-i>=m, and L>=m, then + + exp(-4 eps_m) <= P³ F_ij <= 1. (6) + +Here are the details that avoid the predecessor's exponentially poor +absolute constants. Write R_j=P_j/P. For j>=m, + + 0<=log R_j=sum_{r>j}-log(1-Q^r) + <=Q^(j+1)/((1-Q)(1-Q^(j+1)))<=eps_m. + +The positive weights w_r=P Q^r/P_r sum to one, since +Q^r/P_r=1/P_r-1/P_(r-1) for r>=1. Moreover +sum_{r=0}^L w_r=P/P_L=1/R_L>=exp(-eps_m). Now + + P³ F_ij=sum_{r=0}^L w_r R_(j+r)/(R_i R_(j-i+r) R_j). + +Each numerator is >=1 and each of the three denominator factors is +<=exp(eps_m), proving the lower bound. For the upper bound, +P_(j+r)/P_j<=1, P_i,P_(j-i+r)>=P, and sum Q^r/P_r<=1/P. +This also proves P³F<=1 outside the good region. No finite product is +silently substituted for P, and the whole r-sum is essential. + +For b<=1, h<=1/2, gamma>=b/2. Logarithmic differentiation gives + + d log P(t)/dt = sum_{r>=1} 2r/(exp(2tr)-1) + <= 2/(1-exp(-b))³ <=16/b³, gamma<=t<=b. + +Consequently, with + + k=exp(48 h²/b²)-1, + +we have 1<=P(b)^3/P(gamma)^3<=1+k. On the good cells, + + |P(b)^3 F_ij-1| <=4(1+k)eps_m+k. (7) + +Everywhere 0<=P(b)^3 F_ij<=1+k. The derivative bound follows from a +convergent geometric majorant, so differentiation under the sum is valid. + +## Uniform operator estimate + +Choose R>=1, J=floor(R/s), m>=1, and assume s<=R/2, +2J<=N, J>=m, and N-J>=m+1. Retain the left upper-triangular J-square +and right strictly-lower J-square, assigning the diagonal only once. +Their images lie in the two different half-line summands. + +In the upper remainder j>=J, j²-i²>=(j-i)J. Each row sum and each +column sum of sA/a_b is at most + + (1+k)s sum_{d>=0} exp(-s² J d/rho) + <=(1+k)(s+rho/(sJ)) <=(1+k)(s+4/R). + +We used rho<=2 and sJ>=R/2. Reflection gives the same estimate on the +lower remainder. This includes middle and cross-edge entries. The +continuum remainder has norm at most 2/R per summand by the analogous +row/column integral; using a sum instead of a maximum only enlarges +our bound. A safe combined discrete/continuum tail allowance is + + 4(1+k)(s+4/R). (8) + +On each retained square, x=s(i+u), y=s(j+v), 0<=u,v<=1. The exponent +bound in the pinned half-line proof, with its window radius replaced +by R/sqrt(b), gives + + |E_ij - (b/4-(y²-x²))| <= D, + D=12(R+1)² h. (9) + +Indeed its bound is 12b(R/sqrt(b)+1)²h, at most (9) when b<=1. +The same calculation covers the reflected offset delta in [1,2). +Both exponents after subtracting b/4 are nonpositive, hence exp has +Lipschitz constant one on their range. + +Cells with i=h^(11/10); thus R/s>=h^(-11/10), + J<=h^(-6/5), while N=floor(h^-2). Hence 2J<=N. +* m<=2h^(-2/5), so J>=m and N-J>=m+1 eventually. +* ms(R+1)<=4h^(3/5): use m<=h^(-1/5)/b+1, + s=h sqrt(b), b>=h^(1/5), and R+1<=2h^(-1/10). +* Q<=exp(-b); bm>=h^(-1/5). Thus + eps_m<=4b^-1 exp(-h^(-1/5)) + <=4h^(-1/5)exp(-h^(-1/5)). +* k<=exp(48h^(8/5))-1, and RD<=48h^(7/10). + +All terms in (10) tend to zero uniformly. In particular the R times +exponential tail vanishes, Rk=O(h^(3/2)), and (8) is O(h^(1/10)). +This proves (2) without exchanging two unquantified limits. + +## Production polynomial conditioning, with ceilings preserved + +Put l=log(16p). The actual alpha satisfies +sqrt(4l/pi)<=alpha=1} f(2br) + <=(1/(2b)) integral_0^infinity f(x)dx + =pi²/(12b). + +The integral follows by the positive exponential series and +sum_{k>=1}1/k²=pi²/6. Therefore P(b)^-3<=exp(pi alpha²/4). +For sufficiently large p, (2) bounds the normalized norm by one, giving + + ||K^-1||₂ <= alpha²/(sqrt(pi)*h) + exp(b/4+pi alpha²/4) + <= 2p alpha²/sqrt(pi) + exp(b/4+l+sqrt(pi*l)+pi/4). (11) + +For every fixed eta>0, the right side is <=p^(2+eta) eventually. +This is a uniform polynomial upper bound, with the asymptotic coefficient +still given exactly by (3). We do not replace its product by an unproved +large-alpha formula, nor assert a sharp p-power lower bound here. +In particular a p^10 allowance eventually dominates this *exact full-cell +inverse norm*. A rounded or truncated reference would additionally need +its own perturbation bound (for example ||K^-1|| ||Delta||<1); this proof +has not admitted such a reference or its circuit. + +## Decision, costs and next obligations + +The fixed-alpha restriction is removed for the actual production scale. +A full-cell conditioning objection based solely on taking alpha to infinity +is therefore resolved for this exact kernel. Existing capped-section +conditioning arguments remain separate, and no existing program is changed. + +The theorem constructs no coefficient producer or inverse-application +algorithm. Common rational reference formation, truncation, grid rounding, +all circuit prefix bounds, coefficient/page storage and physical delivery, +tape movement, preparation amortization and integer recovery retain their +costs and proof obligations. No charge is assigned zero; no runtime, +complete multiplication theorem, supplier admission or new kappa follows. + +Open next questions: bind a specified rounded full-cell reference using +(11) and its actual entry-error invoice; then determine whether any concrete +inverse consumer can exploit the guard while paying all preparation and +physical costs. An arbitrary-section or different-endpoint theorem requires +fresh geometry; the present N, phase and reflection domain must not be dropped. diff --git a/research/production-gaussian-boundary-limit/README.md b/research/production-gaussian-boundary-limit/README.md new file mode 100644 index 0000000000..89efd761d5 --- /dev/null +++ b/research/production-gaussian-boundary-limit/README.md @@ -0,0 +1,63 @@ +# Uniform Gaussian conditioning at the production scale + +The exact full-cell broad Gaussian inverse has the two-edge half-line limit +uniformly when `theta^(1/10) <= b=pi/alpha² <= 1`. This includes the actual +PR4100 choice `alpha=ceil(sqrt((4/pi)log(16p)))`, uniformly for +`1/(4p²)<=theta<=1/p²`. Its inverse norm is eventually at most `p^(2+eta)` +for every fixed `eta>0`. The exact asymptotic coefficient retains the full +infinite product; see [PROOF.md](PROOF.md). + +The predecessor proved the boundary limit only for fixed alpha. Normalizing +finite q-products before estimating them removes the absolute constants that +prevented its production substitution. This is a new quantified analytic +implication, not another finite parameter run or a claim of a faster solver. +The exact original phase, `N=floor(1/theta)`, both boundary layers and the +ceiling in alpha are retained. The first source case is still +alpha3/theta1/400/N400; its geometry is checked without pretending that a +small fixture proves the uniform theorem. + +The small standard-library checker authenticates the retained sources, +checks nonvacuous normalized-product bounds by rational enclosures, compares +the whole q-LDU sum with independent exact elimination, and exercises the +rescaled exponent and floor/ceiling geometry. Controls discriminate dropped +positive summands, omitted distance from the edge, missing sqrt(b) grid +scaling, reflection offsets and mistyped receipts. RESULT.json is mandatory; +ordinary verification does not rewrite it. + +``` +python3.12 -B scripts/research_package.py --package research/production-gaussian-boundary-limit +python3 -B scripts/check_research_commit.py --package research/production-gaussian-boundary-limit --check-source-history +``` + +Both normal and optimized runs are registered. An official committed export +can execute verify.py with its declared inputs without Git or network. +This is a scoped written theorem and finite corroboration, not independent +human or formal-kernel acceptance. No selected frontier changes. + +## Costs and limits + +The full cell is an analytic source matrix, not an admitted capped +RawGaussian program. The result does not price coefficient formation, +truncation, common-reference rounding, prefix amplification, inverse +application, page storage/delivery, tape movement or integer recovery. +These remain obligations rather than zero charges. The existing p^10 +allowance dominates this exact inverse eventually; applying it to a +perturbed reference still requires its actual perturbation invoice. + +## Open next questions + +Bind one explicitly rounded full-cell reference to the new polynomial inverse +bound, then identify an actual consumer whose complete preparation and +physical execution costs justify using it. Different section lengths or +phase endpoints need a separate theorem. TASK.json records first steps. + +Canonical claim: [Discussion4202 comment19172868](https://github.com/CrocSwap/integer-mult-bounds/discussions/4202#discussioncomment-19172868). +Base 32890bc5de034ab8fc93ac88ead7279a6a416d04, priority7. Fresh overlap was +coordinated by the parent before assignment; no global novelty guarantee is +claimed. SOURCES.json binds the exact inherited theorem and source geometry. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +Credit Jose Manuel/#4193, Vlado Vojdanovski/#1673, Cinna Davis/PR4100, +Ryanson Jonathan/#4435, Nick Petalas/#5150, the retained JoyboyBrian +full-cell and half-line work, and the classical q-LDU and product identities. +Frozen predecessors and their notices remain unchanged. diff --git a/research/production-gaussian-boundary-limit/SOURCES.json b/research/production-gaussian-boundary-limit/SOURCES.json new file mode 100644 index 0000000000..c35109bdca --- /dev/null +++ b/research/production-gaussian-boundary-limit/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "NOTICE", + "usage": "input", + "git_blob": "59d8e0cf3102e15bd11db430838365531e2d7f18", + "sha256": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/broad-phase-cell-inverse-bound/verify.py", + "usage": "input", + "git_blob": "c953addeca75ea55d6c5e4e4b9b061fad36b6e6d", + "sha256": "2f7c9e1148a331a01695cf7788cda5a78aa5e63232974e780d9d5733f435eaf2" + }, + { + "path": "research/forward-fine-theta-conditioning/verify.py", + "usage": "input", + "git_blob": "48fdf11e4bb4da2928c439d03f05574f7b2c88a7", + "sha256": "0484ba72b20a805ae2a0e9bde0527f6d048389c6453642d5337064d2da23e547" + }, + { + "path": "research/gaussian-half-line-operator-limit/PROOF.md", + "usage": "input", + "git_blob": "794842c1155fe826742a98e6107256b040a39b9d", + "sha256": "2bf0e36ecd0c3647888e78bc0b8ae30614f5daf07511a4424d69cb3efc29c904" + }, + { + "path": "research/gaussian-half-line-operator-limit/model.py", + "usage": "input", + "git_blob": "06f273150614c4059b07a3d335bf5f5ed37afc1b", + "sha256": "66fa22f545985fcdb40dde5b4668442da56bc8beab9a77a46eeef546de603d0c" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + } + ] +} diff --git a/research/production-gaussian-boundary-limit/TASK.json b/research/production-gaussian-boundary-limit/TASK.json new file mode 100644 index 0000000000..fca0ba12ef --- /dev/null +++ b/research/production-gaussian-boundary-limit/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.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 PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Uniform relative two-edge Gaussian inverse limit including the actual production growing-alpha regime and a polynomial conditioning corollary.", + "scope_change_reason": "The pinned fixed-alpha theorem explicitly excludes production growing alpha; normalized q-products close that quantifier gap.", + "bottleneck_link": "An exact full-cell analytic conditioning implication at actual PR4100 scales; rounded/capped/physical adoption remains separate.", + "budget_minutes": 60, + "stop_rule": "20-minute source/proof gate: require uniform relative control, never infer it from finite samples.", + "outcome": "completed", + "evidence": "PROOF.md, verify.py, RESULT.json", + "author": "JoyboyBrian", + "ai_assistance": "TODO: disclose tools used", + "open_questions": [ + { + "question": "Can an actual rounded full-cell reference use this inverse bound?", + "why_it_matters": "Exact-real conditioning does not certify rounded pages or a solver.", + "first_step": "Specify the complete reference entry-error invoice and bound inverse perturbation using (11).", + "blocked_by": "Actual reference preparation and operator-error budget." + }, + { + "question": "Can a complete physical consumer profit from the guard?", + "why_it_matters": "An analytic improvement alone changes no runtime.", + "first_step": "Bind every inverse call and all setup, delivery, storage and movement charges.", + "blocked_by": "No full-cell physical inverse consumer is supplied." + } + ] +} From 299f129800f3045cc6fafba8e63ad9890aadfe9e Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:54:55 -0700 Subject: [PATCH 2/2] Corroborate uniform q-product bounds with exact falsifying controls --- .../RESULT.json | 150 +++++++++++++++++ .../TASK.json | 2 +- .../VERIFY.json | 36 ++++ .../verify.py | 159 ++++++++++++++++++ 4 files changed, 346 insertions(+), 1 deletion(-) create mode 100644 research/production-gaussian-boundary-limit/RESULT.json create mode 100644 research/production-gaussian-boundary-limit/VERIFY.json create mode 100644 research/production-gaussian-boundary-limit/verify.py diff --git a/research/production-gaussian-boundary-limit/RESULT.json b/research/production-gaussian-boundary-limit/RESULT.json new file mode 100644 index 0000000000..923134e544 --- /dev/null +++ b/research/production-gaussian-boundary-limit/RESULT.json @@ -0,0 +1,150 @@ +{ + "authenticated_inputs": 7, + "relative_products": { + "cases": [ + { + "q": "1/2", + "m": 4, + "N": 14, + "eps": "4/3069", + "normalized_lower_dyadic": "602889407484890852370421/604462909807314587353088", + "normalized_upper_dyadic": "1205778814969781704741099/1208925819614629174706176" + }, + { + "q": "2/3", + "m": 8, + "N": 26, + "eps": "2359296/1935791725", + "normalized_lower_dyadic": "1205982700103643579686311/1208925819614629174706176", + "normalized_upper_dyadic": "602991350051821790546279/604462909807314587353088" + }, + { + "q": "3/4", + "m": 12, + "N": 38, + "eps": "40669853253264/31507404330795169", + "normalized_lower_dyadic": "301452228448837679998961/302231454903657293676544", + "normalized_upper_dyadic": "1205808913795350767406509/1208925819614629174706176" + } + ], + "eliminated_entries": 98, + "controls": [ + "discarded-r-tail", + "missing-edge-distance" + ] + }, + "geometry": { + "source_geometry": { + "source_pairs": 7906, + "offsets": [ + "1", + "3/2", + "4/3" + ], + "first_fixture": { + "alpha": 3, + "theta": "1/400", + "N": 400 + } + }, + "scaled_exponent_checks": 216, + "controls": [ + "missing-sqrt-b-grid", + "retained-floor-offset", + "both-edge-orientations" + ] + }, + "scales": { + "regime_rows": [ + { + "h": "1/1024", + "b": "1", + "m": 4, + "J": 2048, + "N": 1048576 + }, + { + "h": "1/1024", + "b": "1/4", + "m": 16, + "J": 4096, + "N": 1048576 + }, + { + "h": "1/1048576", + "b": "1", + "m": 16, + "J": 4194304, + "N": 1099511627776 + }, + { + "h": "1/1048576", + "b": "1/16", + "m": 256, + "J": 16777216, + "N": 1099511627776 + }, + { + "h": "1/1073741824", + "b": "1", + "m": 64, + "J": 8589934592, + "N": 1152921504606846976 + }, + { + "h": "1/1073741824", + "b": "1/64", + "m": 4096, + "J": 68719476736, + "N": 1152921504606846976 + }, + { + "h": "1/1099511627776", + "b": "1", + "m": 256, + "J": 17592186044416, + "N": 1208925819614629174706176 + }, + { + "h": "1/1099511627776", + "b": "1/256", + "m": 65536, + "J": 281474976710656, + "N": 1208925819614629174706176 + }, + { + "h": "1/1125899906842624", + "b": "1", + "m": 1024, + "J": 36028797018963968, + "N": 1267650600228229401496703205376 + }, + { + "h": "1/1125899906842624", + "b": "1/1024", + "m": 1048576, + "J": 1152921504606846976, + "N": 1267650600228229401496703205376 + }, + { + "h": "1/1152921504606846976", + "b": "1", + "m": 4096, + "J": 73786976294838206464, + "N": 1329227995784915872903807060280344576 + }, + { + "h": "1/1152921504606846976", + "b": "1/4096", + "m": 16777216, + "J": 4722366482869645213696, + "N": 1329227995784915872903807060280344576 + } + ], + "controls": [ + "ceiling-retained", + "typed-bool-int" + ] + }, + "claim": "exact finite corroboration; the uniform production theorem is PROOF.md; no rounded or physical caller admission" +} diff --git a/research/production-gaussian-boundary-limit/TASK.json b/research/production-gaussian-boundary-limit/TASK.json index fca0ba12ef..085f7e0ebe 100644 --- a/research/production-gaussian-boundary-limit/TASK.json +++ b/research/production-gaussian-boundary-limit/TASK.json @@ -62,7 +62,7 @@ "outcome": "completed", "evidence": "PROOF.md, verify.py, RESULT.json", "author": "JoyboyBrian", - "ai_assistance": "TODO: disclose tools used", + "ai_assistance": "Substantial OpenAI Codex assistance in source analysis, proof, exact controls and review.", "open_questions": [ { "question": "Can an actual rounded full-cell reference use this inverse bound?", diff --git a/research/production-gaussian-boundary-limit/VERIFY.json b/research/production-gaussian-boundary-limit/VERIFY.json new file mode 100644 index 0000000000..bd68c3f959 --- /dev/null +++ b/research/production-gaussian-boundary-limit/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "LICENSE", + "NOTICE", + "research/broad-phase-cell-inverse-bound/verify.py", + "research/forward-fine-theta-conditioning/verify.py", + "research/gaussian-half-line-operator-limit/PROOF.md", + "research/gaussian-half-line-operator-limit/model.py", + "research/unconditional-batched-crt/GAUSSIAN.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Source authentication, exact normalized-product and q-LDU controls, rescaled original geometry and typed receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same exact checks with assertions disabled." + } + ] +} diff --git a/research/production-gaussian-boundary-limit/verify.py b/research/production-gaussian-boundary-limit/verify.py new file mode 100644 index 0000000000..069fa9bce4 --- /dev/null +++ b/research/production-gaussian-boundary-limit/verify.py @@ -0,0 +1,159 @@ +"""Exact corroboration of the written uniform theorem, never a limit estimator. +JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib +import importlib.util +import json +from fractions import Fraction as F +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def authenticate(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + count = 0 + for row in manifest['files']: + if row['usage'] == 'input': + payload = (ROOT / row['path']).read_bytes() + need(hashlib.sha256(payload).hexdigest() == row['sha256'], 'source hash: ' + row['path']) + count += 1 + return count + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, ROOT / path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def products(Q, last): + values = [F(1)] + for r in range(1, last + 1): + values.append(values[-1] * (1 - Q**r)) + return values + + +def full_coefficient(Q, n, i, j): + p = products(Q, n) + return sum((Q**r * p[j+r] / (p[i]*p[j-i+r]*p[j]*p[r]) + for r in range(n-j)), F()) + + +def relative_checks(old): + records = [] + for q, m in ((F(1,2),4), (F(2,3),8), (F(3,4),12)): + Q=q*q; n=3*m+2; i=m; j=2*m; last=4*m+20 + p=products(Q,last) + tail=Q**(last+1)/(1-Q) + lo=p[-1]*(1-tail); hi=p[-1] + eps=Q**(m+1)/((1-Q)*(1-Q**(m+1))) + value=full_coefficient(Q,n,i,j) + need(0= 1-4*eps,'certified relative lower bound') + # Even the upper enclosure of P certifies the upper bound in these cases. + need(hi**3*value <= 1,'certified relative upper bound') + need(value == old.coefficient(q,n,i,j),'retained full coefficient equality') + partial=sum((Q**r/p[r] for r in range(m+1)), F()) + need(partial == 1/p[m], 'exact truncated weight telescoping') + first=1/(p[i]*p[j-i]) + need(hi**3*first < 1-4*eps,'dropping positive r-tail falsifies relative bound') + edge=full_coefficient(Q,n,0,j) + need(hi**3*edge < 1-4*eps,'omitting i>=m falsifies relative bound') + records.append({'q':str(q),'m':m,'N':n,'eps':str(eps), + 'normalized_lower_dyadic':str(F(int(lo**3*value*2**80),2**80)), + 'normalized_upper_dyadic':str(F(-int(-hi**3*value*2**80)+1,2**80))}) + # Independent elimination, using the predecessor's separately expressed inverse routine. + entries=0 + for q in (F(1,2),F(2,3)): + for n in (3,5,7): + inverse=old.exact_inverse([[q**((i-j)**2) for j in range(n)] for i in range(n)]) + for i in range(n): + for j in range(i,n): + need(inverse[i][j] == (-1)**(i+j)*q**(j-i)*full_coefficient(q*q,n,i,j), + 'independent exact elimination versus full coefficient') + entries+=1 + return {'cases':records,'eliminated_entries':entries,'controls':['discarded-r-tail','missing-edge-distance']} + + +def scaled_geometry(old, source): + setup, expression=source.source_expression() + original=old.geometry_checks(setup,expression) + checked=0 + for h, sqrtb, R in ((F(1,32),F(1,2),F(2)), + (F(1,64),F(1,4),F(2)), + (F(3,200),F(1,2),F(1))): + b=sqrtb**2; s=h*sqrtb; theta=h*h; n=int(1/theta); J=int(R/s) + need(2*J<=n,'finite geometry admissibility') + for i in sorted({0,1,J//2,J-1}): + for j in sorted({i,min(i+1,J-1),J-1}): + for dx,dy in ((0,0),(0,1),(1,0),(1,1)): + x=s*(i+dx); y=s*(j+dy) + if x>y: + continue + target=b/F(4)-(y*y-x*x) + for u,v in ((i,j),(n-1-i,n-1-j)): + need(abs(b*old.gauge(theta,u,v)-target)<=12*(R+1)**2*h, + 'rescaled compact exponent envelope') + checked+=1 + # The unscaled old cell width would give a different limiting exponent. + need(s*s != h*h,'missing sqrt(b) scaling discriminator') + return {'source_geometry':original,'scaled_exponent_checks':checked, + 'controls':['missing-sqrt-b-grid','retained-floor-offset','both-edge-orientations']} + + +def scale_checks(): + rows=[] + # Exact rational subsequences check exponents, floors and ceilings only. + # The all-real b,h assertion is proved in PROOF.md, not sampled here. + for k in range(1,7): + h=F(1,2**(10*k)); R=2**k + for sqrtb in (F(1), F(1,2**k), F(3,2**(k+2))): + b=sqrtb**2 + if b < F(1,2**(2*k)): + continue + s=h*sqrtb; raw=F(2**(2*k))/b + m=-(-raw.numerator//raw.denominator); J=int(R/s); n=int(1/(h*h)) + need(2*J<=n and J>=m and n-J>=m+1,'joint regime geometry') + need(m*s*(R+1)<=F(4,2**(6*k)),'uniform exceptional-area power') + need(R*12*(R+1)**2*h<=F(48,2**(7*k)),'uniform compact exponent power') + need(48*h*h/(b*b)<=F(48,2**(16*k)),'uniform product-drift power') + rows.append({'h':str(h),'b':str(b),'m':m,'J':J,'N':n}) + # Ceiling alpha is not replaced by its unrounded real precursor. + for t in (F(1,2),F(3,2),F(11,3)): + alpha=-(-t.numerator//t.denominator) + need(t<=alpha