From a2d19a68aa4ebae4eec7685c4d72956ce14682a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?= <97155365+krzysztofwojt@users.noreply.github.com> Date: Fri, 23 Oct 2026 14:04:16 +0200 Subject: [PATCH 1/2] Prove strict all-block projection decrease and sharp geometric tail --- research/projection-finite-infimum/PROOF.md | 253 +++++++++++++ research/projection-finite-infimum/README.md | 124 +++++++ .../projection-finite-infimum/RESULT.json | 73 ++++ .../projection-finite-infimum/SOURCES.json | 33 ++ research/projection-finite-infimum/TASK.json | 106 ++++++ .../projection-finite-infimum/VERIFY.json | 38 ++ research/projection-finite-infimum/verify.py | 332 ++++++++++++++++++ 7 files changed, 959 insertions(+) create mode 100644 research/projection-finite-infimum/PROOF.md create mode 100644 research/projection-finite-infimum/README.md create mode 100644 research/projection-finite-infimum/RESULT.json create mode 100644 research/projection-finite-infimum/SOURCES.json create mode 100644 research/projection-finite-infimum/TASK.json create mode 100644 research/projection-finite-infimum/VERIFY.json create mode 100644 research/projection-finite-infimum/verify.py diff --git a/research/projection-finite-infimum/PROOF.md b/research/projection-finite-infimum/PROOF.md new file mode 100644 index 0000000000..391550eb17 --- /dev/null +++ b/research/projection-finite-infimum/PROOF.md @@ -0,0 +1,253 @@ +# Strict decrease and the sharp infimum of the block-four projection recurrence + +Prepared by Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. + +This is a theorem about the **unstrengthened arithmetic recurrence** below. +Jacob Alan Sussman (#4628) supplies its engine interpretation and seed; +Maximilian Lutz (#4643) independently derived the projection counts and checked +a finite prefix plus a conservative tail. Nick Petalas (#5151) proved the exact +limit. We use that credited limit theorem; our additions are strict monotonicity +at every block, the sharp infimum, and a two-sided geometric error estimate. +The hook ranks and representation/engine hypotheses are not re-audited here. + +## 1. Statement and inherited limit + +Start with + +``` +a_4 = (0, 27456, 48576, 68320, 86592). +``` + +For integers k >= 5, define a_k(r), 0 <= r <= k, by + +``` +a_k(r) = N_k(r,r) a_(k-1)(r) + + N_k(r,r-1) a_(k-1)(r-1) + + N_k(r,r-2) a_(k-1)(r-2), + +N_k(r,r) = 2^(k-r)-1 + 4^k-2^(k+r), +N_k(r,r-1) = 2(2^k-2^(k-r)) + (2^r-1)2^(k-1), +N_k(r,r-2) = (2^r-1)(2^(r-1)-1)2^(k-r). +``` + +Omit out-of-range terms; the third coefficient is zero for r < 2. +Write T_m = a_m(m)/a_m(1). No triangle/max strengthening is applied. + +**Theorem.** For every integer m >= 4, T_(m+1) < T_m. Moreover, + +``` +inf_(m>=4) T_m = L = 439277/149175, +2^(-m) < T_m - L < 2^(1-m) for every m >= 5. +``` + +In particular the infimum is never attained, and the error has order 2^(-m). +The theorem does not assert that every nonnegative seed is monotone. + +The equality lim T_m = L is Petalas's theorem at +`e6c8e945a47dcc4a6f08974682090fc7f5e221a3`, +`research/projection-recursion-limit/PROOF.md`, Sections 1--4. Its general formula +specializes to + +``` +L = (11/10) (30 + 280*(48576/27456) + + 960*(68320/27456) + 1024*(86592/27456)) / 2295. +``` + +This source's SHA256 is +`83843a1460d8d5ccca4c312268e3a138f5dddc8197986ba63955392a3da0da33`. +The exact rational simplification is checked locally. Reusing this limit is +explicit: a finite prefix alone would not justify the displayed infimum. + +## 2. A fixed triangular operator and four exact modes + +Put x=2^k and y=2^r. On sequences f(0)=0, the raw row operator is +`N_k = d_k I + x H`, where + +``` +d_k = (2^(k-1)-1)(2^(k+1)+1), +(Hf)(r) = h_r f(r) + B_r f(r-1) + C_r f(r-2), +h_r = 3/2 + 2^(-r) - 2^r, +B_r = 2^(r-1) + 3/2 - 2^(1-r), +C_r = 2^(r-1) - 3/2 + 2^(-r). +``` + +Terms below zero are omitted. At r=1, h_1=0; hence a_k(1)=d_k a_(k-1)(1). +The normalized profile therefore evolves by `I + (2^k/d_k) H`. +The same H works at every k. At the new endpoint r=k the coefficient +N_k(k,k)=0, so no value of the old profile outside its range is needed. + +The numbers h_r strictly decrease for r>=1. For j=1,2,3,4 define the sequence +e_j by e_j(r)=0 for rj, + +``` +e_j(r) = (B_r e_j(r-1) + C_r e_j(r-2)) / (h_j-h_r). (2.1) +``` + +It satisfies H e_j = h_j e_j on every positive row. This follows immediately +from (2.1), including the zero rows below j. The unit lower triangular seed +matrix e_j(r), 1<=j,r<=4, uniquely gives + +``` +(c_1,c_2,c_3,c_4) = (1, 17/39, 6181/14586, 99085/239811), +a_4(r)/a_4(1) = sum_(j=1)^4 c_j e_j(r), 0<=r<=4. (2.2) +``` + +All four coefficients are positive. Define, for m>=4, + +``` +lambda_(k,j) = (2^(k-j)-1)(2^(k+j)+1) = d_k + 2^k h_j, +p_(m,j) = product_(k=5)^m lambda_(k,j)/d_k, +u_(m,j) = p_(m,j) e_j(m). +``` + +The empty product is one. All factors in these products are positive. +Induction on m, using H e_j=h_j e_j and N_m(m,m)=0 at the new row, proves + +``` +a_m(r)/a_m(1) = sum_(j=1)^4 c_j p_(m,j) e_j(r), +T_m = sum_(j=1)^4 c_j u_(m,j). (2.3) +``` + +Thus only four modes are required; this is an exact representation, not a +numerically fitted formula. The e_j are still defined by a second-order +recurrence; no elementary closed form for them is claimed. + +For m>=6, apply the eigenvector identity to row r=m at block m, and multiply +by p_(m-1,j)/d_m. It gives the scalar second-order recurrence + +``` +u_m = alpha(x) u_(m-1) + beta_h(x) u_(m-2), x=2^m, +alpha(x) = (x-1)(x+4) / ((x-2)(2x+1)), +beta_h(x) = (x-1)/(2x+1) * (1 + 2xh/((x-4)(x+1))), (2.4) +``` + +where h=h_j. Initial values u_4,u_5 come from (2.1)--(2.3). + +## 3. An involution controls the entire tail + +Set z_m=2^m(u_m-u_(m-1)), v_m=(u_m,z_m)^t, and + +``` +F_h(x) = x*(alpha(x)+beta_h(x)-1), +A_h(x) = [[1+F_h(x)/x, -2 beta_h(x)/x], + [F_h(x), -2 beta_h(x) ]], +J_h = [[1,0],[h+3/2,-1]]. +``` + +Equation (2.4) is exactly v_m=A_h(2^m)v_(m-1), and J_h^2=I. +Use the maximum vector norm and its induced row-sum matrix norm. + +**Uniform bound.** If -15<=h<=0 and x>=64, then + +``` +||J_h|| <= 16, +||A_h(x)-J_h|| <= 128/x, +||A_h(2x) A_h(x)-I|| <= 4096/x. (3.1) +``` + +Here are explicit elementary bounds proving every quantifier in (3.1). +In beta_h the parenthesized factor is between 1/2 and 1, because +`|2xh/((x-4)(x+1))| <= 30/(x-4) <= 1/2`. Consequently 0<=beta_h<=1/2, +and + +``` +0 <= 1-2 beta_h(x) <= 3/(2x) + 30/(x-4) <= 40/x. +``` + +Direct expansion gives + +``` +F_h(x)-(h+3/2) + = ((6h+9)x^3 + (10h-21)x^2 - (36h+54)x - (16h+24)) + / (2(x-4)(x-2)(x+1)(2x+1)). (3.2) +``` + +The absolute numerator is at most `99x^3+171x^2+594x+264 <= 104x^3`; +the denominator is at least `3x^4`. Thus the absolute difference is <64/x, +and |F_h(x)|<15. The first row of A_h-J_h has norm at most 16/x, and the +second at most 104/x, proving the second bound in (3.1). +Writing A_h=J_h+E_h proves the third: + +``` +||J_h E_h(x) + E_h(2x) J_h + E_h(2x) E_h(x)|| + <= 3072/x + 8192/x^2 <= 3200/x <= 4096/x. +``` + +All four h_j lie in [-15,0]. From (3.1), the two-step update from v_m to +v_(m+2), for m>=5, differs from I by at most 2048*2^(-m). +Fix a parity starting at M, and put + +``` +S_M = sum_(i>=0) 2048*2^(-M-2i) = 8192/(3*2^M). +``` + +If S_M<1, every finite product of these two-step matrices differs from I +by at most S_M/(1-S_M). Indeed its norm difference is bounded by the product +of (1+2048*2^(-M-2i)) minus one. Expanding that product and bounding its +degree-n elementary symmetric sum by S_M^n gives the claimed geometric bound. +This argument needs no commutativity, diagonalization, or convergence assumption. +For every m>=M of the same parity, + +``` +||v_m-v_M|| <= S_M/(1-S_M) * max(|u_M|,|z_M|). (3.3) +``` + +## 4. The finite exact certificate and strict monotonicity + +The standalone verifier obtains u_(M,j),z_(M,j) from the four modes with +Fraction arithmetic. It independently constructs the original integer +triangle through block 48 and compares the whole normalized profile, not just +the top values. The actual infinite-tail certificate uses only M=32 and 33. +Let + +``` +Z_M = sum_j c_j z_(M,j) = 2^M(T_M-T_(M-1)), +R_M = S_M/(1-S_M) * sum_j |c_j| max(|u_(M,j)|,|z_(M,j)|). +``` + +The following are exact rational enclosures checked by integer comparisons: + +| M | enclosure for Z_M | strict upper bound for R_M | +|---|---|---| +| 32 | (-858261/10^6, -858260/10^6) | 3/10^6 | +| 33 | (-1873709/10^6, -1873708/10^6) | 2/10^6 | + +By (2.3) and (3.3), the same-parity scaled differences are contained in +(Z_M-R_M,Z_M+R_M). In particular, for every m>=32, + +``` +-9/10 < 2^m(T_m-T_(m-1)) < -4/5 if m is even, +-2 < 2^m(T_m-T_(m-1)) < -9/5 if m is odd. (4.1) +``` + +These are negative intervals with substantial exact slack. The original +integer recurrence also verifies T_m=32, +17/15 < 2^m(T_m-L) < 19/15 for odd m>=33. +``` + +Both intervals lie inside (1,2). Exact checks of `1 < 2^m(T_m-L) < 2` +for 5<=m<=31 supply the finite prefix. This proves the stated geometric +estimate, strict nonattainment, and exact infimum. + +## 5. Scope and remaining obligations + +The written operator and tail inequalities supply the universal quantifiers; +the finite exact certificate supplies the two initial tail states and finite +prefix. Automated execution alone is not a proof-kernel or independent human +review. The credited #5151 limit theorem remains a mathematical dependency. +The same proof does not establish monotonicity for every seed: the seed +(0,1,1,1,1) already increases at the next block and is a rejection control. + +No hook rank, engine embedding, physical circuit, dirty-state restoration, +complete recursive price, supplier admission, multiplication exponent, or +selected frontier is established or modified. A characterization of all seeds +with monotone top ratios and elementary closed forms for the mode sequences +remain open. The optional triangle/max strengthening is a different recurrence. diff --git a/research/projection-finite-infimum/README.md b/research/projection-finite-infimum/README.md new file mode 100644 index 0000000000..e3bf41786f --- /dev/null +++ b/research/projection-finite-infimum/README.md @@ -0,0 +1,124 @@ +# Strictly decreasing projection ratios and their exact infimum + +For the unstrengthened projection recurrence with block-four seed +`(0,27456,48576,68320,86592)`, this package proves + +``` +T_(m+1) < T_m for every m >= 4, +inf T_m = L = 439277/149175, +2^(-m) < T_m-L < 2^(1-m) for every m >= 5. +``` + +Here `T_m=a_m(m)/a_m(1)`. The exact limit L is Nick Petalas's +[#5151](https://github.com/CrocSwap/integer-mult-bounds/pull/5151) theorem. +The **new results** are strict all-block monotonicity, nonattainment of the +sharp infimum, and a two-sided geometric error bound. They resolve the +original-seed monotonicity/infimum question and improve the conservative +convergence rate explicitly left open there. This is a scoped arithmetic +proof with an exact finite certificate, not a new kappa or supplier. + +## Proof and evidence + +[PROOF.md](PROOF.md) gives the complete argument. Normalizing the recurrence +reveals a single triangular operator and four exact modes. Each mode's scaled +increment has a two-dimensional transfer approaching an involution. The +two-step error is summable; exact states at blocks 32 and 33 therefore certify +the whole infinite tail. A finite prefix completes the monotonicity theorem. +This explains why checking more decimal values alone would not suffice. + +[verify.py](verify.py) uses only integers and `fractions.Fraction`, reads no +external files, and writes nothing. Its deterministic output is retained in +[RESULT.json](RESULT.json). The check covers: + +- 1,215 normalized profile equalities against a separately written literal + integer recurrence, over blocks 4 through 48; +- 172 scalar recurrence and 172 scaled-state transfer identities; +- a bivariate polynomial identity for the uniform remainder, its rational + bound constants, and 49 separately labelled finite lemma fixtures; +- both infinite-tail certificates, exact finite-prefix inequalities, and ten + rejection controls (wrong recurrence, seed, domain, perturbation bound, + involution sign, summability premise, parity, limit, or seed universality). + +The universal inequalities are proved in writing. Executing the finite +certificate does not independently audit the written proof or the inherited +limit theorem. Normal and optimized Python runs use explicit checks, not +disableable assertions. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/projection-finite-infimum +python3.12 -I -X dev -W error -B research/projection-finite-infimum/verify.py +python3.12 -I -O -X dev -W error -B research/projection-finite-infimum/verify.py +python3.12 -B scripts/check_research_commit.py --package research/projection-finite-infimum --check-source-history +``` + +Expected markers: `PASS_PROJECTION_FINITE_INFIMUM`, +`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. +Direct verification takes less than a second on the author's macOS arm64 host +with CPython 3.12.12; this is an observation, not a performance claim. The direct +commands also work from a read-only, Git-free package export. The registered +runner needs Git history for provenance. No third-party dependencies are used. + +## Sources, overlap, and limits + +Fresh base: `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7. +The selected source/metadata baseline passed; no selected scientific replay was +needed or run. [TASK.json](TASK.json) records the handoff-first scope change from +`independent-moment`; [claim #5169](https://github.com/CrocSwap/integer-mult-bounds/discussions/5169) +is the canonical investigation record. + +- Jacob Alan Sussman [#4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628) + supplies the hook seed, recurrence, and engine interpretation; head inspected: + `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`. +- Maximilian Lutz / lm1909 [#4643](https://github.com/CrocSwap/integer-mult-bounds/pull/4643) + independently derived the counts, checked the finite prefix, and proved the + earlier conservative all-block bound. Its retained README is pinned as + provenance in [SOURCES.json](SOURCES.json). Its unresolved hook-rank inputs + remain unresolved here. The central ledger marks #4628/#4643 partially reviewed. +- Nick Petalas's [exact limit proof](https://github.com/CrocSwap/integer-mult-bounds/blob/e6c8e945a47dcc4a6f08974682090fc7f5e221a3/research/projection-recursion-limit/PROOF.md) + at `e6c8e945a47dcc4a6f08974682090fc7f5e221a3` is a **cited mathematical + dependency**, not an imported executable or an independently replayed result. + Its exact proof hash and specialized theorem are recorded in PROOF.md and + SOURCES.json. Publication and passing CI do not imply scientific acceptance; + #5151 was merged during this investigation, without changing its cited head. + +The pre-claim search covered 331 open PRs, 4,339 Discussion records, and 6,918 +main-tree notes, followed by live recent-claim/PR and closed-PR term checks. +The nearby same-account Gram and R437 claims and all earlier excluded topics +were left alone. Search coverage excludes unpublished work and arbitrary diffs. +The final live overlap refresh is recorded in the PR and canonical thread. + +The result is about this seed and this recurrence. It does not provide an +elementary closed form for the mode sequences or classify every seed. The +optional triangle/max strengthening is outside scope. Hook ranks, engine +premises, physical realization, dirty restoration, complete recursive pricing, +native/outer admission, Lean, and independent human review remain unverified. +No selected frontier is changed. + +## Open next questions + +1. Which other seed profiles have monotone top ratios? This would make the + projection method's best all-block bound decidable for new hook data. + Start by applying the four-mode tail certificate to adjacent-difference + linear functionals of a general block-four seed. An exact characterization + must handle equality on the limiting parity boundaries; finite tests do not. +2. Can the mode sequences admit elementary or q-series closed forms? This + could give exact parity-sensitive leading error constants. Start from + (2.1) and the fixed triangular operator. This package proves neither such a + form nor the optimal constants in its geometric enclosure. + +## Credit + +Prepared by Krzysztof Wojt with substantial OpenAI Codex assistance. A Luna +worker assisted with a read-only claim inventory, bounded exact coefficient +fixtures, and an arithmetic/indexing review; final decisions and integration +remained with the primary agent. SymPy was used for exploratory algebra only; +the published certificate uses the standard library. No independent human or +proof-kernel acceptance is claimed. + +Credit Sussman, Lutz, Petalas, eumemic (#288), Swapnil Jain, and the retained +certificate-method/engine lineage. This new work is Apache-2.0. Frozen +predecessor files, shared tooling, and the selected record remain unchanged. diff --git a/research/projection-finite-infimum/RESULT.json b/research/projection-finite-infimum/RESULT.json new file mode 100644 index 0000000000..45b8c462ca --- /dev/null +++ b/research/projection-finite-infimum/RESULT.json @@ -0,0 +1,73 @@ +{ + "claim_type": "scoped arithmetic proof with exact finite tail certificate", + "finite_monotonicity_and_error_blocks": [ + 5, + 48 + ], + "full_profile_equalities": 1215, + "limit_from_pr5151": "439277/149175", + "new_kappa": false, + "rejected_controls": [ + "omit distance-two term", + "perturb fourth mode coefficient", + "domain x below 64", + "eigenvalue outside uniform domain", + "understate matrix perturbation", + "lose involution sign", + "tail product without S less than one", + "apply even interval to odd tail", + "perturb inherited limit", + "claim all nonnegative seeds decrease" + ], + "scalar_mode_equalities": 172, + "scaled_state_equalities": 172, + "seed": [ + 0, + 27456, + 48576, + 68320, + 86592 + ], + "seed_coefficients": [ + "1", + "17/39", + "6181/14586", + "99085/239811" + ], + "status": "PASS_PROJECTION_FINITE_INFIMUM", + "symbolic_F_remainder_identity": true, + "tail_certificates": [ + { + "all_same_parity_scaled_differences": [ + "-9/10", + "-4/5" + ], + "center_interval": [ + "-858261/1000000", + "-42913/50000" + ], + "radius_less_than": "3/1000000", + "start": 32 + }, + { + "all_same_parity_scaled_differences": [ + "-2", + "-9/5" + ], + "center_interval": [ + "-1873709/1000000", + "-468427/250000" + ], + "radius_less_than": "1/500000", + "start": 33 + } + ], + "uniform_lemma_fixtures": 49, + "unrun": [ + "hook ranks", + "physical/recursive admission", + "selected cold replay", + "Lean", + "independent human review" + ] +} diff --git a/research/projection-finite-infimum/SOURCES.json b/research/projection-finite-infimum/SOURCES.json new file mode 100644 index 0000000000..624db878d8 --- /dev/null +++ b/research/projection-finite-infimum/SOURCES.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/projection-recursion-check/README.md", + "usage": "provenance", + "git_blob": "1d8c9f7b1b96cd098a9a00a90022143bbced8b64", + "sha256": "59204f11aa3aae59df44fc69228cd017660139587b2dc18ece1999a98d097996" + } + ], + "cited_mathematical_dependency": { + "author": "Nick Petalas", + "pull_request": 5151, + "head": "e6c8e945a47dcc4a6f08974682090fc7f5e221a3", + "path": "research/projection-recursion-limit/PROOF.md", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/e6c8e945a47dcc4a6f08974682090fc7f5e221a3/research/projection-recursion-limit/PROOF.md", + "sha256": "83843a1460d8d5ccca4c312268e3a138f5dddc8197986ba63955392a3da0da33", + "scope": "Cited exact limit theorem; not an executable input or independently reproduced proof. No source from the cited commit is needed for replay." + } +} diff --git a/research/projection-finite-infimum/TASK.json b/research/projection-finite-infimum/TASK.json new file mode 100644 index 0000000000..b41abf003c --- /dev/null +++ b/research/projection-finite-infimum/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove strict all-block decrease, sharp infimum 439277/149175, and 2^-m < T_m-L < 2^(1-m) for the unstrengthened block-four projection recurrence, using the credited exact limit of PR5151.", + "scope_change_reason": "Handoff-first override: PR5151 explicitly leaves finite-size formulas, monotonicity and the all-block infimum open. This investigates a new arithmetic implication, not another moment-root replay.", + "bottleneck_link": "Scoped side theorem for complex-engine projection lower bounds: replaces a conservative finite-tail floor by the exact infimum and a sharp-order geometric convergence bound. Hook and engine assumptions remain inherited; no supplier or kappa claim.", + "budget_minutes": 210, + "stop_rule": "One-hour algebraic gate; stop or narrow if only the known limit is recovered. At most one focused result; no hook-rank recomputation, physical implementation or new kappa.", + "outcome": "completed", + "evidence": "PROOF.md universal operator/tail inequalities; verify.py exact finite certificate: 1215 full-profile equalities, 172 scalar and 172 scaled-state identities, polynomial remainder identity, 49 uniform-lemma fixtures, checkpoints 32/33 and ten rejecting controls.", + "author": "Krzysztof Wojt", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, and writing. A Luna worker assisted with read-only claim inventory, bounded exact fixtures, and arithmetic/indexing review. SymPy was used only for exploration; published replay is Python standard library.", + "open_questions": [ + { + "question": "Characterize block-four seed profiles whose top ratios are monotone.", + "why_it_matters": "Decides whether the limiting lower bound is the best all-block bound for new hook profiles.", + "first_step": "Apply the four-mode tail certificate to adjacent-difference linear seed functionals.", + "blocked_by": "Equality on limiting parity boundaries needs a sharp analysis; finite testing does not characterize the entire cone." + }, + { + "question": "Find elementary or q-series expressions for the mode sequences and exact leading parity constants.", + "why_it_matters": "May replace the conservative geometric constants by sharp asymptotics.", + "first_step": "Analyze the second-order eigenvector recurrence (2.1) for the fixed triangular operator.", + "blocked_by": "No elementary closed form or optimal leading constants are supplied here." + } + ] +} diff --git a/research/projection-finite-infimum/VERIFY.json b/research/projection-finite-infimum/VERIFY.json new file mode 100644 index 0000000000..3040e9204a --- /dev/null +++ b/research/projection-finite-infimum/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact four-mode/full-profile identity, polynomial uniform remainder, infinite-tail certificate, finite prefix and ten semantic rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact four-mode/full-profile identity, polynomial uniform remainder, infinite-tail certificate, finite prefix and ten semantic rejection controls under optimization" + } + ] +} diff --git a/research/projection-finite-infimum/verify.py b/research/projection-finite-infimum/verify.py new file mode 100644 index 0000000000..40ae4895fc --- /dev/null +++ b/research/projection-finite-infimum/verify.py @@ -0,0 +1,332 @@ +#!/usr/bin/env python3 +"""Exact certificate for the block-four projection infimum and geometric tail. + +Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0. +Standard library, no network/Git/source imports, no writes, no assert statements. +The universal argument is in PROOF.md; finite tests are labelled separately. +""" + +from fractions import Fraction as Q +import json + + +SEED = (0, 27456, 48576, 68320, 86592) +LIMIT = Q(439277, 149175) # Petalas #5151, exact pinned theorem in PROOF.md. +COEFFICIENTS = (Q(1), Q(17, 39), Q(6181, 14586), Q(99085, 239811)) +MAX_BLOCK = 48 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def expect_rejection(operation): + try: + operation() + except ValueError: + return + raise ValueError("negative control was accepted") + + +def raw_step(old, k, omit_two_drop=False): + """Literal integer recurrence, independent of the mode implementation.""" + require(len(old) == k, "wrong old profile length") + result = [] + for r in range(k + 1): + value = 0 + if r < k: + value += (2**(k-r) - 1 + 4**k - 2**(k+r)) * old[r] + if r >= 1: + value += (2*(2**k - 2**(k-r)) + + (2**r - 1)*2**(k-1)) * old[r-1] + if r >= 2 and not omit_two_drop: + value += (2**r - 1)*(2**(r-1) - 1)*2**(k-r) * old[r-2] + result.append(value) + return result + + +def diagonal(k, j): + require(1 <= j <= k, "diagonal domain") + return (2**(k-j) - 1)*(2**(k+j) + 1) + + +def h(j): + return Q(3, 2) + Q(1, 2**j) - 2**j + + +def mode(j, maximum): + values = [Q(0)]*j + [Q(1)] + for r in range(j+1, maximum+1): + y = 2**r + b = Q(y+3, 2) - Q(2, y) + c = Q(y-3, 2) + Q(1, y) + values.append((b*values[r-1] + c*values[r-2]) / (h(j)-h(r))) + return values + + +def reconstruct_seed(modes, coefficients): + return [sum(coefficients[j-1]*modes[j][r] for j in range(1, 5)) + for r in range(5)] + + +def alpha(x): + return Q((x-1)*(x+4), (x-2)*(2*x+1)) + + +def beta(x, eigenvalue): + return Q(x-1, 2*x+1) * (1 + Q(2*x, (x-4)*(x+1))*eigenvalue) + + +def transfer(x, eigenvalue): + b = beta(x, eigenvalue) + f = x*(alpha(x)+b-1) + return ((1+f/x, -2*b/x), (f, -2*b)) + + +def involution(eigenvalue): + return ((Q(1), Q(0)), (eigenvalue+Q(3, 2), Q(-1))) + + +def matrix_product(a, b): + return tuple(tuple(sum(a[i][k]*b[k][j] for k in range(2)) + for j in range(2)) for i in range(2)) + + +def matrix_difference(a, b): + return tuple(tuple(a[i][j]-b[i][j] for j in range(2)) for i in range(2)) + + +def matrix_norm(a): + return max(sum(abs(value) for value in row) for row in a) + + +def matrix_vector(a, v): + return tuple(sum(a[i][j]*v[j] for j in range(2)) for i in range(2)) + + +IDENTITY = ((Q(1), Q(0)), (Q(0), Q(1))) + + +# Bivariate polynomial arithmetic; keys are powers of (x,h). This checks the +# displayed identity as a polynomial identity, not merely at sampled points. +def poly_add(*polynomials): + result = {} + for p in polynomials: + for powers, value in p.items(): + result[powers] = result.get(powers, Q(0)) + value + return {powers: value for powers, value in result.items() if value} + + +def poly_scale(p, scalar): + return {powers: value*scalar for powers, value in p.items() if value*scalar} + + +def poly_mul(*polynomials): + result = {(0, 0): Q(1)} + for p in polynomials: + new = {} + for (i, j), a in result.items(): + for (k, ell), b in p.items(): + key = (i+k, j+ell) + new[key] = new.get(key, Q(0)) + a*b + result = {powers: value for powers, value in new.items() if value} + return result + + +def check_symbolic_identity(): + one = {(0, 0): Q(1)} + x = {(1, 0): Q(1)} + hp = {(0, 1): Q(1)} + + def shifted(a, b): + return poly_add(poly_scale(x, a), poly_scale(one, b)) + + an = poly_mul(shifted(1, -1), shifted(1, 4)) + ad = poly_mul(shifted(1, -2), shifted(2, 1)) + bn = poly_mul(shifted(1, -1), poly_add( + poly_mul(shifted(1, -4), shifted(1, 1)), poly_scale(poly_mul(x, hp), 2))) + bd = poly_mul(shifted(2, 1), shifted(1, -4), shifted(1, 1)) + fn = poly_mul(x, poly_add(poly_mul(an, bd), poly_mul(bn, ad), + poly_scale(poly_mul(ad, bd), -1))) + fd = poly_mul(ad, bd) + difference_numerator = poly_add(fn, poly_scale(poly_mul( + poly_add(hp, poly_scale(one, Q(3, 2))), fd), -1)) + displayed_numerator = { + (3, 1): Q(6), (3, 0): Q(9), (2, 1): Q(10), (2, 0): Q(-21), + (1, 1): Q(-36), (1, 0): Q(-54), (0, 1): Q(-16), (0, 0): Q(-24)} + displayed_denominator = poly_scale(poly_mul( + shifted(1, -4), shifted(1, -2), shifted(1, 1), shifted(2, 1)), 2) + require(poly_mul(difference_numerator, displayed_denominator) + == poly_mul(displayed_numerator, fd), "F remainder polynomial identity") + require(Q(3, 2)+30*Q(16, 15) < 40, "beta remainder constant") + require(99+Q(171, 64)+Q(594, 64**2)+Q(264, 64**3) < 104, + "numerator majorant") + require(4*Q(15, 16)*Q(31, 32) > 3, "denominator minorant") + require(Q(104, 3) < 64, "F remainder constant") + require(16*128+64*16+Q(8192, 64) <= 4096, "two-step constant") + + +def check_uniform_fixture(x, eigenvalue, remainder_constant=128): + require(x >= 64 and -15 <= eigenvalue <= 0, "uniform lemma domain") + j = involution(eigenvalue) + a = transfer(x, eigenvalue) + require(matrix_product(j, j) == IDENTITY, "J squared") + require(matrix_norm(j) <= 16, "J norm") + require(matrix_norm(matrix_difference(a, j)) <= Q(remainder_constant, x), + "one-step perturbation bound") + require(matrix_norm(matrix_difference(matrix_product( + transfer(2*x, eigenvalue), a), IDENTITY)) <= Q(4096, x), + "two-step perturbation bound") + + +def tail_enclosure(u, coefficients, start): + require(start >= 5, "two-step domain") + s = Q(8192, 3*2**start) + require(s < 1, "summable product bound needs S < 1") + center, radius = Q(0), Q(0) + for j in range(1, 5): + z = 2**start*(u[j][start]-u[j][start-1]) + norm = max(abs(u[j][start]), abs(z)) + center += coefficients[j-1]*z + radius += abs(coefficients[j-1])*s/(1-s)*norm + return center, radius + + +def certify_interval(center, radius, low, high): + require(radius >= 0 and low < center-radius and center+radius < high, + "tail interval not certified") + + +def check_error(top, m, limit=LIMIT): + require(Q(1, 2**m) < top-limit < Q(2, 2**m), "geometric error enclosure") + + +def main(): + check_symbolic_identity() + inherited_limit = Q(11, 10)*(30 + 280*Q(SEED[2], SEED[1]) + + 960*Q(SEED[3], SEED[1]) + + 1024*Q(SEED[4], SEED[1]))/2295 + require(inherited_limit == LIMIT, "cited limit specialization") + modes = {j: mode(j, MAX_BLOCK) for j in range(1, 5)} + require(all(c > 0 for c in COEFFICIENTS), "positive seed coefficients") + expected_seed = [Q(a, SEED[1]) for a in SEED] + require(reconstruct_seed(modes, COEFFICIENTS) == expected_seed, "seed decomposition") + + raw = list(SEED) + products = {j: Q(1) for j in range(1, 5)} + u = {j: {} for j in range(1, 5)} + tops = {} + profile_checks = 0 + scalar_checks = 0 + matrix_checks = 0 + for m in range(4, MAX_BLOCK+1): + if m > 4: + old_one = raw[1] + raw = raw_step(raw, m) + require(raw[1] == old_one*diagonal(m, 1), "denominator identity") + for j in products: + require(diagonal(m, j) == diagonal(m, 1)+2**m*h(j), + "raw eigenvalue identity") + products[j] *= Q(diagonal(m, j), diagonal(m, 1)) + for r in range(m+1): + reconstructed = sum(COEFFICIENTS[j-1]*products[j]*modes[j][r] + for j in range(1, 5)) + require(reconstructed == Q(raw[r], raw[1]), "full profile identity") + profile_checks += 1 + tops[m] = Q(raw[-1], raw[1]) + for j in products: + u[j][m] = products[j]*modes[j][m] + if m >= 6: + require(u[j][m] == alpha(2**m)*u[j][m-1] + + beta(2**m, h(j))*u[j][m-2], "scalar mode recurrence") + scalar_checks += 1 + before = (u[j][m-1], 2**(m-1)*(u[j][m-1]-u[j][m-2])) + after = (u[j][m], 2**m*(u[j][m]-u[j][m-1])) + require(matrix_vector(transfer(2**m, h(j)), before) == after, + "scaled state transfer") + matrix_checks += 1 + if m > 4: + require(tops[m] < tops[m-1], "finite-prefix strict decrease") + check_error(tops[m], m) + require([tops[k] for k in (4, 5, 6)] + == [Q(41, 13), Q(834241, 278850), Q(1188222, 399685)], "calibrations") + + tail_rows = [] + for start, coarse_center, radius_bound, interval in ( + (32, (Q(-858261, 10**6), Q(-858260, 10**6)), Q(3, 10**6), + (Q(-9, 10), Q(-4, 5))), + (33, (Q(-1873709, 10**6), Q(-1873708, 10**6)), Q(2, 10**6), + (Q(-2), Q(-9, 5)))): + center, radius = tail_enclosure(u, COEFFICIENTS, start) + require(coarse_center[0] < center < coarse_center[1], "checkpoint center") + require(radius < radius_bound, "checkpoint radius") + certify_interval(center, radius, *interval) + tail_rows.append({"start": start, "center_interval": list(map(str, coarse_center)), + "radius_less_than": str(radius_bound), + "all_same_parity_scaled_differences": list(map(str, interval))}) + require(Q(2, 3)*Q(9, 5)+Q(1, 3)*Q(4, 5) == Q(22, 15) > 1, + "even lower error") + require(Q(2, 3)*2+Q(1, 3)*Q(9, 10) == Q(49, 30) < 2, "even upper error") + require(Q(2, 3)*Q(4, 5)+Q(1, 3)*Q(9, 5) == Q(17, 15) > 1, + "odd lower error") + require(Q(2, 3)*Q(9, 10)+Q(1, 3)*2 == Q(19, 15) < 2, "odd upper error") + + # Corroboration of (3.1), separate from the uniform written proof. + fixture_count = 0 + for eigenvalue in [Q(-15), Q(0), Q(-1, 2)] + [h(j) for j in range(1, 5)]: + for x in [64, 65, 127, 128, 1024, 2**32, 2**64]: + check_uniform_fixture(x, eigenvalue) + fixture_count += 1 + + controls = [] + + def reject(label, operation): + expect_rejection(operation) + controls.append(label) + + reject("omit distance-two term", lambda: require( + Q(raw_step(list(SEED), 5, True)[-1], raw_step(list(SEED), 5, True)[1]) + == tops[5], "wrong recurrence")) + altered = list(COEFFICIENTS) + altered[-1] += Q(1, 1000) + reject("perturb fourth mode coefficient", lambda: require( + reconstruct_seed(modes, altered) == expected_seed, "wrong seed")) + reject("domain x below 64", lambda: check_uniform_fixture(63, h(4))) + reject("eigenvalue outside uniform domain", lambda: check_uniform_fixture(64, Q(-16))) + reject("understate matrix perturbation", lambda: check_uniform_fixture(64, h(4), 1)) + wrong_j = ((Q(1), Q(0)), (h(4)+Q(3, 2), Q(1))) + reject("lose involution sign", lambda: require( + matrix_product(wrong_j, wrong_j) == IDENTITY, "wrong involution")) + reject("tail product without S less than one", lambda: tail_enclosure(u, COEFFICIENTS, 5)) + odd_center, odd_radius = tail_enclosure(u, COEFFICIENTS, 33) + reject("apply even interval to odd tail", lambda: certify_interval( + odd_center, odd_radius, Q(-9, 10), Q(-4, 5))) + reject("perturb inherited limit", lambda: check_error(tops[33], 33, LIMIT+Q(1, 149175))) + constant_seed = [0, 1, 1, 1, 1] + constant_next = raw_step(constant_seed, 5) + reject("claim all nonnegative seeds decrease", lambda: require( + Q(constant_next[-1], constant_next[1]) < 1, "constant seed increases")) + + print(json.dumps({ + "status": "PASS_PROJECTION_FINITE_INFIMUM", + "claim_type": "scoped arithmetic proof with exact finite tail certificate", + "seed": SEED, + "limit_from_pr5151": str(LIMIT), + "seed_coefficients": list(map(str, COEFFICIENTS)), + "full_profile_equalities": profile_checks, + "scalar_mode_equalities": scalar_checks, + "scaled_state_equalities": matrix_checks, + "finite_monotonicity_and_error_blocks": [5, MAX_BLOCK], + "symbolic_F_remainder_identity": True, + "uniform_lemma_fixtures": fixture_count, + "tail_certificates": tail_rows, + "rejected_controls": controls, + "unrun": ["hook ranks", "physical/recursive admission", "selected cold replay", + "Lean", "independent human review"], + "new_kappa": False, + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() From c27103bc12a5c73abeccd63a74dfd106cac03593 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?= <97155365+krzysztofwojt@users.noreply.github.com> Date: Fri, 23 Oct 2026 14:10:42 +0200 Subject: [PATCH 2/2] Focus contribution on geometric rate and credit concurrent monotonicity proof --- .../PROOF.md | 20 ++++++---- .../README.md | 40 ++++++++++++------- .../RESULT.json | 2 +- .../SOURCES.json | 0 .../TASK.json | 6 +-- .../VERIFY.json | 0 .../verify.py | 4 +- 7 files changed, 43 insertions(+), 29 deletions(-) rename research/{projection-finite-infimum => projection-geometric-tail}/PROOF.md (91%) rename research/{projection-finite-infimum => projection-geometric-tail}/README.md (78%) rename research/{projection-finite-infimum => projection-geometric-tail}/RESULT.json (97%) rename research/{projection-finite-infimum => projection-geometric-tail}/SOURCES.json (100%) rename research/{projection-finite-infimum => projection-geometric-tail}/TASK.json (87%) rename research/{projection-finite-infimum => projection-geometric-tail}/VERIFY.json (100%) rename research/{projection-finite-infimum => projection-geometric-tail}/verify.py (98%) diff --git a/research/projection-finite-infimum/PROOF.md b/research/projection-geometric-tail/PROOF.md similarity index 91% rename from research/projection-finite-infimum/PROOF.md rename to research/projection-geometric-tail/PROOF.md index 391550eb17..04818eac5f 100644 --- a/research/projection-finite-infimum/PROOF.md +++ b/research/projection-geometric-tail/PROOF.md @@ -1,4 +1,4 @@ -# Strict decrease and the sharp infimum of the block-four projection recurrence +# Four exact modes and sharp geometric convergence of the projection recurrence Prepared by Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. @@ -6,8 +6,11 @@ This is a theorem about the **unstrengthened arithmetic recurrence** below. Jacob Alan Sussman (#4628) supplies its engine interpretation and seed; Maximilian Lutz (#4643) independently derived the projection counts and checked a finite prefix plus a conservative tail. Nick Petalas (#5151) proved the exact -limit. We use that credited limit theorem; our additions are strict monotonicity -at every block, the sharp infimum, and a two-sided geometric error estimate. +limit. We use that credited limit theorem. The new contribution is the exact +four-mode representation and a two-sided geometric error estimate. During this +work JoyboyBrian's #5184 independently established strict monotonicity and the +sharp infimum by a weighted-order proof; those shared conclusions are credited +corollaries here, not claimed as a newly unresolved result. The hook ranks and representation/engine hypotheses are not re-audited here. ## 1. Statement and inherited limit @@ -33,15 +36,16 @@ N_k(r,r-2) = (2^r-1)(2^(r-1)-1)2^(k-r). Omit out-of-range terms; the third coefficient is zero for r < 2. Write T_m = a_m(m)/a_m(1). No triangle/max strengthening is applied. -**Theorem.** For every integer m >= 4, T_(m+1) < T_m. Moreover, +**Theorem.** The normalized profile has the four-mode representation (2.3), and ``` -inf_(m>=4) T_m = L = 439277/149175, -2^(-m) < T_m - L < 2^(1-m) for every m >= 5. +2^(-m) < T_m - L < 2^(1-m) for every m >= 5, +L = 439277/149175. ``` -In particular the infimum is never attained, and the error has order 2^(-m). -The theorem does not assert that every nonnegative seed is monotone. +Thus the error has order 2^(-m). The proof also independently yields +T_(m+1)=4 and the unattained infimum L, as established +concurrently by #5184. It does not assert that every nonnegative seed is monotone. The equality lim T_m = L is Petalas's theorem at `e6c8e945a47dcc4a6f08974682090fc7f5e221a3`, diff --git a/research/projection-finite-infimum/README.md b/research/projection-geometric-tail/README.md similarity index 78% rename from research/projection-finite-infimum/README.md rename to research/projection-geometric-tail/README.md index e3bf41786f..3f9d51d11a 100644 --- a/research/projection-finite-infimum/README.md +++ b/research/projection-geometric-tail/README.md @@ -1,21 +1,26 @@ -# Strictly decreasing projection ratios and their exact infimum +# Four exact modes and sharp geometric convergence of projection ratios For the unstrengthened projection recurrence with block-four seed `(0,27456,48576,68320,86592)`, this package proves ``` -T_(m+1) < T_m for every m >= 4, -inf T_m = L = 439277/149175, +L = 439277/149175, 2^(-m) < T_m-L < 2^(1-m) for every m >= 5. ``` Here `T_m=a_m(m)/a_m(1)`. The exact limit L is Nick Petalas's [#5151](https://github.com/CrocSwap/integer-mult-bounds/pull/5151) theorem. -The **new results** are strict all-block monotonicity, nonattainment of the -sharp infimum, and a two-sided geometric error bound. They resolve the -original-seed monotonicity/infimum question and improve the conservative -convergence rate explicitly left open there. This is a scoped arithmetic -proof with an exact finite certificate, not a new kappa or supplier. +The **new results** are an exact four-mode representation of the entire +normalized profile and the two-sided geometric error bound. They improve the +conservative O(1/m) convergence rate explicitly left open there. This is a +scoped arithmetic proof with an exact finite certificate, not a new kappa or supplier. + +The proof also yields strict decrease for every m>=4 and the exact unattained +infimum L. JoyboyBrian's concurrent +[#5184](https://github.com/CrocSwap/integer-mult-bounds/pull/5184) already proves +those shared conclusions by a different weighted-order method. They are +credited, independently obtained corollaries here; the submission is focused +on the additional geometric rate and finite-mode representation. ## Proof and evidence @@ -49,13 +54,13 @@ disableable assertions. From the repository root, with CPython 3.12 and its standard library: ```sh -python3.12 -B scripts/research_package.py --package research/projection-finite-infimum -python3.12 -I -X dev -W error -B research/projection-finite-infimum/verify.py -python3.12 -I -O -X dev -W error -B research/projection-finite-infimum/verify.py -python3.12 -B scripts/check_research_commit.py --package research/projection-finite-infimum --check-source-history +python3.12 -B scripts/research_package.py --package research/projection-geometric-tail +python3.12 -I -X dev -W error -B research/projection-geometric-tail/verify.py +python3.12 -I -O -X dev -W error -B research/projection-geometric-tail/verify.py +python3.12 -B scripts/check_research_commit.py --package research/projection-geometric-tail --check-source-history ``` -Expected markers: `PASS_PROJECTION_FINITE_INFIMUM`, +Expected markers: `PASS_PROJECTION_GEOMETRIC_TAIL`, `PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. Direct verification takes less than a second on the author's macOS arm64 host with CPython 3.12.12; this is an observation, not a performance claim. The direct @@ -89,7 +94,12 @@ The pre-claim search covered 331 open PRs, 4,339 Discussion records, and 6,918 main-tree notes, followed by live recent-claim/PR and closed-PR term checks. The nearby same-account Gram and R437 claims and all earlier excluded topics were left alone. Search coverage excludes unpublished work and arbitrary diffs. -The final live overlap refresh is recorded in the PR and canonical thread. +The final live overlap refresh found #5184, head +`b8aa60d489ff067c5b994a54e5ebd3c2bdc09503`. Its claim was posted at 11:39:28 UTC, +between the last pre-claim live query and creation of #5169. Its proof was read +and credited before publication; no peer verifier was rerun. The scope was +narrowed in [the canonical update](https://github.com/CrocSwap/integer-mult-bounds/discussions/5169#discussioncomment-19145289) +to the additional results above. The PR records the latest coverage snapshot. The result is about this seed and this recurrence. It does not provide an elementary closed form for the mode sequences or classify every seed. The @@ -119,6 +129,6 @@ remained with the primary agent. SymPy was used for exploratory algebra only; the published certificate uses the standard library. No independent human or proof-kernel acceptance is claimed. -Credit Sussman, Lutz, Petalas, eumemic (#288), Swapnil Jain, and the retained +Credit Sussman, Lutz, Petalas, JoyboyBrian, eumemic (#288), Swapnil Jain, and the retained certificate-method/engine lineage. This new work is Apache-2.0. Frozen predecessor files, shared tooling, and the selected record remain unchanged. diff --git a/research/projection-finite-infimum/RESULT.json b/research/projection-geometric-tail/RESULT.json similarity index 97% rename from research/projection-finite-infimum/RESULT.json rename to research/projection-geometric-tail/RESULT.json index 45b8c462ca..dd16b484de 100644 --- a/research/projection-finite-infimum/RESULT.json +++ b/research/projection-geometric-tail/RESULT.json @@ -34,7 +34,7 @@ "6181/14586", "99085/239811" ], - "status": "PASS_PROJECTION_FINITE_INFIMUM", + "status": "PASS_PROJECTION_GEOMETRIC_TAIL", "symbolic_F_remainder_identity": true, "tail_certificates": [ { diff --git a/research/projection-finite-infimum/SOURCES.json b/research/projection-geometric-tail/SOURCES.json similarity index 100% rename from research/projection-finite-infimum/SOURCES.json rename to research/projection-geometric-tail/SOURCES.json diff --git a/research/projection-finite-infimum/TASK.json b/research/projection-geometric-tail/TASK.json similarity index 87% rename from research/projection-finite-infimum/TASK.json rename to research/projection-geometric-tail/TASK.json index b41abf003c..7512084e34 100644 --- a/research/projection-finite-infimum/TASK.json +++ b/research/projection-geometric-tail/TASK.json @@ -80,9 +80,9 @@ ] }, "scope_status": "changed", - "actual_scope": "Prove strict all-block decrease, sharp infimum 439277/149175, and 2^-m < T_m-L < 2^(1-m) for the unstrengthened block-four projection recurrence, using the credited exact limit of PR5151.", - "scope_change_reason": "Handoff-first override: PR5151 explicitly leaves finite-size formulas, monotonicity and the all-block infimum open. This investigates a new arithmetic implication, not another moment-root replay.", - "bottleneck_link": "Scoped side theorem for complex-engine projection lower bounds: replaces a conservative finite-tail floor by the exact infimum and a sharp-order geometric convergence bound. Hook and engine assumptions remain inherited; no supplier or kappa claim.", + "actual_scope": "Prove an exact four-mode representation and 2^-m < T_m-L < 2^(1-m) for every m>=5 in the unstrengthened block-four projection recurrence, using the credited exact limit L=439277/149175 of PR5151. Credit the concurrent monotonicity and infimum theorem of PR5184; those shared corollaries are not the new contribution.", + "scope_change_reason": "Handoff-first override: PR5151 left finite-size questions open. The final live overlap check found concurrent PR5184 proving monotonicity and the infimum, so the public claim was narrowed before publication to the additional four-mode representation and sharp-order geometric rate.", + "bottleneck_link": "Scoped side theorem for complex-engine projection lower bounds: sharp-order geometric error bounds replace the known O(1/m) rate, and a fixed four-mode representation removes the growing triangular state. Hook and engine assumptions remain inherited; no supplier or kappa claim.", "budget_minutes": 210, "stop_rule": "One-hour algebraic gate; stop or narrow if only the known limit is recovered. At most one focused result; no hook-rank recomputation, physical implementation or new kappa.", "outcome": "completed", diff --git a/research/projection-finite-infimum/VERIFY.json b/research/projection-geometric-tail/VERIFY.json similarity index 100% rename from research/projection-finite-infimum/VERIFY.json rename to research/projection-geometric-tail/VERIFY.json diff --git a/research/projection-finite-infimum/verify.py b/research/projection-geometric-tail/verify.py similarity index 98% rename from research/projection-finite-infimum/verify.py rename to research/projection-geometric-tail/verify.py index 40ae4895fc..9623420d58 100644 --- a/research/projection-finite-infimum/verify.py +++ b/research/projection-geometric-tail/verify.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""Exact certificate for the block-four projection infimum and geometric tail. +"""Exact certificate for four projection modes and a sharp geometric tail. Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0. Standard library, no network/Git/source imports, no writes, no assert statements. @@ -309,7 +309,7 @@ def reject(label, operation): Q(constant_next[-1], constant_next[1]) < 1, "constant seed increases")) print(json.dumps({ - "status": "PASS_PROJECTION_FINITE_INFIMUM", + "status": "PASS_PROJECTION_GEOMETRIC_TAIL", "claim_type": "scoped arithmetic proof with exact finite tail certificate", "seed": SEED, "limit_from_pr5151": str(LIMIT),