diff --git a/research/heavy-tensor-dimension/README.md b/research/heavy-tensor-dimension/README.md new file mode 100644 index 0000000000..187c2a646a --- /dev/null +++ b/research/heavy-tensor-dimension/README.md @@ -0,0 +1,182 @@ +# Sharp dimension scale of the heavy tensor-error envelope + +This scoped proof replaces a linear sufficient dimension gate by the sharp +quadratic scale of the stated scalar error envelope. For fixed nonnegative +constants K,C, the largest admissible integer dimension satisfies + +```text +g_max(p) ln(p) / p^2 -> 1/10. +``` + +At p=64 and K=C=0, the exact largest dimension is 98. Dimension 99 fails +the scalar inequality. A simpler integer-only gate already certifies g=68. +James Reed's #4695 sufficient gate certifies through g=10 there. The latter +is a consequence of its stated hypothesis, not a replay of its verifier. + +This contribution is produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. New work is Apache-2.0. + +## Scope and predecessor credit + +The inherited envelope is + +```text +M(p,g,K) = g (p^10)^(g-1) p^6 (1+p^4) exp(Kp-p^2) + = g p^(10g) (1+p^-4) exp(Kp-p^2). +``` + +The question is exactly when M < 2^(-Cp), for integers p>=2, g>=1 and +nonnegative K,C. The proof allows real K,C; the finite verifier uses integers. +Credit James Reed's merged #4695 for g copies and the factor-1 sufficient +gate, #4693 for the single slice, #4526 for the heavy trailing slice and +#4524 for the unequal-tail factor. Jose Manuel's #4100 supplies the retained +Gaussian/HALO setting. Source READMEs are pinned in SOURCES.json. Their +results are premises and context; no predecessor computation is replayed. + +The `uniform-transfer-audit` card changes to a new scalar dimension theorem. +This is a side result about a quantified error budget. It does not settle +an existing proof's correctness. It exposes slack in this one restriction +without removing other restrictions on g. In particular, the original +header, storage, geometry and physical-cost conditions may still require +`g log p=o(p)`. No caller at the larger dimension is constructed here. + +## Proof + +All logarithms in this section are natural. Put + +```text +a = 10 ln p, +B = p^2 - (K+C ln 2)p - ln(1+p^-4), +f(x) = a x + ln x. +``` + +Taking the logarithm of M 2^(Cp) gives exactly f(g)-B. Since +f'(x)=a+1/x>0 for x>0, and f ranges from minus infinity to plus infinity, +there is a unique positive real x_* with f(x_*)=B. Consequently + +```text +g_max = max(0, ceil(x_*)-1). +``` + +The strict ceiling accounts for the strict error inequality, including a +hypothetical integer root. If B<=a, no positive integer is admissible. +If B>a, let t=B/a>1. The following explicit bracket avoids special functions: + +```text +t - (ln t)/a < x_* < t. +``` + +Indeed u=t-(ln t)/a is positive. For p>=2, a>1, and ln t1. +Now f(t)=B+ln t>B, whereas +f(u)=B-ln t+ln u1/10, ceil(alpha p^2/ln p) fails +for all sufficiently large p. This proves sharpness for the envelope. +Failure of an upper envelope does not prove failure of an actual operator. + +## A fully integer sufficient gate + +Let L=ceil(log2 p). For nonnegative integer K,C, the condition + +```text +10gL + 2L + 1 + (2K+C)p <= p^2 +``` + +suffices for M<2^(-Cp). It implies g=2^(n-1) for n>=1, with strictness for n>=3. Multiplying gives + +```text +M 2^(Cp) < 2^[10gL+2L+1+(2K+C)p-p^2] <= 1. +``` + +This gate permits order p^2/log p and requires neither p>=64 nor a +separate linear parameter bound. At p=64, L=6, K=C=0, g=68 gives +4093<=4096. At g=69 this particular sufficient gate fails, without +implying failure of M. The exact boundary remains 98. + +## Exact finite evidence + +The standalone verifier uses only integer and Fraction arithmetic. For +1<=x<=2 and z=(x-1)/(x+1), it encloses ln x by + +```text +S_N = 2 sum_(j=0)^(N-1) z^(2j+1)/(2j+1), +S_N <= ln x <= S_N + 2 z^(2N+1)/[(2N+1)(1-z^2)]. +``` + +The positive logarithm series follows by integrating the geometric series +for 2/(1-z^2). Bounding every remaining denominator below by 2N+1 gives +the stated tail. Range reduction x=n/2^k puts integer logarithms in this +interval. All loops have explicit bounds; N=32 in boundary decisions. +A sign overlapping zero fails closed instead of guessing. + +RESULT.json is a generated receipt with source hashes and rational sign +bounds. Its 207 boundary cases include 175 positive integer-gate checks. +Eleven neighboring signs also pass independent rational e-power comparisons. +Seventeen semantic controls cover invalid arguments, series contracts, log +identities, the integer gate and the p=64 sign margins. The verifier finds the last admissible integer by monotonic +binary search, certifies both neighboring signs, checks the integer gate, +and compares a bounded subset against literal rational powers enclosing e. +The independent power comparison does not use the logarithm implementation. +The p=64 signs are additionally separated by the rational margins +`log(M(64,98,0)) < -15` and `log(M(64,99,0)) > 25`. +No floats, predecessor scripts or scientific dependencies are imported. +The recorded finite counts are corroboration; the all-p conclusion rests +on the written proof above. + +## Reproduce + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/heavy-tensor-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/heavy-tensor-dimension +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/heavy-tensor-dimension --check-source-history +``` + +The registered replay includes warning-strict ordinary and optimized runs. +A normal replay reads the receipt and writes nothing. Explicit +`--write-receipt PATH` generates a receipt and refuses an existing path. +CPython 3.12 is sufficient; there are no third-party requirements. + +## Limitations + +The tail formula, norm ceilings and any correspondence to the physical +Gaussian caller remain hypotheses. This proof does not cover operator +conditioning, headers, storage, movement, restoration, recursive admission +or the full multiplication theorem. It yields no new kappa and changes no +selected record. No Lean, Docker, selected-supplier cold replay or independent +human proof review was run. + +Python's managed integer/Fraction allocation is a Power of Ten deviation. +The verifier limits p to 2^20, g to p^2+1, K,C to 2^20, series lengths to +64, and file sizes to 2 MiB. Loops and binary search depth are bounded. +These are verifier resource bounds, not restrictions on the written proof. + +## Open next questions + +1. Which actual caller restriction first blocks dimensions at the quadratic + error scale? This matters because numerical error is only one obligation. + Start by stating one caller's header-size and storage inequalities with + its fixed parameters. The missing physical contract blocks a claimed + algorithmic improvement; no larger implementation campaign is implied. +2. Can a concrete tensor caller use unequal per-axis norm ceilings to obtain + a larger certified dimension than this worst-slice envelope permits? + Start with its explicit ordered list of norm and error bounds. Those + caller data are absent here; a formal change to the scalar envelope is + insufficient by itself. diff --git a/research/heavy-tensor-dimension/RESULT.json b/research/heavy-tensor-dimension/RESULT.json new file mode 100644 index 0000000000..8e0cbcfc04 --- /dev/null +++ b/research/heavy-tensor-dimension/RESULT.json @@ -0,0 +1,3077 @@ +{ + "schema_version": 1, + "status": "PASS_HEAVY_TENSOR_DIMENSION", + "source_sha256": { + "README.md": "1ec0e35889b121ec4fdb647af5c8716e122de1694008078682a1cbc5810dce9e", + "TASK.json": "25998f824463b898be702cc1b3090a4e9f625a429e2061e004da48b3d2c548b0", + "SOURCES.json": "f71d4235e8802f231c9257cad56f35e5becfe0d18fc29aea29287e5669a4a493", + "VERIFY.json": "6e4097f5aadb2b2ee23c90749610b73bae9261c3d768d951fb3cdd12c43dfc15", + "verify.py": "1e553e2e025823703bb364ad3c261ab0ab923c123921d94e99da3d51feadb2d4", + "research/gaussian-heavy-slice/README.md": "42feda423dd82675b5de0917425941b99c203d257915ad7855ceb2af86c48ad6", + "research/gaussian-slice-one-copies/README.md": "f6b584cab7a948775bdeae9e3708443e29c70224c51484eff49cdc1de6e8d73e" + }, + "series_terms": 32, + "boundary_cases": 207, + "integer_gate_checks": 175, + "independent_power_comparisons": 11, + "semantic_controls": 17, + "boundaries": [ + { + "p": 2, + "K": 0, + "C": 0, + "maximum": 0, + "success_log": null, + "next_log": [ + "374/125", + "2993/1000" + ], + "gate": 0 + }, + { + "p": 2, + "K": 1, + "C": 2, + "maximum": 0, + "success_log": null, + "next_log": [ + "1941/250", + "1553/200" + ], + "gate": 0 + }, + { + "p": 2, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "423/20", + "21151/1000" + ], + "gate": 0 + }, + { + "p": 3, + "K": 0, + "C": 0, + "maximum": 0, + "success_log": null, + "next_log": [ + "999/500", + "1999/1000" + ], + "gate": 0 + }, + { + "p": 3, + "K": 1, + "C": 2, + "maximum": 0, + "success_log": null, + "next_log": [ + "9157/1000", + "4579/500" + ], + "gate": 0 + }, + { + "p": 3, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "7309/250", + "29237/1000" + ], + "gate": 0 + }, + { + "p": 4, + "K": 0, + "C": 0, + "maximum": 1, + "success_log": [ + "-1067/500", + "-2133/1000" + ], + "next_log": [ + "6211/500", + "12423/1000" + ], + "gate": 0 + }, + { + "p": 4, + "K": 1, + "C": 2, + "maximum": 0, + "success_log": null, + "next_log": [ + "1853/250", + "7413/1000" + ], + "gate": 0 + }, + { + "p": 4, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "4273/125", + "6837/200" + ], + "gate": 0 + }, + { + "p": 5, + "K": 0, + "C": 0, + "maximum": 1, + "success_log": [ + "-1781/200", + "-1113/125" + ], + "next_log": [ + "7883/1000", + "1971/250" + ], + "gate": 0 + }, + { + "p": 5, + "K": 1, + "C": 2, + "maximum": 0, + "success_log": null, + "next_log": [ + "3027/1000", + "757/250" + ], + "gate": 0 + }, + { + "p": 5, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "36493/1000", + "18247/500" + ], + "gate": 0 + }, + { + "p": 6, + "K": 0, + "C": 0, + "maximum": 1, + "success_log": [ + "-9041/500", + "-18081/1000" + ], + "next_log": [ + "529/1000", + "53/100" + ], + "gate": 0 + }, + { + "p": 6, + "K": 1, + "C": 2, + "maximum": 1, + "success_log": [ + "-941/250", + "-3763/1000" + ], + "next_log": [ + "7423/500", + "14847/1000" + ], + "gate": 0 + }, + { + "p": 6, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "7279/200", + "9099/250" + ], + "gate": 0 + }, + { + "p": 7, + "K": 0, + "C": 0, + "maximum": 2, + "success_log": [ + "-9389/1000", + "-2347/250" + ], + "next_log": [ + "2619/250", + "10477/1000" + ], + "gate": 1 + }, + { + "p": 7, + "K": 1, + "C": 2, + "maximum": 1, + "success_log": [ + "-12837/1000", + "-3209/250" + ], + "next_log": [ + "1463/200", + "1829/250" + ], + "gate": 0 + }, + { + "p": 7, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "6803/200", + "4252/125" + ], + "gate": 0 + }, + { + "p": 8, + "K": 0, + "C": 0, + "maximum": 3, + "success_log": [ + "-259/500", + "-517/1000" + ], + "next_log": [ + "5141/250", + "4113/200" + ], + "gate": 1 + }, + { + "p": 8, + "K": 1, + "C": 2, + "maximum": 2, + "success_log": [ + "-657/250", + "-2627/1000" + ], + "next_log": [ + "4643/250", + "18573/1000" + ], + "gate": 0 + }, + { + "p": 8, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "2943/100", + "29431/1000" + ], + "gate": 0 + }, + { + "p": 9, + "K": 0, + "C": 0, + "maximum": 3, + "success_log": [ + "-2797/200", + "-1748/125" + ], + "next_log": [ + "331/40", + "2069/250" + ], + "gate": 1 + }, + { + "p": 9, + "K": 1, + "C": 2, + "maximum": 2, + "success_log": [ + "-7443/500", + "-2977/200" + ], + "next_log": [ + "1873/250", + "7493/1000" + ], + "gate": 0 + }, + { + "p": 9, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "22687/1000", + "2836/125" + ], + "gate": 0 + }, + { + "p": 10, + "K": 0, + "C": 0, + "maximum": 4, + "success_log": [ + "-6511/1000", + "-651/100" + ], + "next_log": [ + "8369/500", + "16739/1000" + ], + "gate": 2 + }, + { + "p": 10, + "K": 1, + "C": 2, + "maximum": 3, + "success_log": [ + "-5961/1000", + "-149/25" + ], + "next_log": [ + "2169/125", + "17353/1000" + ], + "gate": 1 + }, + { + "p": 10, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "691/50", + "13821/1000" + ], + "gate": 0 + }, + { + "p": 11, + "K": 0, + "C": 0, + "maximum": 4, + "success_log": [ + "-11849/500", + "-23697/1000" + ], + "next_log": [ + "63/125", + "101/200" + ], + "gate": 2 + }, + { + "p": 11, + "K": 1, + "C": 2, + "maximum": 3, + "success_log": [ + "-5429/250", + "-4343/200" + ], + "next_log": [ + "2551/1000", + "319/125" + ], + "gate": 1 + }, + { + "p": 11, + "K": 7, + "C": 3, + "maximum": 0, + "success_log": null, + "next_log": [ + "713/250", + "2853/1000" + ], + "gate": 0 + }, + { + "p": 12, + "K": 0, + "C": 0, + "maximum": 5, + "success_log": [ + "-9073/500", + "-3629/200" + ], + "next_log": [ + "3443/500", + "6887/1000" + ], + "gate": 3 + }, + { + "p": 12, + "K": 1, + "C": 2, + "maximum": 4, + "success_log": [ + "-7291/500", + "-14581/1000" + ], + "next_log": [ + "1049/100", + "10491/1000" + ], + "gate": 2 + }, + { + "p": 12, + "K": 7, + "C": 3, + "maximum": 1, + "success_log": [ + "-5099/500", + "-10197/1000" + ], + "next_log": [ + "1918/125", + "3069/200" + ], + "gate": 0 + }, + { + "p": 13, + "K": 0, + "C": 0, + "maximum": 6, + "success_log": [ + "-1664/125", + "-13311/1000" + ], + "next_log": [ + "3123/250", + "12493/1000" + ], + "gate": 4 + }, + { + "p": 13, + "K": 1, + "C": 2, + "maximum": 5, + "success_log": [ + "-4061/500", + "-8121/1000" + ], + "next_log": [ + "1771/100", + "17711/1000" + ], + "gate": 2 + }, + { + "p": 13, + "K": 7, + "C": 3, + "maximum": 1, + "success_log": [ + "-12659/500", + "-25317/1000" + ], + "next_log": [ + "128/125", + "41/40" + ], + "gate": 0 + }, + { + "p": 14, + "K": 0, + "C": 0, + "maximum": 7, + "success_log": [ + "-9321/1000", + "-233/25" + ], + "next_log": [ + "4301/250", + "3441/200" + ], + "gate": 4 + }, + { + "p": 14, + "K": 1, + "C": 2, + "maximum": 6, + "success_log": [ + "-2457/1000", + "-307/125" + ], + "next_log": [ + "3011/125", + "24089/1000" + ], + "gate": 3 + }, + { + "p": 14, + "K": 7, + "C": 3, + "maximum": 2, + "success_log": [ + "-7707/500", + "-15413/1000" + ], + "next_log": [ + "5691/500", + "11383/1000" + ], + "gate": 0 + }, + { + "p": 15, + "K": 0, + "C": 0, + "maximum": 8, + "success_log": [ + "-6277/1000", + "-1569/250" + ], + "next_log": [ + "20921/1000", + "10461/500" + ], + "gate": 5 + }, + { + "p": 15, + "K": 1, + "C": 2, + "maximum": 6, + "success_log": [ + "-24931/1000", + "-2493/100" + ], + "next_log": [ + "2303/1000", + "288/125" + ], + "gate": 3 + }, + { + "p": 15, + "K": 7, + "C": 3, + "maximum": 3, + "success_log": [ + "-6469/1000", + "-1617/250" + ], + "next_log": [ + "20899/1000", + "209/10" + ], + "gate": 0 + }, + { + "p": 16, + "K": 0, + "C": 0, + "maximum": 9, + "success_log": [ + "-427/100", + "-4269/1000" + ], + "next_log": [ + "23561/1000", + "11781/500" + ], + "gate": 6 + }, + { + "p": 16, + "K": 1, + "C": 2, + "maximum": 7, + "success_log": [ + "-21793/1000", + "-2724/125" + ], + "next_log": [ + "6067/1000", + "1517/250" + ], + "gate": 4 + }, + { + "p": 16, + "K": 7, + "C": 3, + "maximum": 3, + "success_log": [ + "-26453/1000", + "-6613/250" + ], + "next_log": [ + "39/25", + "1561/1000" + ], + "gate": 0 + }, + { + "p": 17, + "K": 0, + "C": 0, + "maximum": 10, + "success_log": [ + "-3377/1000", + "-422/125" + ], + "next_log": [ + "25051/1000", + "6263/250" + ], + "gate": 5 + }, + { + "p": 17, + "K": 1, + "C": 2, + "maximum": 8, + "success_log": [ + "-19697/1000", + "-2462/125" + ], + "next_log": [ + "8753/1000", + "4377/500" + ], + "gate": 4 + }, + { + "p": 17, + "K": 7, + "C": 3, + "maximum": 4, + "success_log": [ + "-3987/200", + "-9967/500" + ], + "next_log": [ + "431/50", + "8621/1000" + ], + "gate": 0 + }, + { + "p": 18, + "K": 0, + "C": 0, + "maximum": 11, + "success_log": [ + "-1831/500", + "-3661/1000" + ], + "next_log": [ + "25329/1000", + "2533/100" + ], + "gate": 6 + }, + { + "p": 18, + "K": 1, + "C": 2, + "maximum": 9, + "success_log": [ + "-18717/1000", + "-4679/250" + ], + "next_log": [ + "10293/1000", + "5147/500" + ], + "gate": 4 + }, + { + "p": 18, + "K": 7, + "C": 3, + "maximum": 5, + "success_log": [ + "-14443/1000", + "-7221/500" + ], + "next_log": [ + "3661/250", + "2929/200" + ], + "gate": 0 + }, + { + "p": 19, + "K": 0, + "C": 0, + "maximum": 12, + "success_log": [ + "-5183/1000", + "-2591/500" + ], + "next_log": [ + "12171/500", + "24343/1000" + ], + "gate": 7 + }, + { + "p": 19, + "K": 1, + "C": 2, + "maximum": 10, + "success_log": [ + "-9457/500", + "-18913/1000" + ], + "next_log": [ + "85/8", + "5313/500" + ], + "gate": 5 + }, + { + "p": 19, + "K": 7, + "C": 3, + "maximum": 6, + "success_log": [ + "-10033/1000", + "-1254/125" + ], + "next_log": [ + "9783/500", + "19567/1000" + ], + "gate": 0 + }, + { + "p": 20, + "K": 0, + "C": 0, + "maximum": 13, + "success_log": [ + "-799/100", + "-7989/1000" + ], + "next_log": [ + "22041/1000", + "11021/500" + ], + "gate": 7 + }, + { + "p": 20, + "K": 1, + "C": 2, + "maximum": 11, + "success_log": [ + "-10173/500", + "-4069/200" + ], + "next_log": [ + "4849/500", + "9699/1000" + ], + "gate": 6 + }, + { + "p": 20, + "K": 7, + "C": 3, + "maximum": 7, + "success_log": [ + "-1691/250", + "-6763/1000" + ], + "next_log": [ + "11663/500", + "23327/1000" + ], + "gate": 0 + }, + { + "p": 21, + "K": 0, + "C": 0, + "maximum": 14, + "success_log": [ + "-1516/125", + "-12127/1000" + ], + "next_log": [ + "9193/500", + "18387/1000" + ], + "gate": 8 + }, + { + "p": 21, + "K": 1, + "C": 2, + "maximum": 12, + "success_log": [ + "-23061/1000", + "-1153/50" + ], + "next_log": [ + "1493/200", + "3733/500" + ], + "gate": 6 + }, + { + "p": 21, + "K": 7, + "C": 3, + "maximum": 8, + "success_log": [ + "-4691/1000", + "-469/100" + ], + "next_log": [ + "3234/125", + "25873/1000" + ], + "gate": 1 + }, + { + "p": 22, + "K": 0, + "C": 0, + "maximum": 15, + "success_log": [ + "-4409/250", + "-3527/200" + ], + "next_log": [ + "13339/1000", + "667/50" + ], + "gate": 9 + }, + { + "p": 22, + "K": 1, + "C": 2, + "maximum": 13, + "success_log": [ + "-13551/500", + "-27101/1000" + ], + "next_log": [ + "3883/1000", + "971/250" + ], + "gate": 7 + }, + { + "p": 22, + "K": 7, + "C": 3, + "maximum": 9, + "success_log": [ + "-1931/500", + "-3861/1000" + ], + "next_log": [ + "13577/500", + "5431/200" + ], + "gate": 1 + }, + { + "p": 23, + "K": 0, + "C": 0, + "maximum": 16, + "success_log": [ + "-24549/1000", + "-6137/250" + ], + "next_log": [ + "6867/1000", + "1717/250" + ], + "gate": 10 + }, + { + "p": 23, + "K": 1, + "C": 2, + "maximum": 15, + "success_log": [ + "-271/250", + "-1083/1000" + ], + "next_log": [ + "3792/125", + "30337/1000" + ], + "gate": 8 + }, + { + "p": 23, + "K": 7, + "C": 3, + "maximum": 10, + "success_log": [ + "-4321/1000", + "-108/25" + ], + "next_log": [ + "27129/1000", + "2713/100" + ], + "gate": 2 + }, + { + "p": 24, + "K": 0, + "C": 0, + "maximum": 18, + "success_log": [ + "-53/50", + "-1059/1000" + ], + "next_log": [ + "15387/500", + "1231/40" + ], + "gate": 11 + }, + { + "p": 24, + "K": 1, + "C": 2, + "maximum": 16, + "success_log": [ + "-1867/250", + "-7467/1000" + ], + "next_log": [ + "24373/1000", + "12187/500" + ], + "gate": 9 + }, + { + "p": 24, + "K": 7, + "C": 3, + "maximum": 11, + "success_log": [ + "-611/100", + "-6109/1000" + ], + "next_log": [ + "25757/1000", + "12879/500" + ], + "gate": 3 + }, + { + "p": 25, + "K": 0, + "C": 0, + "maximum": 19, + "success_log": [ + "-1047/100", + "-10469/1000" + ], + "next_log": [ + "2177/100", + "21771/1000" + ], + "gate": 12 + }, + { + "p": 25, + "K": 1, + "C": 2, + "maximum": 17, + "success_log": [ + "-15301/1000", + "-153/10" + ], + "next_log": [ + "3389/200", + "8473/500" + ], + "gate": 10 + }, + { + "p": 25, + "K": 7, + "C": 3, + "maximum": 12, + "success_log": [ + "-1158/125", + "-9263/1000" + ], + "next_log": [ + "5751/250", + "4601/200" + ], + "gate": 3 + }, + { + "p": 26, + "K": 0, + "C": 0, + "maximum": 20, + "success_log": [ + "-4277/200", + "-2673/125" + ], + "next_log": [ + "2811/250", + "2249/200" + ], + "gate": 13 + }, + { + "p": 26, + "K": 1, + "C": 2, + "maximum": 18, + "success_log": [ + "-24609/1000", + "-3076/125" + ], + "next_log": [ + "4013/500", + "8027/1000" + ], + "gate": 11 + }, + { + "p": 26, + "K": 7, + "C": 3, + "maximum": 13, + "success_log": [ + "-6909/500", + "-13817/1000" + ], + "next_log": [ + "9419/500", + "18839/1000" + ], + "gate": 4 + }, + { + "p": 27, + "K": 0, + "C": 0, + "maximum": 22, + "success_log": [ + "-33/40", + "-103/125" + ], + "next_log": [ + "32177/1000", + "16089/500" + ], + "gate": 14 + }, + { + "p": 27, + "K": 1, + "C": 2, + "maximum": 20, + "success_log": [ + "-2407/1000", + "-1203/500" + ], + "next_log": [ + "153/5", + "30601/1000" + ], + "gate": 12 + }, + { + "p": 27, + "K": 7, + "C": 3, + "maximum": 14, + "success_log": [ + "-19799/1000", + "-9899/500" + ], + "next_log": [ + "3307/250", + "13229/1000" + ], + "gate": 5 + }, + { + "p": 28, + "K": 0, + "C": 0, + "maximum": 23, + "success_log": [ + "-7229/500", + "-14457/1000" + ], + "next_log": [ + "18907/1000", + "4727/250" + ], + "gate": 15 + }, + { + "p": 28, + "K": 1, + "C": 2, + "maximum": 21, + "success_log": [ + "-14377/1000", + "-1797/125" + ], + "next_log": [ + "2374/125", + "18993/1000" + ], + "gate": 13 + }, + { + "p": 28, + "K": 7, + "C": 3, + "maximum": 15, + "success_log": [ + "-27237/1000", + "-6809/250" + ], + "next_log": [ + "6149/1000", + "123/20" + ], + "gate": 5 + }, + { + "p": 29, + "K": 0, + "C": 0, + "maximum": 24, + "success_log": [ + "-29671/1000", + "-2967/100" + ], + "next_log": [ + "2021/500", + "4043/1000" + ], + "gate": 16 + }, + { + "p": 29, + "K": 1, + "C": 2, + "maximum": 22, + "success_log": [ + "-13951/500", + "-27901/1000" + ], + "next_log": [ + "727/125", + "5817/1000" + ], + "gate": 14 + }, + { + "p": 29, + "K": 7, + "C": 3, + "maximum": 17, + "success_log": [ + "-2423/1000", + "-1211/500" + ], + "next_log": [ + "31307/1000", + "7827/250" + ], + "gate": 6 + }, + { + "p": 30, + "K": 0, + "C": 0, + "maximum": 26, + "success_log": [ + "-12431/1000", + "-1243/100" + ], + "next_log": [ + "21619/1000", + "1081/50" + ], + "gate": 17 + }, + { + "p": 30, + "K": 1, + "C": 2, + "maximum": 24, + "success_log": [ + "-4473/500", + "-1789/200" + ], + "next_log": [ + "25107/1000", + "6277/250" + ], + "gate": 15 + }, + { + "p": 30, + "K": 7, + "C": 3, + "maximum": 18, + "success_log": [ + "-12511/1000", + "-1251/100" + ], + "next_log": [ + "4311/200", + "5389/250" + ], + "gate": 7 + }, + { + "p": 31, + "K": 0, + "C": 0, + "maximum": 27, + "success_log": [ + "-3816/125", + "-30527/1000" + ], + "next_log": [ + "481/125", + "3849/1000" + ], + "gate": 19 + }, + { + "p": 31, + "K": 1, + "C": 2, + "maximum": 25, + "success_log": [ + "-2531/100", + "-25309/1000" + ], + "next_log": [ + "9069/1000", + "907/100" + ], + "gate": 16 + }, + { + "p": 31, + "K": 7, + "C": 3, + "maximum": 19, + "success_log": [ + "-3017/125", + "-4827/200" + ], + "next_log": [ + "2051/200", + "1282/125" + ], + "gate": 8 + }, + { + "p": 32, + "K": 0, + "C": 0, + "maximum": 29, + "success_log": [ + "-1557/100", + "-15569/1000" + ], + "next_log": [ + "19121/1000", + "9561/500" + ], + "gate": 20 + }, + { + "p": 32, + "K": 1, + "C": 2, + "maximum": 27, + "success_log": [ + "-1719/200", + "-4297/500" + ], + "next_log": [ + "26099/1000", + "261/10" + ], + "gate": 17 + }, + { + "p": 32, + "K": 7, + "C": 3, + "maximum": 21, + "success_log": [ + "-2609/1000", + "-326/125" + ], + "next_log": [ + "6419/200", + "4012/125" + ], + "gate": 9 + }, + { + "p": 33, + "K": 0, + "C": 0, + "maximum": 31, + "success_log": [ + "-1649/1000", + "-206/125" + ], + "next_log": [ + "8337/250", + "33349/1000" + ], + "gate": 17 + }, + { + "p": 33, + "K": 1, + "C": 2, + "maximum": 28, + "success_log": [ + "-13949/500", + "-27897/1000" + ], + "next_log": [ + "3551/500", + "7103/1000" + ], + "gate": 15 + }, + { + "p": 33, + "K": 7, + "C": 3, + "maximum": 22, + "success_log": [ + "-2132/125", + "-3411/200" + ], + "next_log": [ + "17953/1000", + "8977/500" + ], + "gate": 8 + }, + { + "p": 34, + "K": 0, + "C": 0, + "maximum": 32, + "success_log": [ + "-24099/1000", + "-12049/500" + ], + "next_log": [ + "2239/200", + "2799/250" + ], + "gate": 19 + }, + { + "p": 34, + "K": 1, + "C": 2, + "maximum": 30, + "success_log": [ + "-13557/1000", + "-3389/250" + ], + "next_log": [ + "21739/1000", + "1087/50" + ], + "gate": 16 + }, + { + "p": 34, + "K": 7, + "C": 3, + "maximum": 23, + "success_log": [ + "-33101/1000", + "-331/10" + ], + "next_log": [ + "441/200", + "1103/500" + ], + "gate": 9 + }, + { + "p": 35, + "K": 0, + "C": 0, + "maximum": 34, + "success_log": [ + "-1582/125", + "-2531/200" + ], + "next_log": [ + "22927/1000", + "2866/125" + ], + "gate": 20 + }, + { + "p": 35, + "K": 1, + "C": 2, + "maximum": 32, + "success_log": [ + "-303/1000", + "-151/500" + ], + "next_log": [ + "35281/1000", + "17641/500" + ], + "gate": 17 + }, + { + "p": 35, + "K": 7, + "C": 3, + "maximum": 25, + "success_log": [ + "-3791/250", + "-15163/1000" + ], + "next_log": [ + "20429/1000", + "2043/100" + ], + "gate": 10 + }, + { + "p": 36, + "K": 0, + "C": 0, + "maximum": 36, + "success_log": [ + "-47/20", + "-2349/1000" + ], + "next_log": [ + "4189/125", + "33513/1000" + ], + "gate": 21 + }, + { + "p": 36, + "K": 1, + "C": 2, + "maximum": 33, + "success_log": [ + "-6009/250", + "-4807/200" + ], + "next_log": [ + "11829/1000", + "1183/100" + ], + "gate": 18 + }, + { + "p": 36, + "K": 7, + "C": 3, + "maximum": 26, + "success_log": [ + "-4271/125", + "-34167/1000" + ], + "next_log": [ + "341/200", + "853/500" + ], + "gate": 11 + }, + { + "p": 37, + "K": 0, + "C": 0, + "maximum": 37, + "success_log": [ + "-587/20", + "-29349/1000" + ], + "next_log": [ + "3393/500", + "6787/1000" + ], + "gate": 22 + }, + { + "p": 37, + "K": 1, + "C": 2, + "maximum": 35, + "success_log": [ + "-13331/1000", + "-1333/100" + ], + "next_log": [ + "11403/500", + "22807/1000" + ], + "gate": 20 + }, + { + "p": 37, + "K": 7, + "C": 3, + "maximum": 28, + "success_log": [ + "-2334/125", + "-18671/1000" + ], + "next_log": [ + "2184/125", + "17473/1000" + ], + "gate": 12 + }, + { + "p": 38, + "K": 0, + "C": 0, + "maximum": 39, + "success_log": [ + "-10839/500", + "-21677/1000" + ], + "next_log": [ + "14723/1000", + "3681/250" + ], + "gate": 23 + }, + { + "p": 38, + "K": 1, + "C": 2, + "maximum": 37, + "success_log": [ + "-951/250", + "-3803/1000" + ], + "next_log": [ + "32599/1000", + "163/5" + ], + "gate": 21 + }, + { + "p": 38, + "K": 7, + "C": 3, + "maximum": 30, + "success_log": [ + "-861/200", + "-538/125" + ], + "next_log": [ + "4013/125", + "6421/200" + ], + "gate": 13 + }, + { + "p": 39, + "K": 0, + "C": 0, + "maximum": 41, + "success_log": [ + "-15227/1000", + "-7613/500" + ], + "next_log": [ + "21433/1000", + "10717/500" + ], + "gate": 25 + }, + { + "p": 39, + "K": 1, + "C": 2, + "maximum": 38, + "success_log": [ + "-4018/125", + "-32143/1000" + ], + "next_log": [ + "2259/500", + "4519/1000" + ], + "gate": 22 + }, + { + "p": 39, + "K": 7, + "C": 3, + "maximum": 31, + "success_log": [ + "-6941/250", + "-27763/1000" + ], + "next_log": [ + "8903/1000", + "1113/125" + ], + "gate": 14 + }, + { + "p": 40, + "K": 0, + "C": 0, + "maximum": 43, + "success_log": [ + "-10021/1000", + "-501/50" + ], + "next_log": [ + "26891/1000", + "6723/250" + ], + "gate": 26 + }, + { + "p": 40, + "K": 1, + "C": 2, + "maximum": 40, + "success_log": [ + "-6327/250", + "-25307/1000" + ], + "next_log": [ + "2321/200", + "5803/500" + ], + "gate": 23 + }, + { + "p": 40, + "K": 7, + "C": 3, + "maximum": 33, + "success_log": [ + "-3999/250", + "-3199/200" + ], + "next_log": [ + "20923/1000", + "5231/250" + ], + "gate": 15 + }, + { + "p": 41, + "K": 0, + "C": 0, + "maximum": 45, + "success_log": [ + "-3043/500", + "-1217/200" + ], + "next_log": [ + "31071/1000", + "3884/125" + ], + "gate": 27 + }, + { + "p": 41, + "K": 1, + "C": 2, + "maximum": 42, + "success_log": [ + "-4931/250", + "-19723/1000" + ], + "next_log": [ + "3487/200", + "4359/250" + ], + "gate": 25 + }, + { + "p": 41, + "K": 7, + "C": 3, + "maximum": 35, + "success_log": [ + "-2719/500", + "-5437/1000" + ], + "next_log": [ + "15863/500", + "31727/1000" + ], + "gate": 16 + }, + { + "p": 42, + "K": 0, + "C": 0, + "maximum": 47, + "success_log": [ + "-1723/500", + "-689/200" + ], + "next_log": [ + "4244/125", + "33953/1000" + ], + "gate": 29 + }, + { + "p": 42, + "K": 1, + "C": 2, + "maximum": 44, + "success_log": [ + "-15417/1000", + "-1927/125" + ], + "next_log": [ + "10991/500", + "21983/1000" + ], + "gate": 26 + }, + { + "p": 42, + "K": 7, + "C": 3, + "maximum": 36, + "success_log": [ + "-33519/1000", + "-16759/500" + ], + "next_log": [ + "777/200", + "1943/500" + ], + "gate": 17 + }, + { + "p": 43, + "K": 0, + "C": 0, + "maximum": 49, + "success_log": [ + "-2121/1000", + "-53/25" + ], + "next_log": [ + "4439/125", + "35513/1000" + ], + "gate": 30 + }, + { + "p": 43, + "K": 1, + "C": 2, + "maximum": 46, + "success_log": [ + "-12409/1000", + "-1551/125" + ], + "next_log": [ + "3153/125", + "1009/40" + ], + "gate": 27 + }, + { + "p": 43, + "K": 7, + "C": 3, + "maximum": 38, + "success_log": [ + "-25691/1000", + "-2569/100" + ], + "next_log": [ + "11947/1000", + "2987/250" + ], + "gate": 18 + }, + { + "p": 44, + "K": 0, + "C": 0, + "maximum": 51, + "success_log": [ + "-533/250", + "-2131/1000" + ], + "next_log": [ + "35729/1000", + "3573/100" + ], + "gate": 32 + }, + { + "p": 44, + "K": 1, + "C": 2, + "maximum": 48, + "success_log": [ + "-10721/1000", + "-268/25" + ], + "next_log": [ + "27141/1000", + "13571/500" + ], + "gate": 29 + }, + { + "p": 44, + "K": 7, + "C": 3, + "maximum": 40, + "success_log": [ + "-957/50", + "-19139/1000" + ], + "next_log": [ + "9363/500", + "18727/1000" + ], + "gate": 19 + }, + { + "p": 45, + "K": 0, + "C": 0, + "maximum": 53, + "success_log": [ + "-3499/1000", + "-1749/500" + ], + "next_log": [ + "17293/500", + "34587/1000" + ], + "gate": 33 + }, + { + "p": 45, + "K": 1, + "C": 2, + "maximum": 50, + "success_log": [ + "-5187/500", + "-10373/1000" + ], + "next_log": [ + "3464/125", + "27713/1000" + ], + "gate": 30 + }, + { + "p": 45, + "K": 7, + "C": 3, + "maximum": 42, + "success_log": [ + "-1389/100", + "-13889/1000" + ], + "next_log": [ + "121/5", + "24201/1000" + ], + "gate": 20 + }, + { + "p": 46, + "K": 0, + "C": 0, + "maximum": 55, + "success_log": [ + "-156/25", + "-6239/1000" + ], + "next_log": [ + "4008/125", + "6413/200" + ], + "gate": 35 + }, + { + "p": 46, + "K": 1, + "C": 2, + "maximum": 52, + "success_log": [ + "-5693/500", + "-2277/200" + ], + "next_log": [ + "26919/1000", + "673/25" + ], + "gate": 31 + }, + { + "p": 46, + "K": 7, + "C": 3, + "maximum": 44, + "success_log": [ + "-249/25", + "-9959/1000" + ], + "next_log": [ + "28349/1000", + "567/20" + ], + "gate": 22 + }, + { + "p": 47, + "K": 0, + "C": 0, + "maximum": 57, + "success_log": [ + "-10373/1000", + "-2593/250" + ], + "next_log": [ + "14073/500", + "28147/1000" + ], + "gate": 36 + }, + { + "p": 47, + "K": 1, + "C": 2, + "maximum": 54, + "success_log": [ + "-1722/125", + "-551/40" + ], + "next_log": [ + "3093/125", + "4949/200" + ], + "gate": 33 + }, + { + "p": 47, + "K": 7, + "C": 3, + "maximum": 46, + "success_log": [ + "-737/100", + "-7369/1000" + ], + "next_log": [ + "31153/1000", + "15577/500" + ], + "gate": 23 + }, + { + "p": 48, + "K": 0, + "C": 0, + "maximum": 59, + "success_log": [ + "-7957/500", + "-15913/1000" + ], + "next_log": [ + "11407/500", + "4563/200" + ], + "gate": 38 + }, + { + "p": 48, + "K": 1, + "C": 2, + "maximum": 56, + "success_log": [ + "-439/25", + "-17559/1000" + ], + "next_log": [ + "21169/1000", + "2117/100" + ], + "gate": 34 + }, + { + "p": 48, + "K": 7, + "C": 3, + "maximum": 48, + "success_log": [ + "-307/50", + "-6139/1000" + ], + "next_log": [ + "32593/1000", + "16297/500" + ], + "gate": 24 + }, + { + "p": 49, + "K": 0, + "C": 0, + "maximum": 61, + "success_log": [ + "-22879/1000", + "-11439/500" + ], + "next_log": [ + "3211/200", + "2007/125" + ], + "gate": 39 + }, + { + "p": 49, + "K": 1, + "C": 2, + "maximum": 58, + "success_log": [ + "-5689/250", + "-4551/200" + ], + "next_log": [ + "16179/1000", + "809/50" + ], + "gate": 36 + }, + { + "p": 49, + "K": 7, + "C": 3, + "maximum": 50, + "success_log": [ + "-3143/500", + "-1257/200" + ], + "next_log": [ + "8163/250", + "32653/1000" + ], + "gate": 25 + }, + { + "p": 50, + "K": 0, + "C": 0, + "maximum": 63, + "success_log": [ + "-31283/1000", + "-15641/500" + ], + "next_log": [ + "7853/1000", + "3927/500" + ], + "gate": 41 + }, + { + "p": 50, + "K": 1, + "C": 2, + "maximum": 60, + "success_log": [ + "-14689/500", + "-29377/1000" + ], + "next_log": [ + "9759/1000", + "244/25" + ], + "gate": 38 + }, + { + "p": 50, + "K": 7, + "C": 3, + "maximum": 52, + "success_log": [ + "-313/40", + "-978/125" + ], + "next_log": [ + "15657/500", + "6263/200" + ], + "gate": 27 + }, + { + "p": 51, + "K": 0, + "C": 0, + "maximum": 66, + "success_log": [ + "-903/500", + "-361/200" + ], + "next_log": [ + "37527/1000", + "4691/125" + ], + "gate": 43 + }, + { + "p": 51, + "K": 1, + "C": 2, + "maximum": 62, + "success_log": [ + "-936/25", + "-37439/1000" + ], + "next_log": [ + "947/500", + "379/200" + ], + "gate": 39 + }, + { + "p": 51, + "K": 7, + "C": 3, + "maximum": 54, + "success_log": [ + "-5387/500", + "-10773/1000" + ], + "next_log": [ + "14281/500", + "28563/1000" + ], + "gate": 28 + }, + { + "p": 52, + "K": 0, + "C": 0, + "maximum": 68, + "success_log": [ + "-2587/200", + "-6467/500" + ], + "next_log": [ + "3324/125", + "26593/1000" + ], + "gate": 44 + }, + { + "p": 52, + "K": 1, + "C": 2, + "maximum": 65, + "success_log": [ + "-743/100", + "-7429/1000" + ], + "next_log": [ + "32097/1000", + "16049/500" + ], + "gate": 41 + }, + { + "p": 52, + "K": 7, + "C": 3, + "maximum": 56, + "success_log": [ + "-3787/250", + "-15147/1000" + ], + "next_log": [ + "12191/500", + "24383/1000" + ], + "gate": 30 + }, + { + "p": 53, + "K": 0, + "C": 0, + "maximum": 70, + "success_log": [ + "-6387/250", + "-25547/1000" + ], + "next_log": [ + "14169/1000", + "1417/100" + ], + "gate": 46 + }, + { + "p": 53, + "K": 1, + "C": 2, + "maximum": 67, + "success_log": [ + "-18227/1000", + "-9113/500" + ], + "next_log": [ + "21491/1000", + "5373/250" + ], + "gate": 43 + }, + { + "p": 53, + "K": 7, + "C": 3, + "maximum": 58, + "success_log": [ + "-524/25", + "-20959/1000" + ], + "next_log": [ + "469/25", + "18761/1000" + ], + "gate": 31 + }, + { + "p": 54, + "K": 0, + "C": 0, + "maximum": 72, + "success_log": [ + "-7931/200", + "-19827/500" + ], + "next_log": [ + "31/125", + "249/1000" + ], + "gate": 48 + }, + { + "p": 54, + "K": 1, + "C": 2, + "maximum": 69, + "success_log": [ + "-7627/250", + "-30507/1000" + ], + "next_log": [ + "9397/1000", + "4699/500" + ], + "gate": 44 + }, + { + "p": 54, + "K": 7, + "C": 3, + "maximum": 60, + "success_log": [ + "-14113/500", + "-1129/40" + ], + "next_log": [ + "292/25", + "11681/1000" + ], + "gate": 33 + }, + { + "p": 55, + "K": 0, + "C": 0, + "maximum": 75, + "success_log": [ + "-15183/1000", + "-7591/500" + ], + "next_log": [ + "24903/1000", + "3113/125" + ], + "gate": 50 + }, + { + "p": 55, + "K": 1, + "C": 2, + "maximum": 72, + "success_log": [ + "-2099/500", + "-4197/1000" + ], + "next_log": [ + "35889/1000", + "3589/100" + ], + "gate": 46 + }, + { + "p": 55, + "K": 7, + "C": 3, + "maximum": 62, + "success_log": [ + "-18479/500", + "-36957/1000" + ], + "next_log": [ + "783/250", + "3133/1000" + ], + "gate": 34 + }, + { + "p": 56, + "K": 0, + "C": 0, + "maximum": 77, + "success_log": [ + "-4017/125", + "-6427/200" + ], + "next_log": [ + "8131/1000", + "2033/250" + ], + "gate": 52 + }, + { + "p": 56, + "K": 1, + "C": 2, + "maximum": 74, + "success_log": [ + "-2413/125", + "-19303/1000" + ], + "next_log": [ + "20963/1000", + "5241/250" + ], + "gate": 48 + }, + { + "p": 56, + "K": 7, + "C": 3, + "maximum": 65, + "success_log": [ + "-6899/1000", + "-3449/500" + ], + "next_log": [ + "3337/100", + "33371/1000" + ], + "gate": 36 + }, + { + "p": 57, + "K": 0, + "C": 0, + "maximum": 80, + "success_log": [ + "-10177/1000", + "-1272/125" + ], + "next_log": [ + "6053/200", + "15133/500" + ], + "gate": 53 + }, + { + "p": 57, + "K": 1, + "C": 2, + "maximum": 76, + "success_log": [ + "-8983/250", + "-35931/1000" + ], + "next_log": [ + "564/125", + "4513/1000" + ], + "gate": 50 + }, + { + "p": 57, + "K": 7, + "C": 3, + "maximum": 67, + "success_log": [ + "-18423/1000", + "-9211/500" + ], + "next_log": [ + "11011/500", + "22023/1000" + ], + "gate": 37 + }, + { + "p": 58, + "K": 0, + "C": 0, + "maximum": 82, + "success_log": [ + "-30031/1000", + "-3003/100" + ], + "next_log": [ + "5293/500", + "10587/1000" + ], + "gate": 55 + }, + { + "p": 58, + "K": 1, + "C": 2, + "maximum": 79, + "success_log": [ + "-3369/250", + "-539/40" + ], + "next_log": [ + "27141/1000", + "13571/500" + ], + "gate": 51 + }, + { + "p": 58, + "K": 7, + "C": 3, + "maximum": 69, + "success_log": [ + "-31453/1000", + "-7863/250" + ], + "next_log": [ + "4583/500", + "9167/1000" + ], + "gate": 39 + }, + { + "p": 59, + "K": 0, + "C": 0, + "maximum": 85, + "success_log": [ + "-10651/1000", + "-213/20" + ], + "next_log": [ + "3767/125", + "30137/1000" + ], + "gate": 57 + }, + { + "p": 59, + "K": 1, + "C": 2, + "maximum": 81, + "success_log": [ + "-33009/1000", + "-4126/125" + ], + "next_log": [ + "3889/500", + "7779/1000" + ], + "gate": 53 + }, + { + "p": 59, + "K": 7, + "C": 3, + "maximum": 72, + "success_log": [ + "-521/100", + "-5209/1000" + ], + "next_log": [ + "35579/1000", + "1779/50" + ], + "gate": 41 + }, + { + "p": 60, + "K": 0, + "C": 0, + "maximum": 87, + "success_log": [ + "-6691/200", + "-16727/500" + ], + "next_log": [ + "15/2", + "7501/1000" + ], + "gate": 59 + }, + { + "p": 60, + "K": 1, + "C": 2, + "maximum": 84, + "success_log": [ + "-13143/1000", + "-6571/500" + ], + "next_log": [ + "27813/1000", + "13907/500" + ], + "gate": 55 + }, + { + "p": 60, + "K": 7, + "C": 3, + "maximum": 74, + "success_log": [ + "-4223/200", + "-10557/500" + ], + "next_log": [ + "9921/500", + "19843/1000" + ], + "gate": 42 + }, + { + "p": 61, + "K": 0, + "C": 0, + "maximum": 90, + "success_log": [ + "-8357/500", + "-16713/1000" + ], + "next_log": [ + "12203/500", + "24407/1000" + ], + "gate": 61 + }, + { + "p": 61, + "K": 1, + "C": 2, + "maximum": 86, + "success_log": [ + "-35631/1000", + "-3563/100" + ], + "next_log": [ + "549/100", + "5491/1000" + ], + "gate": 57 + }, + { + "p": 61, + "K": 7, + "C": 3, + "maximum": 76, + "success_log": [ + "-964/25", + "-38559/1000" + ], + "next_log": [ + "1281/500", + "2563/1000" + ], + "gate": 44 + }, + { + "p": 62, + "K": 0, + "C": 0, + "maximum": 93, + "success_log": [ + "-1233/1000", + "-154/125" + ], + "next_log": [ + "40049/1000", + "801/20" + ], + "gate": 63 + }, + { + "p": 62, + "K": 1, + "C": 2, + "maximum": 89, + "success_log": [ + "-4603/250", + "-18411/1000" + ], + "next_log": [ + "22871/1000", + "2859/125" + ], + "gate": 59 + }, + { + "p": 62, + "K": 7, + "C": 3, + "maximum": 79, + "success_log": [ + "-1627/100", + "-16269/1000" + ], + "next_log": [ + "12507/500", + "5003/200" + ], + "gate": 46 + }, + { + "p": 63, + "K": 0, + "C": 0, + "maximum": 95, + "success_log": [ + "-28469/1000", + "-7117/250" + ], + "next_log": [ + "12973/1000", + "6487/500" + ], + "gate": 65 + }, + { + "p": 63, + "K": 1, + "C": 2, + "maximum": 92, + "success_log": [ + "-1229/500", + "-2457/1000" + ], + "next_log": [ + "4873/125", + "7797/200" + ], + "gate": 61 + }, + { + "p": 63, + "K": 7, + "C": 3, + "maximum": 81, + "success_log": [ + "-18331/500", + "-36661/1000" + ], + "next_log": [ + "2391/500", + "4783/1000" + ], + "gate": 48 + }, + { + "p": 64, + "K": 0, + "C": 0, + "maximum": 98, + "success_log": [ + "-1571/100", + "-15709/1000" + ], + "next_log": [ + "25889/1000", + "2589/100" + ], + "gate": 68 + }, + { + "p": 64, + "K": 1, + "C": 2, + "maximum": 94, + "success_log": [ + "-3673/125", + "-29383/1000" + ], + "next_log": [ + "2443/200", + "1527/125" + ], + "gate": 63 + }, + { + "p": 64, + "K": 7, + "C": 3, + "maximum": 84, + "success_log": [ + "-2128/125", + "-17023/1000" + ], + "next_log": [ + "24577/1000", + "12289/500" + ], + "gate": 49 + }, + { + "p": 84, + "K": 0, + "C": 0, + "maximum": 159, + "success_log": [ + "-5933/1000", + "-1483/250" + ], + "next_log": [ + "19191/500", + "38383/1000" + ], + "gate": 100 + }, + { + "p": 84, + "K": 1, + "C": 2, + "maximum": 154, + "success_log": [ + "-27057/1000", + "-3382/125" + ], + "next_log": [ + "8629/500", + "17259/1000" + ], + "gate": 95 + }, + { + "p": 84, + "K": 7, + "C": 3, + "maximum": 141, + "success_log": [ + "-40927/1000", + "-20463/500" + ], + "next_log": [ + "847/250", + "3389/1000" + ], + "gate": 80 + }, + { + "p": 128, + "K": 0, + "C": 0, + "maximum": 337, + "success_log": [ + "-13419/500", + "-26837/1000" + ], + "next_log": [ + "4337/200", + "10843/500" + ], + "gate": 233 + }, + { + "p": 128, + "K": 1, + "C": 2, + "maximum": 331, + "success_log": [ + "-12533/1000", + "-3133/250" + ], + "next_log": [ + "35991/1000", + "4499/125" + ], + "gate": 226 + }, + { + "p": 128, + "K": 7, + "C": 3, + "maximum": 313, + "success_log": [ + "-29231/1000", + "-2923/100" + ], + "next_log": [ + "4823/250", + "19293/1000" + ], + "gate": 202 + }, + { + "p": 256, + "K": 0, + "C": 0, + "maximum": 1181, + "success_log": [ + "-40381/1000", + "-2019/50" + ], + "next_log": [ + "1884/125", + "15073/1000" + ], + "gate": 818 + }, + { + "p": 256, + "K": 1, + "C": 2, + "maximum": 1170, + "success_log": [ + "-9867/250", + "-39467/1000" + ], + "next_log": [ + "1998/125", + "3197/200" + ], + "gate": 806 + }, + { + "p": 256, + "K": 7, + "C": 3, + "maximum": 1139, + "success_log": [ + "-22527/500", + "-45053/1000" + ], + "next_log": [ + "5199/500", + "10399/1000" + ], + "gate": 764 + }, + { + "p": 1024, + "K": 0, + "C": 0, + "maximum": 15127, + "success_log": [ + "-10659/250", + "-8527/200" + ], + "next_log": [ + "26679/1000", + "667/25" + ], + "gate": 10485 + }, + { + "p": 1024, + "K": 1, + "C": 2, + "maximum": 15092, + "success_log": [ + "-3136/125", + "-25087/1000" + ], + "next_log": [ + "44227/1000", + "11057/250" + ], + "gate": 10444 + }, + { + "p": 1024, + "K": 7, + "C": 3, + "maximum": 14993, + "success_log": [ + "-33469/1000", + "-8367/250" + ], + "next_log": [ + "17923/500", + "35847/1000" + ], + "gate": 10311 + }, + { + "p": 4096, + "K": 0, + "C": 0, + "maximum": 201703, + "success_log": [ + "-3979/200", + "-9947/500" + ], + "next_log": [ + "63283/1000", + "15821/250" + ], + "gate": 139809 + }, + { + "p": 4096, + "K": 1, + "C": 2, + "maximum": 201585, + "success_log": [ + "-30299/500", + "-60597/1000" + ], + "next_log": [ + "1129/50", + "22581/1000" + ], + "gate": 139673 + }, + { + "p": 4096, + "K": 7, + "C": 3, + "maximum": 201256, + "success_log": [ + "-10919/1000", + "-5459/500" + ], + "next_log": [ + "72259/1000", + "3613/50" + ], + "gate": 139229 + }, + { + "p": 65536, + "K": 0, + "C": 0, + "maximum": 38727049, + "success_log": [ + "-106407/1000", + "-53203/500" + ], + "next_log": [ + "562/125", + "4497/1000" + ], + "gate": 26843545 + }, + { + "p": 65536, + "K": 1, + "C": 2, + "maximum": 38725639, + "success_log": [ + "-11528/125", + "-92223/1000" + ], + "next_log": [ + "18679/1000", + "467/25" + ], + "gate": 26841906 + }, + { + "p": 65536, + "K": 7, + "C": 3, + "maximum": 38721684, + "success_log": [ + "-36833/500", + "-14733/200" + ], + "next_log": [ + "37237/1000", + "18619/500" + ], + "gate": 26836582 + } + ] +} diff --git a/research/heavy-tensor-dimension/SOURCES.json b/research/heavy-tensor-dimension/SOURCES.json new file mode 100644 index 0000000000..32ffdd89ec --- /dev/null +++ b/research/heavy-tensor-dimension/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/gaussian-heavy-slice/README.md", + "usage": "input", + "git_blob": "33144f496057f74cd090d3727e4327aa43f06806", + "sha256": "42feda423dd82675b5de0917425941b99c203d257915ad7855ceb2af86c48ad6" + }, + { + "path": "research/gaussian-slice-one-copies/README.md", + "usage": "input", + "git_blob": "d0a454f597fc62b947afffcfa0fd4fe84d474915", + "sha256": "f6b584cab7a948775bdeae9e3708443e29c70224c51484eff49cdc1de6e8d73e" + } + ] +} diff --git a/research/heavy-tensor-dimension/TASK.json b/research/heavy-tensor-dimension/TASK.json new file mode 100644 index 0000000000..aa0d23a7c0 --- /dev/null +++ b/research/heavy-tensor-dimension/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the sharp quadratic dimension scale and exact monotone boundary of the heavy tensor-error envelope; certify p=64 maximum 98.", + "scope_change_reason": "The donor requests original research rather than predecessor audit. Extend James Reed's sufficient dimension gate with a new sharp scalar threshold theorem.", + "bottleneck_link": "Side result: separates the scalar error limitation from stricter header, storage and physical-caller obligations; does not admit a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved threshold improvement and exact bounded corroboration.", + "outcome": "completed", + "evidence": "README.md written all-p proof; verify.py exact rational logarithm intervals and independent rational e-power boundary controls; generated source-bound RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which actual caller restriction first blocks quadratic-scale dimensions?", + "why_it_matters": "A wider scalar error gate need not relax physical admissibility.", + "first_step": "Pin one caller and its header-size and storage inequalities.", + "blocked_by": "No physical contract at the larger dimension is supplied." + }, + { + "question": "Can actual unequal per-axis norm ceilings beat the worst-slice envelope?", + "why_it_matters": "The maximum trailing ceiling can be pessimistic.", + "first_step": "Pin a concrete ordered list of per-axis norm and error bounds.", + "blocked_by": "Caller-specific bounds are absent." + } + ], + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "implementation": "CPython", + "version": "3.12.15" + }, + "claim_type": "scoped proof with exact finite corroboration", + "overlap_coverage": { + "base": "624de9dc66858af0945e5f8a0942488d62280d43", + "open_prs": 426, + "discussion_records": 3959, + "remote_snapshot_utc": "2026-10-22T23:35:48Z", + "local_notes_incomplete": true, + "limits": "Searches cover titles, bodies, discussion comments and main READMEs, not arbitrary diffs or unpublished work.", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134562" + } +} diff --git a/research/heavy-tensor-dimension/VERIFY.json b/research/heavy-tensor-dimension/VERIFY.json new file mode 100644 index 0000000000..15f8ff1d7c --- /dev/null +++ b/research/heavy-tensor-dimension/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/gaussian-heavy-slice/README.md", + "research/gaussian-slice-one-copies/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact neighboring threshold signs, integer gate, independent e-power comparisons, input and corruption controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Identical checks with Python assertions disabled." + } + ] +} diff --git a/research/heavy-tensor-dimension/verify.py b/research/heavy-tensor-dimension/verify.py new file mode 100644 index 0000000000..13dccce214 --- /dev/null +++ b/research/heavy-tensor-dimension/verify.py @@ -0,0 +1,242 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration of the heavy tensor dimension theorem.""" +from __future__ import annotations + +import argparse +import hashlib +import json +from fractions import Fraction as Q +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +MAX_BYTES = 2 * 1024 * 1024 +MAX_P = 2**20 +SERIES_TERMS = 32 +LOCAL_SOURCES = ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def integer(value: int, low: int, high: int) -> None: + require(type(value) is int and low <= value <= high, 'integer outside bounds') + + +def read_bytes(path: Path) -> bytes: + require(path.stat().st_size <= MAX_BYTES, 'file exceeds resource bound') + data = path.read_bytes() + require(len(data) <= MAX_BYTES, 'file grew beyond resource bound') + return data + + +def ln_unit(x: Q, terms: int = SERIES_TERMS) -> tuple[Q, Q]: + require(type(x) is Q and 1 <= x <= 2, 'logarithm range reduction failed') + integer(terms, 1, 64) + z = (x - 1) / (x + 1) + power = z + total = Q(0) + for j in range(terms): + total += 2 * power / (2 * j + 1) + power *= z * z + tail = 2 * power / ((2 * terms + 1) * (1 - z * z)) + require(0 <= tail, 'negative logarithm tail') + return total, total + tail + + +def ln_integer(n: int, terms: int = SERIES_TERMS) -> tuple[Q, Q]: + integer(n, 1, 2**41) + k = n.bit_length() - 1 + low, high = ln_unit(Q(n, 2**k), terms) + two_low, two_high = ln_unit(Q(2), terms) + return low + k * two_low, high + k * two_high + + +def log_budget(p: int, g: int, k: int, c: int) -> tuple[Q, Q]: + integer(p, 2, MAX_P) + integer(g, 1, p * p + 1) + integer(k, 0, MAX_P) + integer(c, 0, MAX_P) + gl, gu = ln_integer(g) + pl, pu = ln_integer(p) + tl, tu = ln_unit(1 + Q(1, p**4)) + bl, bu = ln_integer(2) + constant = k * p - p * p + low = gl + 10 * g * pl + tl + c * p * bl + constant + high = gu + 10 * g * pu + tu + c * p * bu + constant + require(low <= high, 'inverted logarithm interval') + return low, high + + +def budget_sign(p: int, g: int, k: int, c: int) -> int: + low, high = log_budget(p, g, k, c) + if high < 0: + return -1 + if low > 0: + return 1 + raise ValueError('logarithm interval does not decide strict sign') + + +def last_dimension(p: int, k: int, c: int) -> int: + integer(p, 2, MAX_P) + integer(k, 0, MAX_P) + integer(c, 0, MAX_P) + low, high = 0, p * p + 1 + require(budget_sign(p, high, k, c) == 1, 'upper bracket failed') + for _ in range(42): + if high - low == 1: + return low + mid = (low + high) // 2 + if budget_sign(p, mid, k, c) < 0: + low = mid + else: + high = mid + raise ValueError('bounded dimension search exhausted') + + +def gate_dimension(p: int, k: int, c: int) -> int: + integer(p, 2, MAX_P) + integer(k, 0, MAX_P) + integer(c, 0, MAX_P) + level = (p - 1).bit_length() + numerator = p * p - 2 * level - 1 - (2 * k + c) * p + return max(0, numerator // (10 * level)) + + +def exp_one_bounds() -> tuple[Q, Q]: + total = Q(1) + term = Q(1) + for n in range(1, 13): + term /= n + total += term + first_omitted = term / 13 + return total, total + first_omitted * Q(14, 13) + + +def direct_power_sign(p: int, g: int) -> int: + integer(p, 2, 64) + integer(g, 1, p * p + 1) + low, high = exp_one_bounds() + envelope = g * p ** (10 * g) * (1 + Q(1, p**4)) + if envelope < low ** (p * p): + return -1 + if envelope > high ** (p * p): + return 1 + raise ValueError('independent e-power interval undecided') + + +def rounded_interval(p: int, g: int, k: int, c: int) -> list[str]: + low, high = log_budget(p, g, k, c) + return [str(Q((1000 * low).__floor__(), 1000)), + str(Q((1000 * high).__ceil__(), 1000))] + + +def boundary_cases() -> tuple[list[dict], int]: + rows = [] + gate_checks = 0 + dimensions = tuple(range(2, 65)) + (84, 128, 256, 1024, 4096, 65536) + for p in dimensions: + for k, c in ((0, 0), (1, 2), (7, 3)): + last = last_dimension(p, k, c) + success = rounded_interval(p, last, k, c) if last else None + failure = rounded_interval(p, last + 1, k, c) + require(Q(failure[0]) > 0, 'failure not certified') + if success is not None: + require(Q(success[1]) < 0, 'success not certified') + gate = gate_dimension(p, k, c) + require(gate <= last, 'integer gate exceeded exact boundary') + if gate: + require(budget_sign(p, gate, k, c) < 0, 'integer gate fails') + gate_checks += 1 + rows.append(dict(p=p, K=k, C=c, maximum=last, + success_log=success, next_log=failure, gate=gate)) + return rows, gate_checks + + +def semantic_controls() -> int: + rejected = 0 + cases = ((1, 1, 0, 0), (True, 1, 0, 0), (2, 0, 0, 0), + (2, 6, 0, 0), (2, 1, -1, 0), (2, 1, 0, -1), + (MAX_P + 1, 1, 0, 0), (2, 1, 0, MAX_P + 1)) + for args in cases: + try: + log_budget(*args) + except ValueError: + rejected += 1 + require(rejected == len(cases), 'invalid input accepted') + for x, terms in ((Q(3), 32), (Q(0), 32), (Q(2), 0), (Q(2), 65)): + try: + ln_unit(x, terms) + except ValueError: + rejected += 1 + require(rejected == 12, 'invalid series contract accepted') + low, high = ln_integer(2) + require(Q(69, 100) < low <= high < Q(7, 10), 'log base control failed') + require(ln_integer(1) == (0, 0), 'log identity failed') + require(gate_dimension(64, 0, 0) == 68, 'integer gate transcription') + require(log_budget(64, 98, 0, 0)[1] < -15, 'success margin failed') + require(log_budget(64, 99, 0, 0)[0] > 25, 'failure margin failed') + return rejected + 5 + + +def source_hashes() -> dict[str, str]: + hashes = {name: hashlib.sha256(read_bytes(PACKAGE / name)).hexdigest() + for name in LOCAL_SOURCES} + manifest = json.loads(read_bytes(PACKAGE / 'SOURCES.json')) + require(len(manifest['files']) <= 100, 'source row bound exceeded') + for row in manifest['files']: + if row['usage'] == 'input': + data = read_bytes(ROOT / row['path']) + digest = hashlib.sha256(data).hexdigest() + require(digest == row['sha256'], 'live predecessor source changed') + hashes[row['path']] = digest + return hashes + + +def result() -> dict: + hashes = source_hashes() + controls = semantic_controls() + rows, gates = boundary_cases() + powers = 0 + for p in (2, 4, 8, 16, 32, 64): + last = last_dimension(p, 0, 0) + if last: + require(direct_power_sign(p, last) == -1, 'direct success mismatch') + powers += 1 + require(direct_power_sign(p, last + 1) == 1, 'direct failure mismatch') + powers += 1 + selected = next(row for row in rows if (row['p'], row['K'], row['C']) == (64, 0, 0)) + require(selected['maximum'] == 98, 'first fixture maximum changed') + return dict(schema_version=1, status='PASS_HEAVY_TENSOR_DIMENSION', + source_sha256=hashes, series_terms=SERIES_TERMS, + boundary_cases=len(rows), integer_gate_checks=gates, + independent_power_comparisons=powers, semantic_controls=controls, + boundaries=rows) + + +def canonical(value: object) -> str: + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-receipt', type=Path) + args = parser.parse_args() + actual = result() + if args.write_receipt is not None: + with args.write_receipt.open('x', encoding='utf-8') as out: + out.write(json.dumps(actual, indent=2) + '\n') + else: + expected = json.loads(read_bytes(PACKAGE / 'RESULT.json')) + require(canonical(expected) == canonical(actual), 'source-bound receipt mismatch') + print('PASS_HEAVY_TENSOR_DIMENSION', + f"boundaries={actual['boundary_cases']}", + f"gates={actual['integer_gate_checks']}", + f"power_comparisons={actual['independent_power_comparisons']}", + f"controls={actual['semantic_controls']}") + + +if __name__ == '__main__': + main()