diff --git a/research/projection-parity-constants/PROOF.md b/research/projection-parity-constants/PROOF.md new file mode 100644 index 0000000000..3fe609ac4d --- /dev/null +++ b/research/projection-parity-constants/PROOF.md @@ -0,0 +1,378 @@ +# Exact parity constants for the projection recurrence + +Status: a proposed scoped mathematical solution with exact finite corroboration. +Prepared with OpenAI Codex assistance for this task, 2026-10-24 (Asia/Shanghai). +New text and code: Apache-2.0. No claim of prior literature priority. + +## 1. Question, sources, and result + +The source is CrocSwap/integer-mult-bounds at +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. +Krzysztof Wojt's PR #5193, `research/projection-geometric-tail`, proves +the order of convergence and explicitly leaves exact leading parity constants +and elementary/q-series expressions for the modes open. This note solves +those two scoped questions. It does not classify monotone seeds. + +At block four start with + +\[ +a_4=(0,27456,48576,68320,86592). +\] + +For k >= 5, use the unstrengthened recurrence + +\[ +a_k(r)=\sum_s N_k(r,s)a_{k-1}(s), +\] + +where the only possibly nonzero entries are + +\[ +\begin{aligned} +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}. +\end{aligned} +\] + +The last entry is zero when r < 2; omit indices outside the old profile. +Set T_m=a_m(m)/a_m(1). Let + +\[ +\mathcal K=\prod_{i=1}^{\infty} +\left(\frac{1-2^{-i}}{1+2^{-i}}\right)^2>0. +\] + +**Theorem.** As integer m tends to infinity, + +\[ +\boxed{ +T_m=\frac{439277}{149175} ++2^{-m}\left(\frac{815083}{596700} ++(-1)^m\frac{323}{28}\mathcal K\right) ++O(4^{-m}). +} +\tag{1} +\] + +Consequently the exact even and odd scaled limits are respectively + +\[ +\frac{815083}{596700}+\frac{323}{28}\mathcal K +=1.535225897075989\ldots, +\] +\[ +\frac{815083}{596700}-\frac{323}{28}\mathcal K +=1.196743266657880\ldots. +\] + +The full scaled sequence has no limit, since K > 0. The known limit +439277/149175 is recovered, not claimed as new. Exact coefficient extraction +from (7) below also gives a nonrecursive q-series expression for every mode +and hence for every finite T_m. + +## 2. The credited four-mode reduction + +Here is a self-contained verification of the reduction from #5193, which is +credited to that work. Define + +\[ +\begin{aligned} +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}. +\end{aligned} +\] + +Let e_j(r)=0 for rj put + +\[ +(h_j-h_r)e_j(r)=B_re_j(r-1)+C_re_j(r-2). +\tag{2} +\] + +Because h_r strictly decreases, this determines e_j. With + +\[ +d_k=(2^{k-1}-1)(2^{k+1}+1), +\] + +the raw row operator is d_k I + 2^k H, where H is the lower-banded operator +with coefficients h_r,B_r,C_r. Thus H e_j=h_j e_j. At the new endpoint +r=k the raw diagonal coefficient is zero, so no undefined old value is needed. +Solving the unit triangular seed system gives + +\[ +(c_1,c_2,c_3,c_4)= +\left(1,\frac{17}{39},\frac{6181}{14586},\frac{99085}{239811}\right). +\] + +Define + +\[ +p_{m,j}=\prod_{k=5}^{m} +\frac{(2^{k-j}-1)(2^{k+j}+1)}{d_k}. +\] + +The seed equations and induction with H give, for 0 <= r <= m, + +\[ +\frac{a_m(r)}{a_m(1)}=\sum_{j=1}^4 c_jp_{m,j}e_j(r). +\tag{3} +\] + +## 3. A new q-series expression for each eigenmode + +Fix j >= 1, and write Q=1/2 and s=2^j. Use the convention + +\[ +(z;Q)_n=\prod_{i=0}^{n-1}(1-zQ^i),\qquad (z;Q)_0=1. +\] + +For n >= 0 define v_n by + +\[ +e_j(j+n)=\frac{(Q^{n+1};Q)_j}{(Q;Q)_j}v_n. +\tag{4} +\] + +Thus v_0=1. To check the substitution, put y=2^r. Equation (2) becomes + +\[ +2(y-s)(sy+1)e_j(r) +=s(y-1)(y+4)e_j(r-1)+s(y-1)(y-2)e_j(r-2). +\] + +The ratio of the prefactors in (4) at consecutive r is +(y-1)/(y-s). Cancellation therefore gives, for n >= 1, + +\[ +2(1+s^{-2}Q^n)v_n +=(1+4s^{-1}Q^n)v_{n-1}+(1-2Q^n)v_{n-2}. +\tag{5} +\] + +At n=1 the last coefficient is zero, and we set v_{-1}=0. + +Let V_j(z)=sum_{n>=0} v_n z^n near zero. Multiplying (5) by z^n +and summing gives + +\[ +(1-z)(2+z)V_j(z)+\frac{(z-2/s)^2}{2}V_j(z/2) +=2(1+s^{-2}). +\tag{6} +\] + +Iterating this functional equation yields the explicit expression + +\[ +\boxed{ +V_j(z)=(1+s^{-2})\sum_{\ell=0}^{\infty} +\frac{(-s^{-2})^\ell(sz/2;Q)_\ell^2} +{(z;Q)_{\ell+1}(-z/2;Q)_{\ell+1}}. +} +\tag{7} +\] + +At z=0 the geometric series gives V_j(0)=1. Near zero the series is +absolutely convergent and satisfies (6); comparing coefficients uniquely +recovers (5). This also establishes that it is the generating function. + +More generally, (7) converges locally uniformly away from +z=1,2,4,... and z=-2,-4,-8,... . On any such compact set its finite products +are uniformly bounded and its denominator products are bounded away from zero, +while s^{-2ell} decays geometrically. Removing the one vanishing factor at +any listed point makes the series locally uniformly convergent there too. +Hence V_j is meromorphic with at most simple poles at these points. + +## 4. Three explicit poles determine the leading terms + +Define the pole coefficients + +\[ +A_j=\lim_{z\to1}(1-z)V_j(z),\quad +D_j=\lim_{z\to2}(1-z/2)V_j(z),\quad +E_j^-=\lim_{z\to-2}(1+z/2)V_j(z). +\] + +We use the classical q-Gauss identity (NIST DLMF 17.6.1): + +\[ +{}_2\phi_1(a,b;c;Q,c/(ab)) +=\frac{(c/a;Q)_\infty(c/b;Q)_\infty} +{(c;Q)_\infty(c/(ab);Q)_\infty},\qquad |c/(ab)|<1. +\tag{8} +\] + +Here the basic hypergeometric series includes the denominator (Q;Q)_ell. +All denominator parameters below avoid its forbidden nonnegative powers +Q^{-n}, and both arguments have absolute value s^{-2}<1. + +At z=1 equation (7) gives + +\[ +A_j=\frac{1+s^{-2}}{1+Q} +{}_2\phi_1(s/2,s/2;-Q^2;Q,-s^{-2}) +=\frac{(-Q;Q)_{2j}}{(-Q;Q)_j^2}. +\tag{9} +\] + +All terms with ell >= j vanish because s/2=Q^{1-j}; the last potentially +nonzero term is ell=j-1. +For example A_1=5/6. The final equality follows by (8) and cancellation +of the shifted infinite products; it can also use terminating q-Chu-Vandermonde. + +Taking the pole at z=2 in (6), where V_j(z/2) contributes A_j, gives + +\[ +D_j=\frac{(1-s^{-1})^2}{2}A_j. +\tag{10} +\] + +At z=-2 equation (7) instead gives + +\[ +\begin{aligned} +E_j^-&=\frac{1+s^{-2}}3 +{}_2\phi_1(-s,-s;-1;Q,-s^{-2})\\ +&=\frac{1+s^{-2}}3 +\frac{(Q^j;Q)_\infty^2}{(-1;Q)_\infty(-Q^{2j};Q)_\infty}\\ +&=\frac{(-Q;Q)_{2j}}{6(Q;Q)_{j-1}^2}\mathcal K. +\end{aligned} +\tag{11} +\] + +The last equality uses (-1;Q)_infty=2(-Q;Q)_infty and +K=(Q;Q)_infty^2/(-Q;Q)_infty^2. + +The meromorphic description proves the coefficient asymptotic + +\[ +v_n=A_j+D_j2^{-n}+E_j^-(-2)^{-n}+O(4^{-n}). +\tag{12} +\] + +For completeness this is not an unproved transfer heuristic: subtract the +simple-pole parts at 1, +/-2, and +/-4. The remainder is analytic on |z|<8, +so Cauchy's coefficient estimate on |z|=5 is O(5^{-n}). The two subtracted +parts at +/-4 have coefficients O(4^{-n}). Their constants need not be +computed to obtain (12). All statements here are for fixed j. + +## 5. Returning to the physical block index + +Define the rational constants + +\[ +F_j=\frac{(-Q;Q)_{2j}}{(Q;Q)_j(-Q;Q)_j^2},\qquad +G_j=\frac{(-Q;Q)_{2j}}{6(Q;Q)_{j-1}^2(Q;Q)_j}. +\] + +Since n=m-j, (4) and (12), including the first-order change in the +finite product in (4), yield + +\[ +e_j(m)=F_j\left(1-\frac{s-s^{-1}}2\,2^{-m}\right) ++(-1)^m(-1)^j sG_j\mathcal K\,2^{-m}+O(4^{-m}). +\tag{13} +\] + +For 1 <= j <= 4 the mode product has the rational limit + +\[ +P_j=\frac{\prod_{i=5-j}^{3}(1-Q^i)} +{\prod_{i=6}^{4+j}(1+Q^i)}, +\tag{14} +\] + +with empty products equal to 1. In fact its exact finite formula is + +\[ +p_{m,j}=P_j +\frac{\prod_{i=m+2}^{m+j}(1+Q^i)} +{\prod_{i=m-j+1}^{m-1}(1-Q^i)}. +\tag{15} +\] + +Thus, by expansion of these finitely many factors, + +\[ +p_{m,j}=P_j(1-h_j2^{-m}+O(4^{-m})). +\tag{16} +\] + +Multiplication with (13) gives + +\[ +p_{m,j}e_j(m)=P_jF_j ++2^{-m}\left[P_jF_j\frac{s-s^{-1}-3}{2} ++(-1)^mP_j(-1)^j sG_j\mathcal K\right]+O(4^{-m}). +\tag{17} +\] + +The three exact sums from (3) are + +\[ +\sum_j c_jP_jF_j=\frac{439277}{149175}, +\] +\[ +\sum_j c_jP_jF_j\frac{2^j-2^{-j}-3}{2} +=\frac{815083}{596700}, +\] +\[ +\sum_j c_jP_j(-1)^j2^jG_j=\frac{323}{28}. +\] + +They prove (1). The accompanying exact checker reconstructs these sums. + +## 6. Exact numerical enclosures and verification boundaries + +Let K_N be the product defining K truncated after N. For 0 <= x < 1, + +\[ +1-\left(\frac{1-x}{1+x}\right)^2=\frac{4x}{(1+x)^2}\le4x. +\] + +Applying product(1-d_i) >= 1-sum d_i to finite tails and then taking +limits proves, for N >= 3, + +\[ +K_N(1-2^{2-N})\le\mathcal K\le K_N. +\tag{18} +\] + +This both proves positivity and provides rational certified enclosures for +the two constants. The verifier uses N=80, an original integer recurrence, +a separately implemented mode recurrence, the rational identities above, +and rejection controls. Those bounded checks corroborate, rather than replace, +the universal analytic proof and the classical q-Gauss identity. + +## 7. Credit, scope, and remaining questions + +- Jacob Alan Sussman #4628: recurrence, seed, and proposed engine interpretation. +- Maximilian Lutz #4643: independent projection counts and recurrence audit. +- Nick Petalas #5151: exact rational limiting value and general seed theorem. +- JoyboyBrian #5184: strict finite-block descent and unattained infimum. +- Krzysztof Wojt #5193: fixed triangular operator, four-mode representation, + and sharp geometric order; these are explicit inputs and credited here. +- Eumemic #288, Swapnil Jain, and the retained certificate/engine lineage + retain their original credit. Q-Gauss summation is classical, not new here. + +Sources: + +- https://github.com/CrocSwap/integer-mult-bounds/pull/5193 +- https://github.com/CrocSwap/integer-mult-bounds/tree/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/projection-geometric-tail +- https://github.com/CrocSwap/integer-mult-bounds/pull/5151 +- https://dlmf.nist.gov/17.6.E1 +- https://dlmf.nist.gov/17.6.E2 + +This is an arithmetic theorem about the specified recurrence. The inherited +hook-rank certificates, engine interpretation, physical caller, dirty-state +restoration, complete costs, and multiplication theorem are not established +by it. No new kappa or selected-frontier change is claimed. No human review +or proof-kernel verification is claimed. Public novelty is limited to the +reviewed source snapshot and targeted live overlap search; unpublished work +and every historical discussion reply were not exhaustively inspected. + +Open next questions: characterize monotone seed profiles; determine whether +the q-series expression can be reduced further for finite m; resolve the +independent inherited hook-rank obligations. These are separate tasks. diff --git a/research/projection-parity-constants/README.md b/research/projection-parity-constants/README.md new file mode 100644 index 0000000000..e504585f22 --- /dev/null +++ b/research/projection-parity-constants/README.md @@ -0,0 +1,122 @@ +# Exact parity constants and q-series for the projection recurrence + +This package answers **Open next questions, item 2** in Krzysztof Wojt's +[#5193](https://github.com/CrocSwap/integer-mult-bounds/pull/5193): an explicit +q-series for every eigenmode and exact parity-sensitive leading error constants. +For the unstrengthened projection recurrence with seed +`a_4=(0,27456,48576,68320,86592)` and `T_m=a_m(m)/a_m(1)`, it proves + +\[ +T_m=\frac{439277}{149175} ++2^{-m}\left(\frac{815083}{596700} ++(-1)^m\frac{323}{28}\mathcal K\right)+O(4^{-m}), +\qquad +\mathcal K=\prod_{i=1}^{\infty} +\left(\frac{1-2^{-i}}{1+2^{-i}}\right)^2>0. +\] + +The even and odd limits of `2^m(T_m-439277/149175)` are, respectively, +`1.535225897075989125...` and `1.196743266657880490...`. The complete scaled +sequence therefore has no limit. The rational limit itself is Nick Petalas's +[#5151](https://github.com/CrocSwap/integer-mult-bounds/pull/5151) result. + +## Proof and evidence + +[PROOF.md](PROOF.md) gives the recurrence and a self-contained derivation. +Starting with #5193's credited four-mode reduction, a change of variables gives +a dilation equation for each mode's generating function. Its explicit q-series, +classical q-Gauss summation ([NIST DLMF 17.6.1](https://dlmf.nist.gov/17.6.E1)), +and simple poles at 1 and +/-2 give the constants. Subtracting the pole parts +at +/-4 as well justifies the `O(4^-m)` remainder by Cauchy's estimate. + +[verify.py](verify.py) uses only the Python standard library and exact rational +arithmetic for the mathematical checks. [RESULT.json](RESULT.json) records: + +- 2,691 whole-profile equalities against a separately implemented raw recurrence; +- 276 finite-product identities and 520 eigenmode transformations; +- 32 rigorous generating-series enclosure comparisons and 16 residue checks; +- six rejected perturbations of the seed, subdiagonal, raw recurrence seed, + eigenvalue, parity sign, or residue factor. + +These finite checks corroborate the proof; series-interval overlap and finite +asymptotic samples do not themselves prove the universal analytic identities. +The q-Gauss identity is a cited classical mathematical input, not a network or +runtime dependency. The script reads its own source and `PROOF.md` only to +produce receipt hashes; it writes no files and imports no predecessor code. + +[REVIEW.md](REVIEW.md) records a separate Codex agent's mathematical and code +review and binds it to exact hashes. It also records an independently written +raw recurrence check through block 100. This is AI review, not human review or +proof-kernel verification. + +## Reproduce + +From the repository root, with Python 3.12 and its standard library: + +```sh +python3 -B scripts/research_package.py --package research/projection-parity-constants +python3 -I -X dev -W error -B research/projection-parity-constants/verify.py +python3 -I -O -X dev -W error -B research/projection-parity-constants/verify.py +python3 -B scripts/check_research_commit.py --package research/projection-parity-constants --check-source-history +``` + +Expected markers are `PASS_PROJECTION_PARITY_CONSTANTS`, +`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. +The retained receipt was produced by CPython 3.12.14; its Python-version field +will reflect the interpreter used. Normal and optimized runs have identical +output on that interpreter. The direct verifier also works in a Git-free +package export. The registered metadata runner needs Git history to check the +provenance pins. + +## Sources, scope and overlap + +Publication base: `1ec1119972c9aefe42525172d07b332fcff81cb4`, priority revision 7. +The proof and independent review were prepared at the earlier source snapshot +`ff3cc58e370d0f678e529246f8c73e8094e18fcf` and are preserved byte-for-byte. +The #5193 README and proof are unchanged at the publication base. +[SOURCES.json](SOURCES.json) pins the predecessor question, proof, exact-limit +proof, task catalogue and selected record as historical provenance. There are +no external executable inputs. [TASK.json](TASK.json) explicitly records the +changed scope from `independent-moment`: this is a user-selected arithmetic +side result, not completion of that paid-ledger card. + +The investigation inspected the source question, nearby PRs and Discussion +handoffs; a final live `projection in:title` PR search again returned #5193 as +the newest relevant projection result. This is bounded overlap coverage, not +a global priority claim. Unpublished work and every historical reply were not +exhaustively checked. + +No new kappa, selected-frontier improvement, supplier admission, hook-rank +certificate, physical caller, dirty-state restoration or full multiplication +theorem follows from this package. The optional triangle/max strengthening and +classification of all seeds are outside its scope. + +## Open next questions + +The structured questions and blockers are also in [TASK.json](TASK.json). + +1. **Which seeds have monotone top ratios?** The parity constants give necessary + tail inequalities. Start with the linear seed-to-mode map and adjacent + differences; equality cases still need higher terms and finite-prefix control. +2. **Can finite mode coefficients simplify further?** Start by extracting + coefficients of PROOF.md equation (7) for modes 1 through 4. A shorter + elementary expression could ease exact evaluation; none is established here. +3. **Can the inherited hook-rank and physical-engine premises be verified?** + Start with one source-bound #4628/#4643 hook-rank obligation. Those missing + certificates and complete physical costs are independent blockers to any + multiplication-bound interpretation. + +## Credit + +Prepared for NicholasStone with substantial OpenAI Codex assistance, including +a separate AI review agent. New text and code are Apache-2.0. + +Jacob Alan Sussman [#4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628) +supplied the recurrence, seed and proposed engine interpretation; Maximilian +Lutz [#4643](https://github.com/CrocSwap/integer-mult-bounds/pull/4643) supplied +independent projection counts and recurrence audit; Nick Petalas #5151 proved +the exact limit; JoyboyBrian +[#5184](https://github.com/CrocSwap/integer-mult-bounds/pull/5184) proved strict +finite-block descent; Krzysztof Wojt #5193 supplied the four modes and sharp +geometric order. Eumemic #288, Swapnil Jain, and the retained certificate/engine +lineage retain their credit. Q-Gauss summation is classical. diff --git a/research/projection-parity-constants/RESULT.json b/research/projection-parity-constants/RESULT.json new file mode 100644 index 0000000000..d310461659 --- /dev/null +++ b/research/projection-parity-constants/RESULT.json @@ -0,0 +1,91 @@ +{ + "status": "PASS_PROJECTION_PARITY_CONSTANTS", + "python": "3.12.14", + "checks": { + "whole_profile_equalities": 2691, + "finite_product_identities": 276, + "eigenmode_transformations": 520, + "generating_series_enclosures": 32, + "residue_checks": 16, + "rejected_negative_controls": 6 + }, + "exact": { + "limit": "439277/149175", + "mean": "815083/596700", + "K_coefficient": "323/28" + }, + "K_interval": [ + "0.0146710737642523866336315", + "0.0146710737642523866336316" + ], + "even_interval": [ + "1.53522589707598912534924", + "1.53522589707598912534925" + ], + "odd_interval": [ + "1.19674326665788049087331", + "1.19674326665788049087332" + ], + "samples": [ + { + "m": 8, + "scaled_error": "1.59639746634160655502181", + "absolute_gap_upper": "0.0611715692656174296725706" + }, + { + "m": 9, + "scaled_error": "1.21366133767430042156318", + "absolute_gap_upper": "0.0169180710164199306898611" + }, + { + "m": 16, + "scaled_error": "1.53545800153956595451344", + "absolute_gap_upper": "0.000232104463576829164194243" + }, + { + "m": 17, + "scaled_error": "1.19680882948816987890177", + "absolute_gap_upper": "0.0000655628302893880284539839" + }, + { + "m": 32, + "scaled_error": "1.53522590061722494693415", + "absolute_gap_upper": "3.54123582158490981280325E-9" + }, + { + "m": 33, + "scaled_error": "1.19674326765825881549630", + "absolute_gap_upper": "1.00037832462298535168112E-9" + }, + { + "m": 48, + "scaled_error": "1.53522589707604316031957", + "absolute_gap_upper": "5.40349703296570287933413E-14" + }, + { + "m": 49, + "scaled_error": "1.19674326665789575543515", + "absolute_gap_upper": "1.52645618314446976845378E-14" + }, + { + "m": 64, + "scaled_error": "1.53522589707598912617375", + "absolute_gap_upper": "8.24508214258661159082806E-19" + }, + { + "m": 65, + "scaled_error": "1.19674326665788049110623", + "absolute_gap_upper": "2.32919289081496269944492E-19" + }, + { + "m": 72, + "scaled_error": "1.53522589707598912535246", + "absolute_gap_upper": "3.22073521194789515138885E-21" + } + ], + "sha256": { + "PROOF.md": "ebb51aae7d58a69242c09b5334d02bd8178358cb2383ce90f38748e323e31ab0", + "verify.py": "77a36f5a328da71153f747284d318ac12a0fb9df16ffc06cbc75de7aaa40692d" + }, + "scope": "Exact finite corroboration; universal proof and classical q-Gauss are separate mathematical evidence." +} diff --git a/research/projection-parity-constants/REVIEW.md b/research/projection-parity-constants/REVIEW.md new file mode 100644 index 0000000000..7b7a114196 --- /dev/null +++ b/research/projection-parity-constants/REVIEW.md @@ -0,0 +1,70 @@ +# Independent mathematical and verifier review + +Verdict: **scoped pass**. A separate Codex review agent found no substantive +mathematical error in the stated recurrence theorem or the finite verifier. +This is an AI review, not independent human review or proof-kernel verification. + +The review started from the written proof and source recurrence, without the +solver's reasoning transcript. It checked the operator reduction, seed system, +generating equation, both q-Gauss substitutions against NIST DLMF 17.6.1, +product simplifications, meromorphic continuation, pole subtraction, index +shifts, finite-product expansions, and all three rational sums. Subtracting the +pole parts at 1, +/-2, and +/-4 leaves an analytic remainder on |z|<8, which +justifies the claimed O(4^-n) coefficient remainder for each fixed mode. + +Independent Fraction calculations checked transformations for modes 1 through +9, telescoping products for modes 1 through 4 and blocks 4 through 34, the seed +system, and the three rational constants. A separately written original integer +recurrence through block 100 corroborated the two limits and remainder order. + +## Verifier execution and enclosure review + +CPython 3.12.14 runs with `-I -X dev -W error -B` and with the additional `-O` +both passed. Their outputs were byte-identical to the reviewed RESULT.json: +2,691 whole-profile equalities, 276 product identities, 520 transformations, +32 generating-series enclosure comparisons, 16 residue checks, and six rejected +negative controls. Checks use explicit exceptions and remain active under `-O`. + +The interval tails are justified on the tested domains: + +- For j>=1, the transformed recurrence has nonnegative coefficients whose sum + is at most one. Induction gives 0<=v_n<=1 for all n, validating the ordinary + generating-series truncation bound. +- For |z|<=1/2 and ell>=terms>=j+4, the explicit q-series term ratio has modulus + at most 1690/6477<1/2. Twice the first omitted absolute term bounds its tail. +- For j>=1 and ell>=3, the negative-residue term ratio has modulus at most + 5/12<1/2. The helper now guards this domain; the tested truncation is 80 terms. +- The K interval follows from the product-tail inequality in the proof. + The displayed decimal intervals were checked to contain their exact rational + endpoints; every displayed `absolute_gap_upper` rounds upward. + +The six controls fail for their intended reasons: an altered seed coefficient, +omitted second subdiagonal, altered raw seed, perturbed eigenvalue, reversed +parity, and doubled residue factor. Their failure locations/messages were +inspected separately; no incidental exception accounts for these rejections. + +The terminating-series wording was clarified: all terms with ell>=j vanish. +Ordinary decimal rounding of enclosure bounds was replaced by directed rounding. +No unresolved substantive finding remains. + +## Scope and exact reviewed files + +Series-interval overlap is compatibility evidence, not an identity proof. +The eleven asymptotic samples and their threshold 32 do not establish a +universal numerical remainder constant. The universal theorem still relies on +the written analytic argument and classical q-Gauss summation. These six +controls are targeted perturbations, not exhaustive fault coverage. Global +novelty, engine interpretation, hook ranks, physical implementation, and any +multiplication-bound claim are outside this review. + +SHA-256 hashes bind this review to these exact files: + +| File | SHA-256 | +|---|---| +| PROOF.md | `ebb51aae7d58a69242c09b5334d02bd8178358cb2383ce90f38748e323e31ab0` | +| verify.py | `77a36f5a328da71153f747284d318ac12a0fb9df16ffc06cbc75de7aaa40692d` | +| RESULT.json | `cb48d1611d8f3d0ab77f084800b96881d934aca7efd11b7136f7f5196490a3e0` | + +Reviewed against the source snapshot +`ff3cc58e370d0f678e529246f8c73e8094e18fcf` and +. diff --git a/research/projection-parity-constants/SOURCES.json b/research/projection-parity-constants/SOURCES.json new file mode 100644 index 0000000000..7439881749 --- /dev/null +++ b/research/projection-parity-constants/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/projection-geometric-tail/README.md", + "usage": "provenance", + "git_blob": "3f9d51d11a2e018b8ddbc1bb507ea9e140b9955d", + "sha256": "41857587220722e5ce7b3e3beeaa2ff7697dc3d2a191b51f3a073c42f8ee7e36" + }, + { + "path": "research/projection-geometric-tail/PROOF.md", + "usage": "provenance", + "git_blob": "04818eac5f8f791352c004021e9db74a8a9137cc", + "sha256": "803efbaefac070b5a88c33035d53c6a326cb177e4d22ad7f9e6e2e1602ae3977" + }, + { + "path": "research/projection-recursion-limit/PROOF.md", + "usage": "provenance", + "git_blob": "ec946a12a248c33a45350fb780b0d02d992e62ea", + "sha256": "83843a1460d8d5ccca4c312268e3a138f5dddc8197986ba63955392a3da0da33" + } + ] +} diff --git a/research/projection-parity-constants/TASK.json b/research/projection-parity-constants/TASK.json new file mode 100644 index 0000000000..bbbd8f3bf1 --- /dev/null +++ b/research/projection-parity-constants/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "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": "Solve the explicit q-series and exact parity-leading-constant questions in projection-geometric-tail / PR #5193 for the unstrengthened block-four projection recurrence.", + "scope_change_reason": "The user asked for an unresolved repository problem. The explicit open question in PR #5193 was selected as a bounded follow-on; this is not a completion of the independent-moment paid-ledger card.", + "bottleneck_link": "Scoped arithmetic side result: identifies the exact parity obstruction to a single scaled-error limit and a generating function for the projection modes. It supplies no physical supplier, paid cost improvement, new kappa, or selected-frontier update.", + "budget_minutes": 60, + "stop_rule": "Stop after a complete scoped analytic argument, exact corroboration with targeted failure controls, independent AI review, and source-bound publication checks; do not extend the engine or claim its inherited hook ranks.", + "outcome": "completed", + "evidence": "PROOF.md: q-series formula and parity asymptotic with O(4^-m) remainder. RESULT.json: exact finite verification receipt. REVIEW.md: independent AI review bound to hashes of proof, verifier and receipt.", + "author": "NicholasStone", + "ai_assistance": "Prepared for NicholasStone with substantial OpenAI Codex assistance. A separate Codex agent independently reviewed the mathematics and verifier; this is AI review, not human or proof-kernel verification.", + "open_questions": [ + { + "question": "Which block-four seed profiles give monotone top ratios?", + "why_it_matters": "The q-series formulas expose exact parity boundary functionals, potentially simplifying the general-seed classification.", + "first_step": "Combine the four mode asymptotics with the linear seed-to-mode map and derive necessary parity inequalities for adjacent differences.", + "blocked_by": "Boundary cases need control of higher-order terms and the finite prefix; the leading asymptotic alone is insufficient." + }, + { + "question": "Can the finite mode coefficients be reduced to a shorter elementary expression?", + "why_it_matters": "This would simplify direct exact evaluation beyond the explicit convergent q-series supplied here.", + "first_step": "Study coefficient extraction in PROOF.md equation (7) for j=1 through 4 and terminating product cancellations.", + "blocked_by": "No further reduction is established; the current expression already solves the q-series part of the predecessor question." + }, + { + "question": "Can the inherited hook-rank inputs and physical engine obligations be independently established?", + "why_it_matters": "A recurrence theorem alone does not establish an integer multiplication cost bound.", + "first_step": "Read the retained #4628/#4643 source-bound obligations and isolate one hook-rank certificate for independent audit.", + "blocked_by": "This package contains neither physical realization nor complete recursive pricing evidence." + } + ] +} diff --git a/research/projection-parity-constants/VERIFY.json b/research/projection-parity-constants/VERIFY.json new file mode 100644 index 0000000000..98f77a3797 --- /dev/null +++ b/research/projection-parity-constants/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 recurrence/mode agreement, finite products, q-series enclosures, residue identities and six semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all explicit checks under optimized Python; checks do not rely on assertions." + } + ] +} diff --git a/research/projection-parity-constants/verify.py b/research/projection-parity-constants/verify.py new file mode 100644 index 0000000000..63ab99a630 --- /dev/null +++ b/research/projection-parity-constants/verify.py @@ -0,0 +1,236 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration; the universal proof is PROOF.md. Apache-2.0.""" +from decimal import Decimal, ROUND_CEILING, ROUND_FLOOR, localcontext +from fractions import Fraction as F +from hashlib import sha256 +import json +from math import prod +from pathlib import Path +import platform + +Q = F(1, 2) +SEED = (0, 27456, 48576, 68320, 86592) +C = (F(1), F(17, 39), F(6181, 14586), F(99085, 239811)) +LIMIT = F(439277, 149175) +MEAN = F(815083, 596700) +AMPLITUDE = F(323, 28) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def poch(a, n): + return prod((1 - a * Q**i for i in range(n)), start=F(1)) + + +def h(r): + return F(3, 2) + Q**r - 2**r + + +def integer_triangle(last, drop_second=False, seed=SEED): + """Direct source recurrence; no eigenmode or asymptotic code is used.""" + rows = {4: list(seed)} + for k in range(5, last + 1): + old = rows[k - 1] + new = [] + for r in range(k + 1): + a = 2**(k-r) - 1 + 4**k - 2**(k+r) + b = 2 * (2**k - 2**(k-r)) + (2**r-1) * 2**(k-1) + c = 0 if r < 2 else (2**r-1)*(2**(r-1)-1)*2**(k-r) + terms = ((r, a), (r-1, b), (r-2, 0 if drop_second else c)) + new.append(sum(coef*old[s] for s, coef in terms if 0 <= s < k)) + rows[k] = new + return rows + + +def eigenmode(j, last, h_shift=F(0)): + e = [F(0)] * j + [F(1)] + for r in range(j + 1, last + 1): + b = F(2**r, 2) + F(3, 2) - 2*Q**r + c = F(2**r, 2) - F(3, 2) + Q**r + e.append((b*e[r-1] + c*e[r-2]) / (h(j)+h_shift-h(r))) + return e + + +def mode_product(m, j): + out = F(1) + for k in range(5, m + 1): + out *= F((2**(k-j)-1)*(2**(k+j)+1), + (2**(k-1)-1)*(2**(k+1)+1)) + return out + + +def constants(j): + fj = poch(-Q, 2*j) / (poch(Q, j)*poch(-Q, j)**2) + gj = poch(-Q, 2*j) / (6*poch(Q, j-1)**2*poch(Q, j)) + pj = prod((1-Q**i for i in range(5-j, 4)), start=F(1)) + pj /= prod((1+Q**i for i in range(6, 5+j)), start=F(1)) + return pj, fj, gj + + +def k_interval(n): + need(n >= 3, "K interval domain") + high = prod((((1-Q**i)/(1+Q**i))**2 for i in range(1, n+1)), start=F(1)) + return high*(1-4*Q**n), high + + +def decimals(value, digits=24): + with localcontext() as ctx: + ctx.prec = digits + return str(Decimal(value.numerator)/Decimal(value.denominator)) + + +def outward_interval(low, high): + out = [] + for value, direction in ((low, ROUND_FLOOR), (high, ROUND_CEILING)): + with localcontext() as ctx: + ctx.prec = 24 + ctx.rounding = direction + out.append(str(Decimal(value.numerator)/Decimal(value.denominator))) + return out + + +def v_values(j, last): + s = 2**j + out = [F(1)] + for n in range(1, last+1): + rhs = (1+F(4, s)*Q**n)*out[n-1] + if n >= 2: + rhs += (1-2*Q**n)*out[n-2] + out.append(rhs/(2*(1+F(1, s*s)*Q**n))) + return out + + +def overlap(a, b): + return max(a[0], b[0]) <= min(a[1], b[1]) + + +def series_interval(j, z, terms=64): + """Explicit q-series (7); ratio of omitted terms has modulus <= 1/2.""" + need(abs(z) <= Q and terms >= j+4, "q-series domain") + s = 2**j + t = (1+F(1, s*s))/((1-z)*(1+z/2)) + total = F(0) + for ell in range(terms): + total += t + t *= -F(1, s*s)*(1-s*z*Q**ell/2)**2 + t /= (1-z*Q**(ell+1))*(1+z*Q**(ell+2)) + return total-2*abs(t), total+2*abs(t) + + +def negative_residue_interval(j, terms=80): + """Independent series evaluation at the -2 pole before q-Gauss.""" + need(isinstance(j, int) and j >= 1 and isinstance(terms, int) and terms >= 3, + "negative residue series domain") + s = 2**j + t = (1+F(1, s*s))/3 + total = F(0) + for ell in range(terms): + total += t + t *= -F(1, s*s)*(1+s*Q**ell)**2 + t /= (1+Q**ell)*(1-Q**(ell+1)) + return total-2*abs(t), total+2*abs(t) + + +def check_profile(rows, modes, coefficients=C): + checks = 0 + for m, row in rows.items(): + ps = [mode_product(m, j) for j in range(1, 5)] + for r in range(m+1): + predicted = sum(coefficients[j-1]*ps[j-1]*modes[j][r] for j in range(1, 5)) + need(predicted == F(row[r], row[1]), f"profile mismatch m={m} r={r}") + checks += 1 + return checks + + +def rejected(callback): + try: + callback() + except ValueError: + return 1 + raise ValueError("A negative control was incorrectly accepted") + + +def main(): + last = 72 + rows = integer_triangle(last) + modes = {j: eigenmode(j, last) for j in range(1, 5)} + checks = {"whole_profile_equalities": check_profile(rows, modes)} + limit = mean = amplitude = F(0) + product_checks = 0 + for j, c in enumerate(C, 1): + p, f, g = constants(j) + limit += c*p*f + mean += c*p*f*(2**j-Q**j-3)/2 + amplitude += c*p*(-1)**j*2**j*g + for m in range(4, last+1): + end = prod((1+Q**i for i in range(m+2, m+j+1)), start=F(1)) + end /= prod((1-Q**i for i in range(m-j+1, m)), start=F(1)) + need(mode_product(m, j) == p*end, "finite product telescoping") + product_checks += 1 + need((limit, mean, amplitude) == (LIMIT, MEAN, AMPLITUDE), "rational constants") + checks["finite_product_identities"] = product_checks + kl, kh = k_interval(80) + transformations = series_checks = residue_checks = 0 + for j in range(1, 9): + vs = v_values(j, 64) + es = eigenmode(j, j+64) + for n, v in enumerate(vs): + factor = poch(Q**(n+1), j)/poch(Q, j) + need(factor*v == es[j+n], "eigenmode transformation") + need(0 <= v <= 1, "subconvex recurrence bound") + transformations += 1 + for z in (F(-1, 2), F(-1, 4), F(1, 4), F(1, 2)): + value = sum(v*z**n for n, v in enumerate(vs)) + tail = abs(z)**len(vs)/(1-abs(z)) + need(overlap((value-tail, value+tail), series_interval(j, z)), "generating series") + series_checks += 1 + aj = poch(-Q, 2*j)/poch(-Q, j)**2 + finite = sum((-Q**(2*j))**ell * poch(F(2**j, 2), ell)**2 / + (poch(Q, ell)*poch(-Q, ell+1)) for ell in range(j)) + need((1+Q**(2*j))*finite == aj, "positive residue summation") + bj = poch(-Q, 2*j)/(6*poch(Q, j-1)**2) + need(overlap(negative_residue_interval(j), (bj*kl, bj*kh)), "negative residue q-Gauss") + residue_checks += 2 + checks.update(eigenmode_transformations=transformations, + generating_series_enclosures=series_checks, + residue_checks=residue_checks) + samples = [] + for m in (8, 9, 16, 17, 32, 33, 48, 49, 64, 65, 72): + scaled = 2**m*(F(rows[m][m], rows[m][1])-LIMIT) + lo = MEAN + AMPLITUDE*(kl if m % 2 == 0 else -kh) + hi = MEAN + AMPLITUDE*(kh if m % 2 == 0 else -kl) + # A finite corroboration threshold, not a claimed universal remainder constant. + need(max(abs(scaled-lo), abs(scaled-hi)) < 32*Q**m, "asymptotic sample") + samples.append({"m": m, "scaled_error": decimals(scaled), + "absolute_gap_upper": outward_interval(F(0), max(abs(scaled-lo), abs(scaled-hi)))[1]}) + controls = 0 + short = {m: rows[m] for m in range(4, 9)} + bad_c = list(C); bad_c[3] += 1 + controls += rejected(lambda: check_profile(short, modes, bad_c)) + controls += rejected(lambda: check_profile(integer_triangle(8, drop_second=True), modes)) + bad_seed = list(SEED); bad_seed[3] += 1 + controls += rejected(lambda: check_profile(integer_triangle(8, seed=bad_seed), modes)) + bad_modes = dict(modes); bad_modes[2] = eigenmode(2, last, F(1, 100)) + controls += rejected(lambda: check_profile(short, bad_modes)) + even_scaled = 2**32*(F(rows[32][32], rows[32][1])-LIMIT) + controls += rejected(lambda: need(abs(even_scaled-(MEAN-AMPLITUDE*kl)) < Q**20, "wrong parity")) + b1 = poch(-Q, 2)/(6*poch(Q, 0)**2) + controls += rejected(lambda: need(overlap(negative_residue_interval(1), (2*b1*kl, 2*b1*kh)), "wrong residue factor")) + checks["rejected_negative_controls"] = controls + root = Path(__file__).resolve().parent + hashes = {name: sha256((root/name).read_bytes()).hexdigest() for name in ("PROOF.md", "verify.py")} + result = {"status": "PASS_PROJECTION_PARITY_CONSTANTS", "python": platform.python_version(), + "checks": checks, "exact": {"limit": str(LIMIT), "mean": str(MEAN), "K_coefficient": str(AMPLITUDE)}, + "K_interval": outward_interval(kl, kh), + "even_interval": outward_interval(MEAN+AMPLITUDE*kl, MEAN+AMPLITUDE*kh), + "odd_interval": outward_interval(MEAN-AMPLITUDE*kh, MEAN-AMPLITUDE*kl), + "samples": samples, "sha256": hashes, + "scope": "Exact finite corroboration; universal proof and classical q-Gauss are separate mathematical evidence."} + print(json.dumps(result, indent=2)) + + +if __name__ == "__main__": + main()