From e6c8e945a47dcc4a6f08974682090fc7f5e221a3 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 12:03:47 +0100 Subject: [PATCH] feat(research): prove exact Lagrangian projection limit --- research/projection-recursion-limit/PROOF.md | 225 +++++++++++++++ research/projection-recursion-limit/README.md | 122 ++++++++ .../projection-recursion-limit/RESULT.json | 14 + .../projection-recursion-limit/SOURCES.json | 24 ++ research/projection-recursion-limit/TASK.json | 120 ++++++++ .../projection-recursion-limit/VERIFY.json | 40 +++ research/projection-recursion-limit/verify.py | 263 ++++++++++++++++++ 7 files changed, 808 insertions(+) create mode 100644 research/projection-recursion-limit/PROOF.md create mode 100644 research/projection-recursion-limit/README.md create mode 100644 research/projection-recursion-limit/RESULT.json create mode 100644 research/projection-recursion-limit/SOURCES.json create mode 100644 research/projection-recursion-limit/TASK.json create mode 100644 research/projection-recursion-limit/VERIFY.json create mode 100644 research/projection-recursion-limit/verify.py diff --git a/research/projection-recursion-limit/PROOF.md b/research/projection-recursion-limit/PROOF.md new file mode 100644 index 0000000000..ec946a12a2 --- /dev/null +++ b/research/projection-recursion-limit/PROOF.md @@ -0,0 +1,225 @@ +# Exact limit of the projection recursion + +This is a theorem about an explicit arithmetic recurrence. Its interpretation +as a complex-engine lower bound inherits the representation and hook premises +of Jacob Alan Sussman #4628 and Maximilian Lutz #4643. None of those premises +is proved or certified here. + +## Statement + +Fix an integer b >= 1 and a nonnegative real profile a_b(0),...,a_b(b), +with a_b(0)=0 and a_b(1)>0. For k>b and 0<=r<=k, define + +``` +a_k(r) = sum_s N_k(r,s) a_(k-1)(s), +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). +``` + +The third entry is zero at r=0,1. The first entry is zero at r=k. +Zero entries outside the previous profile's range are omitted. At r=0 +only N_k(0,0)=4^k-1 remains. These are the cited predecessor counts. +No optional triangle/max strengthening is part of this recurrence. + +Write [b choose r]_2 for the Gaussian binomial coefficient and put + +``` +Z_b = product_(i=1)^b (2^i+1), +C_b = (2^(b+1)+1)/(2^b-1), +f(r) = a_b(r)/a_b(1), +F = max_(0<=r<=b) f(r), +T_m = a_m(m)/a_m(1). +``` + +Then the exact limit is + +``` +L_b = (C_b/2) / Z_b + * sum_(r=0)^b [b choose r]_2 2^(r(r+1)/2) f(r). +``` + +For every pair of integers b<=K=2b proves convergence. The formula is exact +for every seed profile in the stated domain, rather than a decimal estimate +of one seed's tail. It does not assert monotonicity or that L_b is an +all-m lower bound. + +For b=4 and the cited seed (0,27456,48576,68320,86592), + +``` +Z_4 = 2295, +([4 choose r]_2 2^(r(r+1)/2))_(r=0)^4 = (1,30,280,960,1024), +C_4/2 = 11/10, +L_4 = 439277/149175 = 2.9447092341209986... . +``` + +The exact rational limit and the general limit/error theorem are the new +result. The predecessor's quoted decimal 2.944709234 agrees to its displayed +precision; that agreement is not a new hook-rank verification. + +## 1. Normalize the recurrence + +Each row of N_k sums to 4^k-1. Thus P_k(r,s)=N_k(r,s)/(4^k-1) +is a stochastic reduction from block k to k-1. If X starts at distance m +at block m and follows these reductions down to b, then + +``` +a_m(m) = a_b(1) product_(k=b+1)^m (4^k-1) * E[f(X_b)]. +``` + +At r=1 only the s=1 term contributes, with coefficient + +``` +N_k(1,1) = (2^(k-1)-1)(2^(k+1)+1). +``` + +Both products telescope to give + +``` +T_m = G_(m,b) E[f(X_b)], +G_(m,b) = C_b (2^m-1)/(2^(m+1)+1), +G_(m,b) -> C_b/2, +C_b/2-G_(m,b) = 3 C_b/(2(2^(m+1)+1)). (2) +``` + +## 2. A coherent family of reference distributions + +In a binary symplectic space of dimension 2k, fix a Lagrangian L. +There are + +``` +D_k(r) = [k choose r]_2 2^(r(r+1)/2) +``` + +Lagrangians M with distance r=k-dim(L intersect M). To see this, first +choose I=L intersect M of codimension r in L. In I-perp/I, a transverse +Lagrangian to L/I is the graph of a symmetric r-by-r binary matrix over +a chosen complementary Lagrangian. There are 2^(r(r+1)/2) such matrices. + +The total number Z_k is product_(i=1)^k(2^i+1). An elementary induction +counts pairs (p,M), with 0!=p in M. There are 2^k-1 choices in each M, +and each of the 4^k-1 nonzero p belongs to Z_(k-1) Lagrangians, by +reduction in p-perp/

. Hence Z_k=(2^k+1)Z_(k-1). + +For uniform M and independently uniform nonzero p, the reduced M is +uniform among Lagrangians of p-perp/

. Indeed each symplectic map of +that quotient lifts, by extending a symplectic basis, to a map fixing p; +the lifted map permutes the original uniform M's and commutes with +reduction. The quotient action is transitive. The reduced L is fixed +conditional on p. Consequently the distance law D_k/Z_k reduces to +D_(k-1)/Z_(k-1). This also follows by substituting the three displayed +N_k coefficients into the Gaussian-binomial formula. + +Use the deficit j=k-r. Let pi_k(j)=D_k(k-j)/Z_k for 0<=j<=k. +In deficit coordinates the coherence identity is pi_k P_k=pi_(k-1). +For fixed j, + +``` +pi_k(j) = w_j * product_(i=k-j+1)^k(1-2^-i) + / product_(i=1)^k(1+2^-i), +w_0=1, w_j=1/product_(i=1)^j(2^i-1). +``` + +Since pi_k(j)<=w_j, and w_j<=3^(-(j-1)) for j>=1, dominated +convergence on this countable set proves total-variation convergence +pi_k -> pi, where pi(j)=w_j/sum_h w_h. It also proves that +sum_h w_h=product_(i=1)^infinity(1+2^-i). No infinite numerical product +is needed to evaluate L_b. + +## 3. A homogeneous comparison chain + +Put M=2^k and z=2^j. The deficit transition from j has probabilities + +``` +u_k(j) = (M^2/(2z)-3M/2+z)/(M^2-1), to j+1, +d_k(j) = (z-1+M^2-M^2/z)/(M^2-1), to j-1, +1-u_k(j)-d_k(j), to j. +``` + +At j=k the transition is deterministically to k-1; the same formulas +apply. Define the homogeneous chain Q on nonnegative integers by + +``` +u(j)=2^(-j-1), d(j)=1-2^-j, stay(j)=2^(-j-1). +``` + +Detailed balance holds because w_(j+1)/w_j=1/(2^(j+1)-1), so pi is +stationary for Q. Its expected deficit is at most 9/8: the unnormalized +first moment is at most sum_(j>=1) j/3^(j-1)=9/4 and the normalizer +is at least w_0+w_1=2. + +Q is monotone. Adjacent states can cross in an ordered coupling only +if u(j)+d(j+1)>1; here their sum equals 1. Use inverse distribution +functions driven by one uniform random number to preserve order. +Couple a chain starting at 0 below a stationary chain starting with pi. +When the upper chain first reaches 0 they coalesce. + +From j>=1 the upper chain's mean increment is +3*2^(-j-1)-1<=-1/4. Stopping at 0 and at a deterministic time n gives +E[min(tau,n)]<=4j by summing this drift and using nonnegativity of the +stopped state. Letting n increase gives E[tau|j]<=4j. Thus the coupling +time has mean at most 9/2, and Markov's inequality proves, for n>=1, + +``` +TV(delta_0 Q^n, pi) <= 9/(2n). (3) +``` + +This argument supplies recurrence and convergence directly; it invokes +no unproved mixing assumption. + +For 0<=j<=k, direct subtraction gives + +``` +u_k(j)-u(j) = (-3M/2+z+1/(2z))/(M^2-1) <= 0, +d_k(j)-d(j) = (z-1/z)/(M^2-1) >= 0. +``` + +The total variation of the three-entry rows is the maximum of these +two absolute differences. The first is <=2/M and the second <=4/(3M) +for M>=2. Extend P_k to j>k by using Q there. Therefore + +``` +sup_j TV(P_k(j,.),Q(j,.)) <= 2^(1-k). (4) +``` + +## 4. Convergence down to the fixed seed block + +Let A_(m,K)=delta_0 P_m ... P_(K+1). The starting deficit is 0. +Stochastic kernels contract total variation. Telescoping (4), with +sum_(k=K+1)^m 2^(1-k)<=2^(1-K), and (3) give + +``` +TV(A_(m,K),pi) <= 9/(2(m-K)) + 2^(1-K). +``` + +Apply the same comparison with starting distribution pi_m. Coherence +gives pi_m P_m ... P_(K+1)=pi_K, while stationarity gives +pi Q^(m-K)=pi. Since pi_m -> pi, taking m to infinity yields +TV(pi_K,pi)<=2^(1-K). Hence + +``` +TV(A_(m,K),pi_K) <= 9/(2(m-K)) + 2^(2-K). +``` + +Propagate both laws from K to b. Coherence and contraction show that +the same upper bound holds for TV(A_(m,b),pi_b). In distance coordinates +pi_b has probabilities D_b(r)/Z_b. Since 0<=f<=F, the expectation +difference is at most F times this total variation bound. Combine this +with (2) and G_(m,b)<=C_b/2 to obtain (1) and the asserted limit. + +## Limits of the conclusion + +The hook values are premises, including the two lower bounds whose stored +rank certificates #4643 leaves open. The result is unconditional as a theorem +about the stated recurrence, and conditional when interpreted as an engine +bound. It certifies no engine implementation, new paid construction, physical +cost, selected frontier, or complete multiplication theorem. The optional +triangle strengthening is outside the theorem. No infimum over finite m, +monotonicity theorem, or formal proof-kernel review is asserted. diff --git a/research/projection-recursion-limit/README.md b/research/projection-recursion-limit/README.md new file mode 100644 index 0000000000..6fe89d37f9 --- /dev/null +++ b/research/projection-recursion-limit/README.md @@ -0,0 +1,122 @@ +# Exact rational limit of the Lagrangian projection recurrence + +**Scoped mathematical proof with finite corroboration; no new kappa.** +The projection recurrence of Jacob Alan Sussman [#4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628) +and Maximilian Lutz [#4643](https://github.com/CrocSwap/integer-mult-bounds/pull/4643) +has the exact asymptotic ratio + +``` +lim_(m->infinity) a_m(m)/a_m(1) = 439277/149175. +``` + +The displayed decimal is 2.9447092341209986... . The new result identifies +this limit exactly, proves convergence with an explicit error bound, and +gives the limit for every nonnegative seed profile at any fixed seed block. +It extends the predecessors' numerical tail description. It does not +re-check their hook ranks, projection geometry or engine implementation. + +## The result + +[PROOF.md](PROOF.md) defines the recurrence and proves that a seed profile +`a_b(0)=0`, `a_b(1)>0`, `a_b(r)>=0` has limit + +``` +(2^(b+1)+1) / (2(2^b-1) product_(i=1)^b(2^i+1)) +* sum_(r=0)^b [b choose r]_2 2^(r(r+1)/2) a_b(r)/a_b(1). +``` + +Here `[b choose r]_2` is the Gaussian binomial coefficient. For the cited +block-four seed `(0,27456,48576,68320,86592)`, the distance weights are +`(1,30,280,960,1024)/2295` and the remaining factor is `11/10`. +The result is a finite rational expression, despite the infinite products +and stationary laws that appear in its proof. + +The proof normalizes the integer recurrence into a Markov reduction, +uses coherent uniform-Lagrangian distance laws, and compares the deficit +with a homogeneous birth-and-death chain. A monotone coupling has expected +coalescence time at most `9/2`. A summable row-error bound proves convergence +to the coherent seed-block law. Equation (1) of PROOF.md gives the explicit +all-m error estimate. The proof invokes no numerical mixing assumption. + +This theorem is unconditional for the displayed arithmetic recurrence. +Its engine-game interpretation is conditional on the predecessor's hook +profile and representation argument. In particular, the two stored-rank +certificate obligations identified in #4643 remain unresolved here. +The result does not assert monotonicity, a finite-m infimum, the optional +triangle/max strengthened recurrence, physical costs, native admission, +a new supplier, or a complete multiplication theorem. The selected +frontier is unchanged. Independent human and formal proof-kernel review +are unclaimed. + +## Reproduce + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projection-recursion-limit +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -X dev -W error -B research/projection-recursion-limit/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -X dev -W error -B research/projection-recursion-limit/verify.py +``` + +Another CPython 3.12 interpreter may replace the absolute local path. +Success markers are `PASS_PROJECTION_RECURSION_LIMIT` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. Both registered commands run with a +120-second timeout. Default verification is read-only and writes no receipt. +Explicit `--emit` prints newly generated hash-bound evidence to standard +output; [RESULT.json](RESULT.json) was generated through that command. + +The standalone checker imports no predecessor code. It checks 3,320 new +kernel-coordinate and row-error identities, 63 coherence reductions, +80 detailed-balance/monotonicity indices, 73 seed-profile limit enclosures, +54 enclosures for six other seed blocks, and 38 independent comparisons +between probability-law propagation and the integer recurrence. Six +controls distinguish wrong normalization, a wrong exact limit, a changed +seed, a corrupt transition and a wrong coherent law. These finite checks +corroborate the written proof; they do not replace its infinite-limit +argument. The generated receipt binds the verifier, proof and cited source +README by SHA256. The registered runner also authenticates source metadata. + +New code is bounded to block/index 100 and uses explicit exceptions under +normal and optimized Python. Each function is below 60 lines. Python's +managed integers and fractions allocate during execution, a deliberate +Power of Ten deviation; the finite index limits bound live collections +and integer sizes. No recursion, dynamic code execution, external solver, +network call, subprocess or background process occurs in the verifier. +Warning-strict development-mode replay supplies interpreter diagnostics; +no static type checker or formal kernel is claimed. + +## Sources and overlap + +Scientific base is `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority +revision 7. [SOURCES.json](SOURCES.json) pins the predecessor README, +task catalogue and selected record. Only the predecessor README is a live +input; its source bytes remain unchanged. Arbitrary code diffs and unpublished +work are outside the overlap search. The sparse local-note inventory is +incomplete and was supplemented with targeted main-tree and merged-PR searches. +The local card changes from independent ledger checking to this original +closed-form recurrence theorem; it is a complex small-block side result. + +## Open next questions + +1. Does this recurrence admit a finite-m closed form, or a faster convergence + rate? The present proof gives an explicit error estimate and an exact limit. + Begin with the coherent-law comparison rather than recomputing hook ranks. +2. Which seed profiles make the top ratios monotone, and when is their + infimum the limit? A limit alone does not settle these questions. Start by + examining adjacent-block differences as linear functionals of the seed. + +Neither question requires another physical construction round. The separate +engine, hook-rank, native, precision, hosting and complete-cost obligations +remain with their existing investigations. Structured questions are in +[TASK.json](TASK.json). + +## Credit + +This result was produced by Nick Petalas. Jacob Alan Sussman #4628 supplies +the projection recurrence and block-four hook profile. Maximilian Lutz #4643 +supplies its public count formulas, coherent geometry context and prior tail +analysis, including the explicit unresolved rank obligations. Eumemic #288 +and Swapnil Jain retain the underlying certificate-method credit. Classical +Gaussian-binomial counting, symplectic reduction, birth-and-death chains and +coupling arguments retain their mathematical authorship. No literature-priority +claim is made for those methods. New work is Apache-2.0. diff --git a/research/projection-recursion-limit/RESULT.json b/research/projection-recursion-limit/RESULT.json new file mode 100644 index 0000000000..c39f077a5a --- /dev/null +++ b/research/projection-recursion-limit/RESULT.json @@ -0,0 +1,14 @@ +{ + "claim_type": "scoped recurrence proof with finite corroboration", + "coherence_transitions": 63, + "failure_controls": 6, + "general_seed_enclosures": 54, + "kernel_rows": 3320, + "limit": "439277/149175", + "markov_raw_comparisons": 38, + "proof_sha256": "83843a1460d8d5ccca4c312268e3a138f5dddc8197986ba63955392a3da0da33", + "seed_limit_enclosures": 73, + "source_sha256": "59204f11aa3aae59df44fc69228cd017660139587b2dc18ece1999a98d097996", + "stationary_indices": 80, + "verifier_sha256": "5014e6aef2eb9fb3aa77d460a4a4946bbad3dbc470f4bccc28de6b905920f505" +} diff --git a/research/projection-recursion-limit/SOURCES.json b/research/projection-recursion-limit/SOURCES.json new file mode 100644 index 0000000000..051924d15d --- /dev/null +++ b/research/projection-recursion-limit/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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": "input", + "git_blob": "1d8c9f7b1b96cd098a9a00a90022143bbced8b64", + "sha256": "59204f11aa3aae59df44fc69228cd017660139587b2dc18ece1999a98d097996" + } + ] +} diff --git a/research/projection-recursion-limit/TASK.json b/research/projection-recursion-limit/TASK.json new file mode 100644 index 0000000000..3b7a3032f7 --- /dev/null +++ b/research/projection-recursion-limit/TASK.json @@ -0,0 +1,120 @@ +{ + "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 the exact asymptotic ratio of the stated Lagrangian projection recurrence for every fixed nonnegative seed profile, with an explicit convergence bound; apply it to the cited block-four seed to obtain 439277/149175.", + "scope_change_reason": "The card requests independent paid-ledger coverage. This contribution instead gives an original closed-form limit theorem for the complex small-block projection recurrence of Sussman #4628 and Lutz #4643; their inputs are cited premises and are not replayed as the deliverable.", + "bottleneck_link": "Scoped complex small-block side result: it identifies exactly the asymptotic output of this lower-bound recurrence and preserves its unresolved hook and engine premises. It changes no selected supplier or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved exact limit and convergence theorem; do not extend into hook-rank certification, finite-m optimization or a physical construction.", + "outcome": "completed", + "evidence": "PROOF.md proves the general rational limit and equation (1) error bound. verify.py checks new kernel/coherence/normalization identities, independent integer/probability propagation, exact limit enclosures and six controls. RESULT.json is generated and hash-bound.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the finite-m ratio be expressed in closed form, or can the convergence rate be improved?", + "why_it_matters": "The exact limit now has a rational formula, while the explicit coupling estimate is conservative.", + "first_step": "Study the coherent Lagrangian distance laws and the finite product of deficit kernels for a fixed seed.", + "blocked_by": "No blocker identified; a new finite-m identity is needed." + }, + { + "question": "Which nonnegative seed profiles make the top ratios monotone and their infimum equal to the limit?", + "why_it_matters": "The proved limit alone does not supply a sharp all-m lower bound.", + "first_step": "Express adjacent-block differences as linear functionals of the seed and identify their sign cone.", + "blocked_by": "No monotonicity or finite-m infimum theorem is supplied." + } + ], + "claim_type": "scoped arithmetic recurrence proof with finite corroboration", + "local_environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144283", + "publication_checkpoint": { + "canonical_main": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "utc": "2026-10-23T11:03:46.827339+00:00", + "guidance_and_source_changes": "None since scientific base.", + "overlap": "Fresh main exact-rational/formula searches, merged PR searches, open PRs and recent #1166 comments found only the cited predecessors and this claim. No novelty guarantee for unpublished work." + } +} diff --git a/research/projection-recursion-limit/VERIFY.json b/research/projection-recursion-limit/VERIFY.json new file mode 100644 index 0000000000..3052c8aa47 --- /dev/null +++ b/research/projection-recursion-limit/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/projection-recursion-check/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact general limit normalization, coherent laws, transition approximation, rational enclosures and six semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete exact checks with interpreter assertions disabled." + } + ] +} diff --git a/research/projection-recursion-limit/verify.py b/research/projection-recursion-limit/verify.py new file mode 100644 index 0000000000..a6c1c26220 --- /dev/null +++ b/research/projection-recursion-limit/verify.py @@ -0,0 +1,263 @@ +#!/usr/bin/env python3 +"""Exact corroboration for the scoped projection-recursion limit theorem.""" + +import argparse +from fractions import Fraction as Q +import hashlib +import json +from math import prod +from pathlib import Path +import sys + +BASE = (0, 27456, 48576, 68320, 86592) +LIMIT = Q(439277, 149175) +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def gaussian(k, r): + require(0 <= r <= k <= 100, "Gaussian-binomial domain") + numerator = prod(2 ** (k - i) - 1 for i in range(r)) + denominator = prod(2 ** (r - i) - 1 for i in range(r)) + value, remainder = divmod(numerator, denominator) + require(remainder == 0, "nonintegral Gaussian binomial") + return value + + +def reference_law(k): + """Distance distribution; deficit order is its reversal.""" + require(1 <= k <= 100, "reference-law domain") + total = prod(2 ** i + 1 for i in range(1, k + 1)) + values = tuple(Q(gaussian(k, r) * 2 ** (r * (r + 1) // 2), total) + for r in range(k + 1)) + require(sum(values) == 1, "reference law does not normalize") + return values + + +def counts(k, r): + """Cited integer recurrence, independently encoded in distance order.""" + require(1 <= k <= 100 and 0 <= r <= k, "count domain") + same = 2 ** (k - r) - 1 + 4 ** k - 2 ** (k + r) + one = 2 * (2 ** k - 2 ** (k - r)) + (2 ** r - 1) * 2 ** (k - 1) + two = ((2 ** r - 1) * (2 ** (r - 1) - 1) * 2 ** (k - r) + if r >= 2 else 0) + result = {r: same, r - 1: one, r - 2: two} + require(all(v >= 0 for v in result.values()), "negative count") + require(sum(result.values()) == 4 ** k - 1, "incorrect row sum") + return {s: v for s, v in result.items() if v} + + +def deficit_row(k, j): + """New comparison-chain formulas, separate from counts().""" + require(0 <= j <= k <= 100 and k >= 1, "deficit domain") + size, z = 2 ** k, 2 ** j + up = Q(size * size, 2 * z) - Q(3 * size, 2) + z + up /= size * size - 1 + down = Q(z - 1 + size * size - size * size // z, size * size - 1) + stay = 1 - up - down + require(min(up, stay, down) >= 0, "negative transition") + return up, stay, down + + +def homogeneous(j): + require(0 <= j <= 100, "homogeneous domain") + return Q(1, 2 ** (j + 1)), Q(1, 2 ** (j + 1)), 1 - Q(1, 2 ** j) + + +def multiplier(m, b): + return Q((2 ** (b + 1) + 1) * (2 ** m - 1), + (2 ** b - 1) * (2 ** (m + 1) + 1)) + + +def limit_of(seed): + b = len(seed) - 1 + law = reference_law(b) + scale = Q(2 ** (b + 1) + 1, 2 * (2 ** b - 1)) + return scale * sum(law[r] * Q(seed[r], seed[1]) for r in range(b + 1)) + + +def error_bound(m, b, maximum): + k = m // 2 + require(b <= k < m, "error-bound split domain") + c = Q(2 ** (b + 1) + 1, 2 ** b - 1) + variation = Q(9, 2 * (m - k)) + Q(2) ** (2 - k) + return maximum * (c * variation / 2 + 3 * c / (2 * (2 ** (m + 1) + 1))) + + +def row_matches_counts(k, j, row): + expected = counts(k, k - j) + return all(probability == Q(expected.get(k - 1 - j - offset, 0), 4 ** k - 1) + for offset, probability in zip((1, 0, -1), row)) + + +def check_kernels(): + rows = 0 + for k in range(1, 81): + for j in range(k + 1): + row = deficit_row(k, j) + require(row_matches_counts(k, j, row), "coordinate mismatch") + other = homogeneous(j) + variation = sum(abs(x - y) for x, y in zip(row, other)) / 2 + require(variation <= Q(2, 2 ** k), "kernel-error bound") + rows += 1 + return rows + + +def check_coherence(): + transitions = 0 + for k in range(2, 65): + initial = reference_law(k)[::-1] + reduced = [Q(0)] * k + for j, probability in enumerate(initial): + for offset, part in zip((1, 0, -1), deficit_row(k, j)): + if part: + reduced[j + offset] += probability * part + require(tuple(reduced) == reference_law(k - 1)[::-1], "coherence") + transitions += 1 + return transitions + + +def check_stationary(): + weight = Q(1) + moment = Q(0) + normalizer = Q(1) + for j in range(80): + next_weight = weight / (2 ** (j + 1) - 1) + require(weight * homogeneous(j)[0] == next_weight * homogeneous(j + 1)[2], + "detailed balance") + require(homogeneous(j)[0] + homogeneous(j + 1)[2] == 1, "monotonicity") + if j >= 1: + require(homogeneous(j)[0] - homogeneous(j)[2] <= -Q(1, 4), "drift") + moment += (j + 1) * next_weight + normalizer += next_weight + weight = next_weight + require(moment <= Q(9, 4) and normalizer >= 2, "mean bound") + return 80 + + +def evolve(seed, end): + """Raw integer recurrence, with the new normalization checked at each step.""" + b = len(seed) - 1 + require(1 <= b < end <= 100 and seed[0] == 0 and seed[1] > 0, "seed domain") + profile = tuple(seed) + cap = seed[1] + total = seed[1] + tops = {b: Q(seed[-1], seed[1])} + for k in range(b + 1, end + 1): + profile = tuple(sum(count * profile[s] for s, count in counts(k, r).items()) + for r in range(k + 1)) + cap *= (2 ** (k - 1) - 1) * (2 ** (k + 1) + 1) + total *= 4 ** k - 1 + require(profile[1] == cap, "cap product") + require(Q(total, cap) == multiplier(k, b), "telescoping normalization") + tops[k] = Q(profile[-1], cap) + return tops + + +def check_markov(seed, end): + """Propagate full probability laws instead of the raw seed recurrence.""" + b = len(seed) - 1 + raw = evolve(seed, end) + for m in range(b + 1, end + 1): + probabilities = [Q(1)] + [Q(0)] * m + for k in range(m, b, -1): + reduced = [Q(0)] * k + for j, probability in enumerate(probabilities): + for offset, part in zip((1, 0, -1), deficit_row(k, j)): + if part: + reduced[j + offset] += probability * part + probabilities = reduced + expected = sum(p * Q(seed[b - j], seed[1]) + for j, p in enumerate(probabilities)) + require(multiplier(m, b) * expected == raw[m], "Markov/raw mismatch") + return end - b + + +def check_controls(): + """Reject concrete wrong formulas through the same exact identities.""" + require(limit_of(BASE) != Q(439278, 149175), "wrong-limit control") + changed = list(BASE) + changed[2] += 1 + require(limit_of(changed) != LIMIT, "seed-sensitivity control") + require(multiplier(5, 4) != Q(4 ** 5 - 1, (2 ** 4 - 1) * (2 ** 6 + 1) + 1), + "wrong-cap control") + weights = reference_law(4) + require(sum(weights[r] * Q(BASE[r], BASE[1]) for r in range(5)) != LIMIT, + "missing-normalization control") + row = list(deficit_row(5, 0)) + row[0] += Q(1, 100) + row[1] -= Q(1, 100) + require(not row_matches_counts(5, 0, row), "transition-corruption control") + wrong = list(reference_law(5)[::-1]) + wrong[0], wrong[1] = wrong[1], wrong[0] + reduced = [Q(0)] * 5 + for j, probability in enumerate(wrong): + for offset, part in zip((1, 0, -1), deficit_row(5, j)): + if part: + reduced[j + offset] += probability * part + require(tuple(reduced) != reference_law(4)[::-1], "wrong-law control") + return 6 + + +def evidence(): + source = "research/projection-recursion-check/README.md" + source_hash = hashlib.sha256((ROOT / source).read_bytes()).hexdigest() + pins = json.loads((PACKAGE / "SOURCES.json").read_text()) + pin = next(row for row in pins["files"] if row["path"] == source) + require(source_hash == pin["sha256"], "source hash mismatch") + require(limit_of(BASE) == LIMIT, "exact limit identity") + kernels = check_kernels() + coherence = check_coherence() + stationary = check_stationary() + tops = evolve(BASE, 80) + maximum = Q(41, 13) + bounded = 0 + for m in range(8, 81): + require(abs(tops[m] - LIMIT) <= error_bound(m, 4, maximum), "limit enclosure") + bounded += 1 + markov = check_markov(BASE, 18) + general = 0 + for b in range(1, 7): + seed = tuple([0] + [r * r + 3 for r in range(1, b + 1)]) + markov += check_markov(seed, b + 4) + values = evolve(seed, 2 * b + 8) + for m in range(2 * b, 2 * b + 9): + if m > b: + require(abs(values[m] - limit_of(seed)) <= + error_bound(m, b, Q(max(seed), seed[1])), "general-seed enclosure") + general += 1 + return {"claim_type": "scoped recurrence proof with finite corroboration", + "limit": str(LIMIT), "kernel_rows": kernels, + "coherence_transitions": coherence, "stationary_indices": stationary, + "seed_limit_enclosures": bounded, "general_seed_enclosures": general, + "markov_raw_comparisons": markov, "failure_controls": check_controls(), + "source_sha256": source_hash, + "verifier_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(), + "proof_sha256": hashlib.sha256((PACKAGE / "PROOF.md").read_bytes()).hexdigest()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print generated evidence instead of comparing it") + args = parser.parse_args() + result = evidence() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "evidence differs from generated RESULT.json") + print("PASS_PROJECTION_RECURSION_LIMIT", json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, StopIteration) as error: + print(f"FAIL_PROJECTION_RECURSION_LIMIT: {error}", file=sys.stderr) + raise SystemExit(1) from error