diff --git a/research/log-potential-template-ranks/.gitattributes b/research/log-potential-template-ranks/.gitattributes new file mode 100644 index 0000000000..2435bfdf63 --- /dev/null +++ b/research/log-potential-template-ranks/.gitattributes @@ -0,0 +1 @@ +vendor/** -text -whitespace diff --git a/research/log-potential-template-ranks/README.md b/research/log-potential-template-ranks/README.md new file mode 100644 index 0000000000..641d00f3d4 --- /dev/null +++ b/research/log-potential-template-ranks/README.md @@ -0,0 +1,396 @@ +# Smaller sufficient ranks for the conditional κ = 0.0023 compiler + +The finite source/exit compiler of [PR4359](https://github.com/CrocSwap/integer-mult-bounds/pull/4359) +admits the same proposed uniform savings at much smaller specified ambient +ranks. Replace the intermediate power majorant by + +\[ +L(n)\le n^t(1+\log_2 n)^{1/q},\qquad L(n)=P_n/B_n. +\] + +Together with a compatible outer parameter retuning, this gives sufficient +ranks **`2^465000` (complex)** and **`2^7100` (BIT before cover)** while retaining +the proposed **κ = 0.0023**. The exact outer ledger passes all nine cost rows, +all 63 inherited arithmetic predicates, and 22 additional interface inequalities. +The retuning spends supplier saving that the κ target does not need. + +There are two useful configurations. First, preserve the original supplier +savings, invoices, tested mixed exponents and native hypotheses: + +| Family | Original sufficient rank | New sufficient rank | Reduction in exponent of 2 | Uniform saving | +| --- | ---: | ---: | ---: | ---: | +| Complex | `2^276540184361` | **`2^2352000`** | about 117,577× | 0.002304 | +| BIT, before delayed cover | `2^6552928412` | **`2^529000`** | about 12,387× | 0.002760 | + +Second, retain κ = 0.0023 with weaker supplier savings and retuned outer parameters: + +| Family | Sufficient rank | Uniform saving | Consumer condition | +| --- | ---: | ---: | --- | +| Complex | **`2^465000`** | 0.0023005 | Above outer `b=0.0023004` | +| BIT, before delayed cover | **`2^7100`** | 0.002318 | Cover/atom conversion gives ordinary saving 0.0023011913797 | + +The original rank exponents decrease by about 594,710× and 922,948× in this +second configuration. The two rows of each configuration belong together; +the weaker savings are not substituted into the predecessor's original +outer parameter point. + +These ranks remain astronomical. This is a written conditional proof with +author-checked exact arithmetic. It does not emit the winning words, bound +their complete constants, independently admit the compiler/native/outer +transfer, or claim a new κ. In particular, it does not assert that the +productive width `B_N`, scalar word or precision constants improve by the +same factors. No selected-result record or predecessor package is changed. + +## What changes in the argument + +PR4359 chooses `t < z0 < z`, pays an induction constant +`A = n0^(1-z0)`, and then makes `A*N^z0 < N^z`. Its sufficient `log2 N` +therefore loses two inverse powers of the small exponent gap. The logarithmic +majorant below has constant **one** and uses `t` directly. With fixed `q`, its +final condition is just + +\[ +1+H < 2^{q(z-t)H},\qquad N=2^H. +\] + +As `z-t` decreases, this condition needs +`H = O((z-t)^(-1) log(1/(z-t)))`. This comparison concerns the two sufficient +estimates; it is not an asymptotic formula for the compiler's smallest success. +The mixed rule, source complements, whole-array routing, integral batch +replication and owned-bank allocation are unchanged. Only the choice of the +fixed ambient rank changes. + +## Conditional logarithmic-majorant theorem + +Assume the native finite compiler in the pinned +[`FINITE-PRECOMPILATION.md`](vendor/FINITE-PRECOMPILATION.md), including its +whole-job adapters, arbitrary-input restoration and finite-program closure. +Set `m=max(k)`, `k_min=min(k)`, `r_max=max(r)`, with +`1 <= r_max < k_min <= m`. + +Use the ordinary base `L(n)=n` for `0 <= n < m`. For every integer `n >= m`, +the compiler gives finite nonnegative weights and the exact recurrence + +\[ +\begin{aligned} +L(n)&=\sum_s w_sL(n-s)+\sum_e x_eL(e), &\sum_s w_s&=1,\\ +n/m&=m` because +`r_max=1`, + +\[ +L(n)\le F(n):=n^t(1+\log_2 n)^{1/q};\qquad F(0):=0. +\tag{5} +\] + +### Base ranks + +For `n=1`, (5) is equality. For `2<=n=1`. Because `n/m>=1`, + +\[ +\begin{aligned} +1+\log_2 E(n) +&\le \bar\theta\log_2 n+1+\log_2 r_{\max}-\bar\theta\log_2 m\\ +&\le \bar\theta(1+\log_2 n), +\end{aligned} +\] + +where the last inequality is exactly (2). Thus +`C(e)<=theta_bar^(1/q)*C(n)` for every exit. By (1), + +\[ +\sum_e x_eF(e)\le +\bar\theta^{1/q}C(n)\sum_s w_s s^t. +\tag{6} +\] + +### Source complements and strong induction + +For `y=s/n` in `(1/m,1]`, concavity of `x^t` gives + +\[ +1-(1-y)^t\ge ty\ge t m^{t-1}y^t=\eta y^t. +\] + +Since `C(n-s)<=C(n)` whenever `n-s>=1`, and `F(0)=0`, + +\[ +F(n)-\sum_s w_sF(n-s) +\ge \eta C(n)\sum_s w_s s^t. +\tag{7} +\] + +Condition (3) makes the upper bound in (6) strictly smaller than the lower +bound in (7). All complement and exit ranks are below `n`. Substituting the +strong induction hypotheses into the exact recurrence proves (5). This +avoids both an intermediate exponent and an unknown multiplicative constant. + +## Two explicit choices of N + +The source histograms are copied byte-for-byte in `vendor/`, and their exact +origin is recorded in [VENDOR.json](VENDOR.json). Leaf arithmetic uses separate +code; the consumer cross-check executes the pinned outer ledger function as +described below. + +| Family | `t` | `z` | `theta_bar` | `q` | Certified `eta^q - theta_bar` lower bound | +| --- | ---: | ---: | ---: | ---: | ---: | +| Complex | 0.997695 | 0.997696 | 9/10 | 9 | 0.000646856868158037041419759048 | +| BIT | 0.997231 | 0.997240 | 15/16 | 4 | 0.009533387925024688687300943262 | + +The κ-preserving configuration uses the same `t`, `theta_bar` and `q`, with +`z=0.9976995` for complex and `z=0.997682` for BIT. + +For `N=2^H`, (5) yields `L(N) 0.002301 > a = 0.0023003. +``` + +The unchanged gap preserves the entire delayed-cover inequality: the prime +rule remains `prime > 25,600,000*N^5`, avoiding the finite denominator/rank +exclusions, and the fully charged fallback moment remains at most +`400001/400002`. Since `N>=2`, the same proof uses +`N^gap > 1+gap/2` and fallback multiplier `<1+gap/4`. The atom power remains +0.003, which exceeds the new ordinary saving; its borrowed-stock and linear +adapter inequalities remain strict. The row-stock exponent and support-local +reserve argument therefore have the same form, with constants recomputed for +the new finite words. + +For the outer recursion, `b>a>outer_q`, the stopped internal and leaf +exponents are below `lambda` and `lambda_prime`, and the complex saving is +strictly above `b`. The nine cost savings, recomputed from the pinned outer +equations, are: + +| Cost row | Saving | +| --- | ---: | +| Main transform | 0.002300176998 | +| Global coordinate router | 0.0023003 | +| Fused Gaussian | 0.002310130994 | +| Group BIT router | 0.002310230991 | +| Group scans | 0.99998 | +| Boundary algebraic matrix | 0.002301176998 | +| Sparse union movement | 0.408551176998 | +| Polynomial products | 0.99999 | +| Microbox face corrections | 77.00004 | + +Every row exceeds 0.0023. The smallest strict margin is exactly +`88499/500000000000 = 0.000000176998`. The grid/backoff calculation with +`FLOOR=10^7`, `BACKOFF=10^-7` returns exactly 0.0023. This is an ordinary +strict lower target, not a claim of maximizing the predecessor's old grid. + +The checker separately executes only the pinned `check_ledger.py` **ledger +function** and its historical comparison constants, following PR4359's AST +oracle approach. All nine rows agree exactly, and all 63 inherited predicates +remain positive. It does not run or bypass the old m=73 native admission +script. An additional 22 inequalities cover the changed supplier endpoints, +stopped recursion, cover/atom terms, semantic guards, support reserve, fine-prime +guard, explicit metadata halo and record budgets. Four outer mutations reject: +`epsilon=1`, zero layout slack, group width equal to global dimension and an +unfunded old per-axis scan. The full rational ledger and failure rows are in +`RESULT.json`. + +The native, delayed-cover, precision and support proofs are reused as stated +in the pinned [outer transfer argument](vendor/OUTER-TRANSFER-AUDIT.md). +This package checks their changed quantitative premises, not their independent +scientific acceptance. All compiled-word constants must still be replaced; +the reduced ranks do not grant the predecessor's small-template constants. + +## Reproduction and evidence + +From the repository root, with Python 3.12 or newer and no third-party packages: + +```sh +python3 -B research/log-potential-template-ranks/verify.py +python3 -B scripts/research_package.py --package research/log-potential-template-ranks --check-only +``` + +To recompute a receipt without editing the package: + +```sh +python3 -B research/log-potential-template-ranks/verify.py --out /absolute/path/to/new-result.json +``` + +The verifier authenticates all ten predecessor inputs, encloses each mixed +moment and `eta^q` with rational arithmetic, checks the integer theta/shift +tests, proves the entire base range by (4), and checks the final integer +powers. Twelve mutations must reject at the specified obligation: losing the +unit superpotential, losing strict separation, and increasing q, for each +configuration and family. Previous grid points provide four additional failing +final comparisons. The retuned consumer checks and its four controls are +described above. +`RESULT.json` contains the complete receipts. + +Logarithm bounds use the first 80 terms of `2*atanh(u)`, with binary range +reduction and the tail bound `2*u^161/(161*(1-u^2))`. Exponential bounds use +48 positive Taylor terms and the geometric upper tail beginning at term 49. +Every exponential argument is checked in `[0,1)`. Displayed decimal intervals +are rounded outwards; all decisions use exact fractions or integers. + +Local validation used Python 3.12.8 on macOS 26.5.1 arm64, with the same receipt +also generated under Python 3.14.5. The registered replay and metadata/pin check +passed. An inode-independent, Git-free copy passed `python3.12 -I -O -B verify.py` +in 8.77 seconds while another light check ran; changed-input and changed-receipt +controls both rejected. Timings are host-dependent. + +The algebraic proof above is not machine-formalized. No native circuit replay, +delayed-cover implementation replay, full multiplication theorem, Lean build, +Docker run or historical replay suite is part of this bounded quantitative change. + +## Provenance, overlap and scope + +Scientific predecessor: zxv's PR4359 head +`da637c87c89482bc4c86be36bd0071b3d400dbed`, including its finite compiler, +explicit-rank estimate, productive complex controller and delayed BIT cover. +The integer lockstep construction and Theorem 1G are Jacob Alan Sussman's +work, retained by that PR from `wht-power-saving-lean` commit +`563b4e6e913625637f36ba7869bf5fcd0dd4975a`. The original repository supplier, +PR589 BIT word and the contributor lineage recorded by PR4359 retain credit. +This package contributes the logarithmic majorant, its sufficient ranks and +the compatible outer retuning. + +The publication base is canonical main +`12fa8c5c844be21bfefb38a19503fbd867a11244`, priority revision 7. Ten immutable +inputs from the pending predecessor are included so this focused follow-up +can replay independently of whether PR4359 has merged. `SOURCES.json` pins +main's orientation metadata; `VENDOR.json` separately binds the copied inputs +to their original commit, paths, Git blobs and SHA256 hashes. This is an +offline byte binding, not an independent replay of their producers. + +The overlap refresh covered 513 open PR bodies and 3,250 discussions/comments, +with complete reported pagination at 2026-10-21 17:02 UTC, plus local package +notes and the ledger. It did not search remote closed PR bodies or every code +diff. [pinterbanget's initial claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19102222) +targeted the predecessor's recurrence and H0/H1 chain. Before submission, they +published [PR4404](https://github.com/CrocSwap/integer-mult-bounds/pull/4404), head +`77f20afb7c24286937c75cb65a7f19e24e7a567f`, reporting that the original arithmetic, +exit bound and induction hold, with separate flow simulation through rank 10,000. +That is external evidence about the predecessor, not independent review of this +new majorant or its retuned consumer. No part of PR4404's code is imported. + +The same refresh located parallel [PR4405](https://github.com/CrocSwap/integer-mult-bounds/pull/4405), +head `873d1b3c96a83b701a5c0bba8e37a861e6672fef`. It sharpens the original +power-majorant coefficient and proposes a higher conditional κ = 0.00230509. +At the original supplier savings it reports rank exponents 1,546,084,442 and +42,843,607. Our unchanged-saving exponents 2,352,000 and 529,000 improve those +sufficient estimates by a different argument. Its higher-κ parameter point is +not instantiated here, and no part of its code or proof is imported. + +## Open next questions + +1. **Sharpen the logarithmic exponent using actual source/exit distributions.** + A useful first test is a uniform bound on their complete weighted ratios, + rather than just the worst-case `eta` and `theta_bar`. This could lower H + further; another q grid by itself would add little evidence. +2. **Bound productive width and total program size.** Start with compressed + recurrences for `B_N`, `P_N`, batch denominators and owned-unit counts. + Ambient rank alone does not bound the complete constants. Integer batch + growth and the absence of a materialized winning word remain the blockers. +3. **Review the inherited compiler and native/outer transfer independently.** + Follow the existing source/exit audit, then separate the native closure, + delayed BIT cover and outer support obligations. Their acceptance remains + necessary before interpreting either set of sufficient ranks as an + admitted multiplication result. + +4. **Combine with PR4405's higher proposed κ endpoint.** Pin its exact + parameter point, choose a strict rational tested `t`, then apply (5) and + reprice the full consumer. The logarithmic majorant is general, but that + extra point and PR4405's scientific acceptance are not checked here. + +Prepared by zxv with substantial OpenAI Codex assistance. Apache-2.0. No +subagents or independent human mathematical review were used for this package. diff --git a/research/log-potential-template-ranks/RESULT.json b/research/log-potential-template-ranks/RESULT.json new file mode 100644 index 0000000000..be40a1a8b8 --- /dev/null +++ b/research/log-potential-template-ranks/RESULT.json @@ -0,0 +1,482 @@ +{ + "cases": [ + { + "N": { + "H": 2352000, + "encoding": "2^H" + }, + "base_m_to_q_saving_upper": "1.087490880883680536600217019613", + "controls": { + "previous_grid_point_fails_final_majorant": true, + "q_plus_one_fails_contraction": true + }, + "eta_to_q": { + "lower": "0.900646856868158037041419759048", + "upper": "0.900646856868158037041419759049" + }, + "eta_to_q_minus_theta": { + "lower": "0.000646856868158037041419759048", + "upper": "0.000646856868158037041419759049" + }, + "exponent_reduction_factor": "39505740623/336000", + "family": "complex/same-savings", + "final_integer_test": { + "left_base": 2352001, + "left_exponent": 125, + "relation": "<", + "right_base": 2, + "right_exponent": 2646 + }, + "grid_step": 1000, + "logarithm_power": "1/9", + "majorant": "L(n) <= n^t * (1+log2(n))^(1/q), n>=1; L(0)=0", + "materialized_word": false, + "paid": { + "1": 17623, + "2": 5065, + "3": 1738, + "4": 714, + "5": 254 + }, + "previous_H": 276540184361, + "previous_uniform_saving": "36/15625", + "shift_integer_test": { + "left": 19531250, + "right": 6351461955384057 + }, + "strict_unit_moment_margin": { + "lower": "0.008726900862591659520183402183", + "upper": "0.008726900862591659520183402184" + }, + "t": "199539/200000", + "targets": { + "6": 192, + "7": 56, + "8": 93, + "9": 1229, + "25": 448, + "57": 224 + }, + "tested_mixed_saving": "461/200000", + "theta_upper": "9/10", + "uniform_saving": "36/15625", + "z": "15589/15625" + }, + { + "N": { + "H": 529000, + "encoding": "2^H" + }, + "base_m_to_q_saving_upper": "1.044281998830006779723851077618", + "controls": { + "previous_grid_point_fails_final_majorant": true, + "q_plus_one_fails_contraction": true + }, + "eta_to_q": { + "lower": "0.947033387925024688687300943262", + "upper": "0.947033387925024688687300943263" + }, + "eta_to_q_minus_theta": { + "lower": "0.009533387925024688687300943262", + "upper": "0.009533387925024688687300943263" + }, + "exponent_reduction_factor": "1638232103/132250", + "family": "BIT/same-savings", + "final_integer_test": { + "left_base": 529001, + "left_exponent": 250, + "relation": "<", + "right_base": 2, + "right_exponent": 4761 + }, + "grid_step": 1000, + "logarithm_power": "1/4", + "majorant": "L(n) <= n^t * (1+log2(n))^(1/q), n>=1; L(0)=0", + "materialized_word": false, + "paid": { + "1": 9261, + "2": 9394, + "3": 553, + "4": 308, + "5": 714, + "6": 77, + "7": 1465 + }, + "previous_H": 6552928412, + "previous_uniform_saving": "69/25000", + "shift_integer_test": { + "left": 66465861139202, + "right": 30517578125000000000000000 + }, + "strict_unit_moment_margin": { + "lower": "0.067093183910202306343224051947", + "upper": "0.067093183910202306343224051948" + }, + "t": "997231/1000000", + "targets": { + "8": 3073, + "22": 444, + "50": 222 + }, + "tested_mixed_saving": "2769/1000000", + "theta_upper": "15/16", + "uniform_saving": "69/25000", + "z": "24931/25000" + }, + { + "N": { + "H": 465000, + "encoding": "2^H" + }, + "base_m_to_q_saving_upper": "1.087490880883680536600217019613", + "controls": { + "previous_grid_point_fails_final_majorant": true, + "q_plus_one_fails_contraction": true + }, + "eta_to_q": { + "lower": "0.900646856868158037041419759048", + "upper": "0.900646856868158037041419759049" + }, + "eta_to_q_minus_theta": { + "lower": "0.000646856868158037041419759048", + "upper": "0.000646856868158037041419759049" + }, + "exponent_reduction_factor": "276540184361/465000", + "family": "complex/kappa-0023", + "final_integer_test": { + "left_base": 465001, + "left_exponent": 400, + "relation": "<", + "right_base": 2, + "right_exponent": 7533 + }, + "grid_step": 1000, + "logarithm_power": "1/9", + "majorant": "L(n) <= n^t * (1+log2(n))^(1/q), n>=1; L(0)=0", + "materialized_word": false, + "paid": { + "1": 17623, + "2": 5065, + "3": 1738, + "4": 714, + "5": 254 + }, + "previous_H": 276540184361, + "previous_uniform_saving": "36/15625", + "shift_integer_test": { + "left": 19531250, + "right": 6351461955384057 + }, + "strict_unit_moment_margin": { + "lower": "0.008726900862591659520183402183", + "upper": "0.008726900862591659520183402184" + }, + "t": "199539/200000", + "targets": { + "6": 192, + "7": 56, + "8": 93, + "9": 1229, + "25": 448, + "57": 224 + }, + "tested_mixed_saving": "461/200000", + "theta_upper": "9/10", + "uniform_saving": "4601/2000000", + "z": "1995399/2000000" + }, + { + "N": { + "H": 7100, + "encoding": "2^H" + }, + "base_m_to_q_saving_upper": "1.044281998830006779723851077618", + "controls": { + "previous_grid_point_fails_final_majorant": true, + "q_plus_one_fails_contraction": true + }, + "eta_to_q": { + "lower": "0.947033387925024688687300943262", + "upper": "0.947033387925024688687300943263" + }, + "eta_to_q_minus_theta": { + "lower": "0.009533387925024688687300943262", + "upper": "0.009533387925024688687300943263" + }, + "exponent_reduction_factor": "1638232103/1775", + "family": "BIT/kappa-0023", + "final_integer_test": { + "left_base": 7101, + "left_exponent": 2500, + "relation": "<", + "right_base": 2, + "right_exponent": 32021 + }, + "grid_step": 100, + "logarithm_power": "1/4", + "majorant": "L(n) <= n^t * (1+log2(n))^(1/q), n>=1; L(0)=0", + "materialized_word": false, + "paid": { + "1": 9261, + "2": 9394, + "3": 553, + "4": 308, + "5": 714, + "6": 77, + "7": 1465 + }, + "previous_H": 6552928412, + "previous_uniform_saving": "69/25000", + "shift_integer_test": { + "left": 66465861139202, + "right": 30517578125000000000000000 + }, + "strict_unit_moment_margin": { + "lower": "0.067093183910202306343224051947", + "upper": "0.067093183910202306343224051948" + }, + "t": "997231/1000000", + "targets": { + "8": 3073, + "22": 444, + "50": 222 + }, + "tested_mixed_saving": "2769/1000000", + "theta_upper": "15/16", + "uniform_saving": "1159/500000", + "z": "498841/500000" + } + ], + "input_sha256": { + "research/log-potential-template-ranks/vendor/BIT-ALLSIZE-PARAMETERS.json": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef", + "research/log-potential-template-ranks/vendor/DELAYED-COVER-BRIDGE.md": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.json": "3f1abfafa6f1bb192aafdf342a33ef60fd469fb0764be3eb1516984fc3c22c3f", + "research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.md": "e54345bfdbceda1e41a68682c6902899372252d36d16ca914c1207f0bf03f8b0", + "research/log-potential-template-ranks/vendor/FINITE-PRECOMPILATION.md": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8", + "research/log-potential-template-ranks/vendor/MIXED-PRODUCTIVE-BIT.json": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf", + "research/log-potential-template-ranks/vendor/OUTER-PARAMETERS.json": "15818c10c41ac2ea650e503de830795f6c88830a7f9be9553dd938bb1d76717a", + "research/log-potential-template-ranks/vendor/OUTER-TRANSFER-AUDIT.md": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779", + "research/log-potential-template-ranks/vendor/P3-NATIVE-COVER.json.gz": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f", + "research/log-potential-template-ranks/vendor/check_ledger.py": "1dd56009986eb14dd6603c9193c7ad71dd45c7d005bf71c9cd3f916e66f54d98" + }, + "kappa_0023_retuned_outer": { + "BIT_after_cover": "577/250000", + "BIT_atom_power": "3/1000", + "BIT_before_cover": "1159/500000", + "BIT_fallback_moment_upper": "400001/400002", + "BIT_old_leaf_saving": "384599/10000000000", + "BIT_ordinary_saving": "23011913797/10000000000000", + "BIT_prime_coefficient": "25600000", + "functional_gaps": { + "BIT_borrowed_stock": "9946988086203/10000000000000", + "BIT_cover_gap": "1/100000", + "BIT_linear_adapter": "6988086203/10000000000000", + "BIT_row_stock_sublinear": "99697009/100000000", + "admitted_BIT_above_effective": "7/10000000", + "descriptor_complete_fiber": "1/100000", + "explicit_metadata_halo": "1925001/25000", + "fine_prime_group_guard": "45736661501/250000000000", + "fine_prime_umbrella": "7/2", + "global_gamma_spare": "9/1000000", + "group_below_dimension": "1/50000", + "lambda_above_internal": "1/20000000", + "lambda_above_sigma": "3/20000000", + "lambda_prime_above_lambda": "1/20000000", + "lambda_prime_above_leaf": "49994249/250000000000000", + "membership_record_budget": "1/100000", + "ordinary_BIT_above_admitted": "1913797/10000000000000", + "selected_complex_above_effective": "1/10000000", + "semantic_group_guard": "3/100000", + "semantic_main_guard": "1/100000", + "short_record_fallback": "9976897/10000000", + "uniform_complex_above_b": "1/10000000" + }, + "grid_backoff": "1/10000000", + "grid_floor": 10000000, + "inherited_predicates": { + "actual_bit_above_effective": "7/10000000", + "actual_logarithmic_gamma_guard": "1/100000", + "actual_logarithmic_group_guard": "45736911501/250000000000", + "alpha_logarithm_absorption": "1/1000000", + "boundary_algebraic_matrix_above_kappa": "588499/500000000000", + "cap_above_band": "204270588499/500000000000", + "cap_below_cell": "45724411501/500000000000", + "cap_below_phase_cell_power": "545729411501/500000000000", + "complex_above_effective": "1/10000000", + "complex_below_one_over_32": "36187/1250000", + "complex_endpoint": "1/5000000", + "epsilon_below_one": "1/100000", + "epsilon_positive": "99999/100000", + "fused_gaussian_above_kappa": "5065497/500000000000", + "gaussian_above_main": "2488499/250000000000", + "global_coordinate_router_above_kappa": "3/10000000", + "global_gamma_power_slack": "9/1000000", + "group_below_dimension": "1/50000", + "group_bit_router_above_kappa": "10230991/1000000000000", + "group_gauge_power_slack": "45736661501/250000000000", + "group_key_fits_record": "1/50000", + "group_positive": "99997/100000", + "group_scans_above_kappa": "12471/12500", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_online_final": "284514790400418148631/500000000000000000000000", + "improvement_over_pkg_k2": "622007392794717479267911225169191627777122102965890395790280701170194526587548469132116575062403/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1699": "622358268656645435748941712936355250934431507/1000000000000000000000000000000000000000000000000", + "improvement_over_pr1712": "3111791343283227178741362020680007884145727138632283638941299969772687285461029288600736779707649/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1758": "620254491197700948453466314800026327686526580209199320247542619067215757027414399369818327775017/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1786": "6202452118499510912194521335000000000000000000000000000000001999999800001/10000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1828": "1240490087748910957328658012158594846003377122994839409079344959674400000000000000000000000004006719019826502178085342683975683/2000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1839": "3101225219372277393321645030396487115008442807487098522698362399185677258698371805868475000000001001679754956625544521335670993920703/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1875": "3101225219372277393321645030396487115008442807487098522698362399185677258698371805868471719335776838627743415457068895139647759399172939286143496816535216421325187363046885361425772909502231218314437622205930116079297234806627210590217190600996553729143901162562581526621534715086055386213403722175000000001001679754956625544521335670993920703/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1876": "310122521937227739332164503039648711500844280748709852269836239918567725869837180586847171933577683862774341545706889513964775939917293928614349681653521642132518736304688536142577290950223121831443762220593011607929723480662721059021719060099655372914390116256258152662153471508605538621340372217196657216794137380775174500330086462142358142864921147118845386980694114022172311249292673931726844600000000000000000001001679754956625544521335670993920702577/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1897": "620245043874455478664329006079297423001688561497419704539672479837135451739674361173694343867155367725548683091413779027929551879834587857228699363307043284265037472609377072285154581900446243662887524441186023215859446961325442118043438120199310745828780232512516305324306943017211077242680744434393314433588274761550349000660172924284716285729842294237690773961388228044344622498585347863453689118814253082419197486359454032147189198319033143866021423837056207677317517847011467076188001061138620310116832610271556685687769184940440093096226243113127523863162928128796969576356494654526264864467/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_previous_local_final": "284514790400418148631/500000000000000000000000", + "improvement_over_previous_package": "6221800976855635663689448641223998986170598784229341400200650717283025923262102542077285802551153/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_above_internal": "1/20000000", + "lambda_above_sigma": "3/20000000", + "lambda_above_tau": "1/20000000", + "lambda_prime_above_lambda": "1/20000000", + "lambda_prime_above_leaf": "49994249/250000000000000", + "leaf_saving_above_effective": "24994249/250000000000000", + "main_transform_above_kappa": "88499/500000000000", + "membership_arithmetic_fits_record": "1/100000", + "microbox_face_corrections_above_kappa": "3849887/50000", + "microbox_halo_volume": "7900003/100000", + "polynomial_products_above_kappa": "99769/100000", + "positive_layout_slack": "1/1000000", + "q_below_effective": "1/10000000", + "q_below_internal": "1/10000000", + "q_below_leaf": "49994249/250000000000000", + "q_positive": "11501/5000000", + "short_record_fallback": "9976897/10000000", + "source_axis_superpolynomial": "1/100000", + "sparse_union_movement_above_kappa": "203125588499/500000000000", + "stop_below_one": "99999999/100000000", + "stop_positive": "1/100000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/100000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/100000", + "union_tag_work_per_visit_fits_record": "3/100000" + }, + "minimum_saving_minus_kappa": "88499/500000000000", + "nine_cost_savings": { + "boundary_algebraic_matrix": "1150588499/500000000000", + "fused_gaussian": "1155065497/500000000000", + "global_coordinate_router": "23003/10000000", + "group_bit_router": "2310230991/1000000000000", + "group_scans": "49999/50000", + "main_transform": "1150088499/500000000000", + "microbox_face_corrections": "1925001/25000", + "polynomial_products": "99999/100000", + "sparse_union_movement": "204275588499/500000000000" + }, + "parameters": { + "BIT_saving": "2301/1000000", + "Strassen_exponent": "45/16", + "b": "5751/2500000", + "cap_xi": "454270588499/500000000000", + "complex_uniform_saving": "4601/2000000", + "core_power": "128", + "effective_saving": "23003/10000000", + "epsilon": "99999/100000", + "group_beta": "99997/100000", + "halo_power": "48", + "kappa": "23/10000", + "lambda": "3990799/4000000", + "lambda_prime": "4988499/5000000", + "layout_slack": "1/1000000", + "q": "11501/5000000", + "r0": "1/1000000", + "stop": "1/100000000", + "theta_power": "2" + }, + "rejected_controls": { + "epsilon_one": [ + "actual_logarithmic_gamma_guard", + "epsilon_below_one", + "gaussian_above_main", + "global_gamma_power_slack", + "source_axis_superpolynomial" + ], + "group_equals_dimension": [ + "group_below_dimension", + "group_key_fits_record", + "membership_arithmetic_fits_record" + ], + "unfunded_old_per_axis_scan": [ + "old_per_axis_scan_above_kappa" + ], + "zero_layout_slack": [ + "positive_layout_slack" + ] + }, + "scope": "Exact parameter compatibility under the pinned native/cover/support/outer hypotheses; not a fresh native admission or full replay." + }, + "proof_dependency": "README.md and PR4359 finite source/exit compiler with its native closure hypotheses", + "rejected_mutations": [ + { + "family": "complex/same-savings", + "mutation": "lost_unit_superpotential", + "rejected_at": "unit t-superpotential" + }, + { + "family": "complex/same-savings", + "mutation": "lost_strict_separation", + "rejected_at": "strict mixed separation" + }, + { + "family": "complex/same-savings", + "mutation": "q_plus_one", + "rejected_at": "eta^q > theta" + }, + { + "family": "BIT/same-savings", + "mutation": "lost_unit_superpotential", + "rejected_at": "unit t-superpotential" + }, + { + "family": "BIT/same-savings", + "mutation": "lost_strict_separation", + "rejected_at": "strict mixed separation" + }, + { + "family": "BIT/same-savings", + "mutation": "q_plus_one", + "rejected_at": "eta^q > theta" + }, + { + "family": "complex/kappa-0023", + "mutation": "lost_unit_superpotential", + "rejected_at": "unit t-superpotential" + }, + { + "family": "complex/kappa-0023", + "mutation": "lost_strict_separation", + "rejected_at": "strict mixed separation" + }, + { + "family": "complex/kappa-0023", + "mutation": "q_plus_one", + "rejected_at": "eta^q > theta" + }, + { + "family": "BIT/kappa-0023", + "mutation": "lost_unit_superpotential", + "rejected_at": "unit t-superpotential" + }, + { + "family": "BIT/kappa-0023", + "mutation": "lost_strict_separation", + "rejected_at": "strict mixed separation" + }, + { + "family": "BIT/kappa-0023", + "mutation": "q_plus_one", + "rejected_at": "eta^q > theta" + } + ], + "schema": "logarithmic-uniform-template-ranks/1", + "scope": "Smaller sufficient ambient ranks; no emitted supplier, complete constant bounds, native admission, or new kappa.", + "status": "PASS_LOGARITHMIC_MAJORANT_RANKS", + "verifier_sha256": "9ac70a9c1fe243b95d0ea2eb95468b969af378f29b28b99e2d25b9098d2eed61" +} diff --git a/research/log-potential-template-ranks/SOURCES.json b/research/log-potential-template-ranks/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/log-potential-template-ranks/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/log-potential-template-ranks/TASK.json b/research/log-potential-template-ranks/TASK.json new file mode 100644 index 0000000000..19f989aeb5 --- /dev/null +++ b/research/log-potential-template-ranks/TASK.json @@ -0,0 +1,121 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Can the #4088 four-provider dispatch satisfy the complete ordinary/outer admission contract?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/scatter-boundary-decision/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4088 Scope and Open next questions: local words, native receipts and literal fill do not include a rerun of the mixed four-provider ordinary/outer engine. #3801 is the newer scatter-boundary decision; do not restart #2977 as if untouched.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Pin the provider registry, four native source closures and dispatch. Make a bounded acceptance coverage map or one registry adapter preserving every inherited admission predicate and rejection control (including an omitted fourth provider). Record remaining ordinary/outer obligations and a resource estimate before heavy execution. Stop at unresolved source/caller dependencies; no selected-result promotion from a local pass.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "One provider-registry, dispatch, native-closure or admission-predicate obligation; separate branches must name distinct coverage." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary.", + "Running another root enclosure instead of validating dispatch or weakening an inherited predicate to make mixed admission pass." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics", + "4088", + "3801", + "staged544-mixed-fourth-entry", + "scatter-boundary-decision" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a logarithmic majorant for PR4359 leaf counts, certify smaller ranks at unchanged supplier savings, and retune the complete cover/atom/outer consumer to retain kappa 0.0023 at ranks 2^465000 and 2^7100.", + "scope_change_reason": "Explicit user assignment to build on conditional-kappa-0023, followed by a request to shrink ranks further. The catalogue four-provider audit is replaced by a changed majorant and complete consumer-parameter retuning; no new kappa is claimed.", + "bottleneck_link": "The majorant removes a squared inverse-gap loss; the complete consumer ledger allows the surplus supplier saving to be exchanged for smaller ambient ranks.", + "budget_minutes": 60, + "stop_rule": "One proved majorant, two exact sufficient ranks and negative controls; no template materialization, H decoder campaign or full outer replay.", + "outcome": "completed", + "evidence": "README.md proof and complete retuned consumer bill; RESULT.json exact checks; VENDOR.json immutable predecessor subset.", + "author": "zxv, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof development, code, verification and writing. No subagents or independent human review.", + "open_questions": [ + { + "question": "Can the logarithmic exponent be sharpened using the actual source and exit distributions?", + "why_it_matters": "Further lowers the sufficient rank while testing the coarse worst-case source-band estimate.", + "first_step": "Bound the complete weighted source complement and exit logarithm ratios before changing t or q.", + "blocked_by": "A uniform distribution-sensitive inequality, beyond the present eta/theta bound." + }, + { + "question": "Can one construct a materially smaller supplier or rigorously bound its productive width and instruction count?", + "why_it_matters": "Reduced ambient rank alone does not make the finite program practical.", + "first_step": "Build compressed count recurrences for B_N, P_N and owned-unit counts with denominator clearing.", + "blocked_by": "Huge integer batch widths and no materialized winning template." + }, + { + "question": "Does the inherited compiler and native/outer transfer pass independent mathematical review?", + "why_it_matters": "These remain premises of the conditional rank improvement and proposed kappa.", + "first_step": "Follow pinterbanget’s announced source/exit audit, then separately audit native closure and delayed BIT cover.", + "blocked_by": "Independent acceptance is not supplied by this package." + }, + { + "question": "Can the logarithmic majorant reduce ranks at PR4405’s higher proposed kappa point?", + "why_it_matters": "Combines this structural quantitative improvement with a distinct endpoint refinement.", + "first_step": "Pin PR4405’s exact endpoint parameters and choose a rational tested t strictly below its uniform exponent; then recheck the complete consumer and final integer powers.", + "blocked_by": "Independent acceptance of PR4405 and exact source binding for that additional parameter point; not tested here." + } + ], + "upstream_checkpoint": { + "commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "priority_revision": 7, + "checked_at_utc": "2026-10-21T17:02:27.623597+00:00" + }, + "overlap": { + "checked_at_utc": "2026-10-21T17:02:27.623597+00:00", + "open_pr_records": 513, + "discussion_records": 3250, + "cache_pagination_complete": true, + "scope": "Open PR bodies and discussions; local READMEs/TASKs/ledger. No remote closed PR bodies or code-diff search.", + "nearest": "PR4359; pinterbanget PR4404 at 77f20afb7c24286937c75cb65a7f19e24e7a567f audits the original chain; parallel PR4405 at 873d1b3c96a83b701a5c0bba8e37a861e6672fef sharpens the old power majorant and increases the proposed kappa. This package instead replaces the power majorant by a logarithmic factor and reprices the smaller-rank kappa=0.0023 consumer." + } +} diff --git a/research/log-potential-template-ranks/VENDOR.json b/research/log-potential-template-ranks/VENDOR.json new file mode 100644 index 0000000000..cd8b6e6efb --- /dev/null +++ b/research/log-potential-template-ranks/VENDOR.json @@ -0,0 +1,69 @@ +{ + "schema": "pinned-predecessor-subset/1", + "repository": "https://github.com/zxv/integer-mult-bounds", + "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4359", + "source_commit": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "scope": "Ten byte-identical inputs for the conditional leaf-count, cover/atom and outer-parameter arguments only; native programs and full outer admission are not reproduced.", + "files": [ + { + "original_path": "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "path": "research/log-potential-template-ranks/vendor/FINITE-PRECOMPILATION.md", + "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca", + "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8" + }, + { + "original_path": "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "path": "research/log-potential-template-ranks/vendor/MIXED-PRODUCTIVE-BIT.json", + "git_blob": "6a139eedbc1015c13df6f2a4333e1a89b5edd18d", + "sha256": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf" + }, + { + "original_path": "research/kappa-rebuild/controller/EXPLICIT-TEMPLATE-BOUNDS.json", + "path": "research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.json", + "git_blob": "19b27c6e40a7bf20822ec35b7a4159cc7e89be2e", + "sha256": "3f1abfafa6f1bb192aafdf342a33ef60fd469fb0764be3eb1516984fc3c22c3f" + }, + { + "original_path": "research/kappa-rebuild/controller/EXPLICIT-TEMPLATE-BOUNDS.md", + "path": "research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.md", + "git_blob": "b00acfbe8bf0fb540e90eebd0d1fe0b094b1880d", + "sha256": "e54345bfdbceda1e41a68682c6902899372252d36d16ca914c1207f0bf03f8b0" + }, + { + "original_path": "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz", + "path": "research/log-potential-template-ranks/vendor/P3-NATIVE-COVER.json.gz", + "git_blob": "51a09b3952a491f06780bf6ce5f69b385f026b21", + "sha256": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f" + }, + { + "original_path": "research/kappa-rebuild/controller/OUTER-PARAMETERS.json", + "path": "research/log-potential-template-ranks/vendor/OUTER-PARAMETERS.json", + "git_blob": "956853dcd169c71ac69fff5d2c213d2ebb89c22e", + "sha256": "15818c10c41ac2ea650e503de830795f6c88830a7f9be9553dd938bb1d76717a" + }, + { + "original_path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "path": "research/log-potential-template-ranks/vendor/OUTER-TRANSFER-AUDIT.md", + "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535", + "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779" + }, + { + "original_path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "path": "research/log-potential-template-ranks/vendor/BIT-ALLSIZE-PARAMETERS.json", + "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a", + "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef" + }, + { + "original_path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "path": "research/log-potential-template-ranks/vendor/DELAYED-COVER-BRIDGE.md", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "original_path": "research/kappa-observation-integration/release-work/current/package/outer/check_ledger.py", + "path": "research/log-potential-template-ranks/vendor/check_ledger.py", + "git_blob": "d3b6149c5c1cca84c7c305f6e2e32c814e30777e", + "sha256": "1dd56009986eb14dd6603c9193c7ad71dd45c7d005bf71c9cd3f916e66f54d98" + } + ] +} diff --git a/research/log-potential-template-ranks/VERIFY.json b/research/log-potential-template-ranks/VERIFY.json new file mode 100644 index 0000000000..ad4fe19a23 --- /dev/null +++ b/research/log-potential-template-ranks/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/log-potential-template-ranks/vendor/FINITE-PRECOMPILATION.md", + "research/log-potential-template-ranks/vendor/MIXED-PRODUCTIVE-BIT.json", + "research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.json", + "research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.md", + "research/log-potential-template-ranks/vendor/P3-NATIVE-COVER.json.gz", + "research/log-potential-template-ranks/vendor/OUTER-PARAMETERS.json", + "research/log-potential-template-ranks/vendor/OUTER-TRANSFER-AUDIT.md", + "research/log-potential-template-ranks/vendor/BIT-ALLSIZE-PARAMETERS.json", + "research/log-potential-template-ranks/vendor/DELAYED-COVER-BRIDGE.md", + "research/log-potential-template-ranks/vendor/check_ledger.py", + "research/log-potential-template-ranks/VENDOR.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Four logarithmic-majorant rank certificates, 12 rejecting scientific mutations, four failing previous grid points, complete BIT cover/atom chain, nine outer cost rows, 63 inherited predicates, 22 added interface inequalities and four rejecting outer controls." + } + ] +} diff --git a/research/log-potential-template-ranks/vendor/BIT-ALLSIZE-PARAMETERS.json b/research/log-potential-template-ranks/vendor/BIT-ALLSIZE-PARAMETERS.json new file mode 100644 index 0000000000..fbe6da7241 --- /dev/null +++ b/research/log-potential-template-ranks/vendor/BIT-ALLSIZE-PARAMETERS.json @@ -0,0 +1,69 @@ +{ + "C0_before_cover": "69/25000", + "C0_minus_C1": "1/100000", + "C1_after_cover": "11/4000", + "atom_power": "3/1000", + "finite_constants_to_replace": { + "ambient_dimension": "N, not50 or64", + "bad_fallback_children": "At most32*N^2 per bad final leaf", + "coefficient_data": "Every fixed rational entry, inverse, determinant, prefix descriptor and height", + "fixed_row_routes": "R, original port charts and every internal matcher/inverse", + "generic_affine_work": "At most4*N^2-2*N basic shears per rank1 normalizer together with its inverse", + "owned_storage": "C, bounded by one owned bank per allocated finite unit instance", + "paid_leaf_count": "P, including copied-center descendants", + "pointwise_and_copy_count": "L, literal compiled scalar/copy/erase records", + "productive_roles": "B, not3739 or661" + }, + "finite_template_hypothesis": "Fixed integers N>=2,B>=1,P>=1 and a whole-cover native schematic uniform word, with P/B < N^(1-C0), final paid leaves of rank1, arbitrary productive inputs and separately owned storage.", + "mixed_margin_at_C0": { + "display": 0.7944031286900184, + "lower": "67580344230009584908122845692691165477/85070591730234615865843651857942052864", + "strict_negative": false, + "strict_positive": true, + "upper": "270321376920038339632491382770764742407/340282366920938463463374607431768211456" + }, + "new_kappa": false, + "old_ordinary_saving": "384599/10000000000", + "ordinary_saving_admitted": "27/10000", + "ordinary_saving_before_final_relaxation": "27418653797/10000000000000", + "ordinary_saving_display": 0.0027418653797, + "prime_rule": { + "N_to_d_lower": "200001/200000", + "also_required": "Odd prime avoiding every fixed rational denominator, matcher determinant and chosen rank witness of the entire compiled word.", + "bound": "q > 25600000 * N^5", + "complete_moment_upper": "400001/400002", + "fallback_multiplier_upper": "400001/400000", + "good_moment_upper": "N^(-d), d=C0-C1", + "strict_moment_slack_lower": "1/400002" + }, + "root_cost_terms": [ + "e^(1-delta)", + "e^((1-delta)*(1-C1)+delta*(1-a_old))", + "e^delta * log(e)" + ], + "schema": "conditional-delayed-cover-BIT-allsize-parameters/1", + "source_sha256": { + "notes/batched-bit-rows.tex": "ef72c0ead19373cbc19c8a3aacb44dd0f75353ee5f4d055f775a986a4878022c", + "notes/three-stage-cover-bit.tex": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511", + "notes/three-stage-cover-rows.tex": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8", + "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json": "9ece46fdfda6182e757e9a3b1f513fb3d029d730f3bafdcd6ed59180a14175b0", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.json": "1e1a91871ad8d1098b6851c95d257e8e3fb130222933009b4edfb5e2c2d5c471", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf", + "research/kappa-rebuild/bit/bit_allsize_parameters.py": "59f92cf44019c27bde3db2f4482f2b5fcf25f0c3dcf071319d46b041f7b6a821" + }, + "status": "PASS_EXACT_PARAMETERS_CONDITIONAL_ON_FINITE_UNIFORM_PRECOMPILATION", + "stock": { + "asymptotic": "Fixed compiled N,B,P: k=O_(N,B,q)(w*log e)=o(e), w=ceil(e^(3/1000)); pad high rows once by factor<2.", + "borrowed_digits": "k <= D_N(ceil(e/w))*(N^2*(w-1)+ceil(log_q(B*|GL_N(F_q)|)))+ceil(log_q S_old)+1", + "depth_bound": "D_N(n)=floor(log_N n) for rank<=floor(n/N) children; any larger explicit integer bound is safe.", + "descendant_weights": "Only final leaves are lowered. This outer cover row and role type become ancestor data; every next ordinary invocation has fresh disjoint role stock.", + "reserve": "S(e,w)=W(w)^D_N(ceil(e/w))*S_old(e,w)", + "role_divisor": "W(w)=B*|GL_N(F_q)|*q^(N^2*(w-1))" + }, + "strict_power_gaps": { + "borrowed_stock_log_absorption": "9942581346203/10000000000000", + "final_relaxation": "418653797/10000000000000", + "linear_adapter": "2581346203/10000000000000" + } +} diff --git a/research/log-potential-template-ranks/vendor/DELAYED-COVER-BRIDGE.md b/research/log-potential-template-ranks/vendor/DELAYED-COVER-BRIDGE.md new file mode 100644 index 0000000000..a58774e237 --- /dev/null +++ b/research/log-potential-template-ranks/vendor/DELAYED-COVER-BRIDGE.md @@ -0,0 +1,401 @@ +# Delaying the BIT cover until the whole finite program is compiled + +Status: a constructive native-interface argument, with an exact local-ring +audit. This closes the particular common-weight mismatch identified in the +first mixed BIT proposal, conditional on the finite mixed-flow compiler +producing the stated finite projector program. It is not an independent +proof of that compiler's asymptotic termination or of integer multiplication. + +Substantial OpenAI assistance. Apache-2.0. This argument uses the arbitrary- +projector GL cover and weighted-child normal form in +[`notes/three-stage-cover-bit.tex`](../../../notes/three-stage-cover-bit.tex), +the retained PR589 local word and its predecessors, and the finite +precompilation proposal in `../architecture/FINITE-PRECOMPILATION.md`. +The decisive order of operations was proposed jointly with the architecture +research task: compile all internal jobs first; apply one common cover and +one common external weight only afterwards. + +## 1. The earlier obstruction was real + +A productive rank-eight helper is a proper projector job inside a larger +ambient address space. After an ambient GL cover, its endpoint is + +\[ +D_{gPg^{-1}}, +\] + +not the same fixed eight-coordinate interchange on every cover row. +Lowering this job immediately to a canonical recursive query introduces a +diagonal weight determined by the pivot coefficients of `g P g^-1`. +Jobs from different parents can have different such weights. The inherited +scalar word accepts one common external weight across every fresh role; +simply placing differently weighted jobs in its roles is invalid. + +The solution below does not identify these weights. It avoids creating +weighted internal jobs at all. Only leaves of the entire precompiled word +are lowered to canonical weighted calls. + +## 2. Native projector jobs before canonical lowering + +Fix an ambient rational head space of dimension `N` and the atom-reversal +matrix `C_N`. For any rational idempotent `P` put + +\[ +D_P=\begin{pmatrix} +I-P & PC_N\\ +C_NP & I-C_NPC_N +\end{pmatrix}. +\] + +For `G` invertible let + +\[ +Q_G=\operatorname{diag}(G,C_NGC_N). +\] + +Direct block multiplication gives + +\[ +Q_GD_PQ_G^{-1}=D_{GPG^{-1}},\qquad +D_PD_{I-P}=D_I. +\] + +No symmetry of `P` is required. The second identity says that any source +job and its complementary projector complete the full interchange on that +array. If a unit of rank `m` is used at column multiplicity `c`, first embed +its rational projectors into the chosen `mc`-dimensional coordinate block +of the common `N`-dimensional space. Complete unused coordinates are +spectators. All these dimensions and embeddings are constants of the +finite precompiled program. + +The local PR589 primitive, the new global controller, its pointwise boundary +adapters, and owned COPY storage can all be treated as a finite chronological +word of pointwise scalar operations, proper projector requests, restores, +and fixed right-multiplication symbols on one future cover coordinate. +Their exact finite operator identities are established independently of a +generic canonical child normalizer. An internal request may therefore be +replaced by a finite native word computing the same `D_P` on arbitrary data. + +This schematic qualification matters. The p3 construction already uses +per-port chart routes to share one local helper bank across 111 data ports. +It is not a 3,739-field word with those routes silently deleted. Before +choosing the final cover, embed every local projector and every port chart +into the common ambient `N`. Preserve all fixed right-route symbols during +substitution. Only then instantiate that single `GL_N` cover. A helper's +endpoint is the rank-eight local-space projector at its local invocation +vertex, while main data endpoints use their port-specific line and stage +projectors. `BIT-P3-NATIVE-BINDING.json` checks every fixed rational port +chart, this ownership distinction, and the complete recursive tariff. + +## 3. Equal rank gives a fixed rational matcher + +For rational idempotents `P,Q` of the same rank, choose a rational basis of +their images and kernels. Let `B_P` and `B_Q` be the corresponding full basis +matrices, with image columns first. Then + +\[ +S=B_PB_Q^{-1},\qquad SQS^{-1}=P. +\] + +This is a finite rational matrix construction. A physical execution of the +dense address map `Q_S` is **not** assumed. The matcher is used only as a +right multiplication of the full cover row, as follows. + +Choose a fixed odd prime `q` avoiding the denominators and nonzero +determinants of every native matrix and matcher in the finite program. +For atom width `w`, use one global cover + +\[ +\mathcal G=\operatorname{GL}_N(\mathbb Z/q^w\mathbb Z). +\] + +All matchers reduce to invertible matrices over this local ring. +An array role is accompanied by the full cover coordinate `g in G`. +Its entries at different `g` are independent data. + +Suppose a parent role at cover row `g` requests `D_(g P g^-1)` and a child +target role at its cover row `h` computes `D_(h Q h^-1)`. Before running +the child, route that complete target-role fiber by + +\[ +x_g\longmapsto y_{gS}=x_g. +\] + +Execute the child word on these routed inputs, then undo the role-specific +route. The endpoint on the parent's original `x_g` is exactly + +\[ +D_{(gS)Q(gS)^{-1}}=D_{gPg^{-1}}. +\] + +Every child target role can use its own fixed matcher `S`. Each mapping +`g -> gS` is a bijection of the *whole* cover fiber, so no input is copied, +discarded, or assumed zero. The child word can mix its roles at a common +child row `h`, because those routed inputs are arbitrary independent data. +After the completed word returns its independent endpoints, undoing the +routes restores the parent ordering. The finite flow's ownership and +chronology are still required; cover routing does not repair an aliased +or cyclic flow. + +## 4. One common external weight survives every internal routing + +At column multiplicity `f`, let the outer invocation's diagonal weight +`A` be any permitted generated descriptor on its `Nf` head atoms. It can +depend on exposed ancestor rows and atom indices. It must be independent +of all fresh role and cover fields of this entire compiled invocation. +Write `Lambda_A=diag(A,I)`. + +Conjugate the entire completed covered word by `Lambda_A`. Pointwise scalar +ADDs commute with this common address permutation across roles. Every +internal role route also commutes with it: a route changes only a fresh +role or the current cover row, while `A` is independent of both. Thus the +matching identity becomes + +\[ +\Lambda_A D_{(gS)Q(gS)^{-1}}\Lambda_A^{-1} +=\Lambda_A D_{gPg^{-1}}\Lambda_A^{-1}. +\] + +There is no child-specific weight to reconcile inside the precompiled +word. The source/complement product gives + +\[ +\Lambda_A D_I\Lambda_A^{-1}=F_A +\] + +on every productive source array. This is exactly the inherited weighted +full-interchange endpoint. Owned zero storage is unaffected by address +permutations and is excluded from productive output credit; its allocation, +initialization and final erasure still belong to the finite word. + +The condition on `A` is essential. The companion audit exhibits a concrete +failure when `A` is allowed to depend on the current fresh cover row. The +argument does not quietly weaken the old ancestor-only contract. + +## 5. Only the final leaves become weighted children + +After the mixed finite compiler has replaced every internal request, suppose +the remaining paid projector requests have rank one. At multiplicity `f`, +each is a rank-`f` residual on the outer atom space. Apply the inherited +generic ordered normal form to this *finished* leaf list. + +For a generic residue class, that proof produces unit lower intrabank and +cross-bank adapters around one contiguous weighted reversed interchange. +For column `j`, the resulting weight is + +\[ +A_{\rm child}[j]=A[i_0f+j]D_P[0], +\] + +with the inherited reversed tail pairing. The pivot coefficient is evaluated +from the current outer cover row and the fixed leaf projector. Those are +ancestor data when the recursive rank-`f` child is invoked. Its fresh roles +come from unused row stock, so the child's weight is independent of them. + +Different leaf calls can have different weights; the ordinary recursion +already permits this. Each such child itself receives one common weight +across all of *its* fresh roles and cover rows. This is the critical +distinction from calling a mixed unit on several already-normalized, +differently weighted parent jobs. + +Bad residue classes use the inherited genuine local-ring fallback, including +its swaps, paired scalings and reversals. This is charged explicitly rather +than declaring a nonunit pivot invertible. + +## 6. Routing is priced by the retained native lemma + +The cover row has the unique chart `g=g0+qG1`, with `g0` in `GL_N(F_q)`. +For each fixed matcher `S`, right multiplication gives a permutation of +the finite low type and a fixed affine map on the high matrix, with carry +determined by the low type. The retained proof of finite cover routing +implements this with a constant number of fixed scalings, ordered shifts +and old atom interchanges. Its cost is + +\[ +O(Vw^{1-a_{\rm old}}) +\] + +per fixed route. It is not a free address-gather operation. A precompiled +word contains finitely many matchers, so their total remains a finite +constant times this term. High matrices are streamed by fixed low type; +the number of tapes and program types does not grow with `w`. + +The same statement holds for nonintegral rational matchers: choose `q` +avoiding their fixed denominators, use their local-ring representatives, +and apply the retained fixed-rational routing lemma. The exact small audit +uses integral unimodular matchers to exercise the carry formula directly. + +## 7. Moment and row-stock consequences + +Let the finite uniform compiler have `B` productive source arrays, ambient +rank `N`, and `P` rank-one leaves, with a certified strict inequality + +\[ +\frac PB N^{-\tau}<1. +\] + +The covered, weighted word has the same normalized good-class leaf count. +Choose `q` large enough that the full fallback surcharge fits the displayed +slack. For example, the conservative inherited per-leaf bounds yield + +\[ +\mu_\tau\le +\frac PB N^{-\tau} +\left(1+\frac{2N^3}{q}\,32N^2\right)<1. +\] + +No old fixed choice of `q` or old numerical fallback envelope is reused for +the potentially enormous new `N`. Prime avoidance and a sufficiently large +prime exist because the whole precompiled program is finite. + +For the present candidate, use the exact mixed saving +`C0=69/25000=0.00276` for the finite compiler and retain +`C1=11/4000=0.00275` after covering. Put `d=C0-C1=1/100000`. +The former gives `P/B\frac{256N^5}{d}=25,600,000N^5. +\] + +Then the fallback multiplier is less than `1+d/4`, while +`N^d >= 1+d/2` for `N>=2`, using `log 2>1/2` and `exp x>=1+x`. +Thus the complete moment is strictly below +`(1+d/4)/(1+d/2)<1`. This uses an explicit exponent gap and does not +require knowing the eventual winning template's numerical moment slack. + +The cover consumes `N^2(w-1)` high-row digits plus a fixed low-type and role +reserve. Its finite owned-storage and scalar costs may be enormous. They +replace the old constants. For fixed `N` and a fixed finite word, the +ancestor reserve remains `O(w log e)`, and the previous eventual-threshold +arguments still apply after substituting those constants. They cannot be +reused numerically without that substitution. + +The existing weighted recursion can now be applied to this one uniform +supplier: every paid query has width at most `f`, the endpoint is `F_A`, and +all routing and scalar terms have the inherited permitted form. This is a +native-interface bridge. The complete final exponent still depends on the +mixed compiler's termination theorem, its exact leaf-count saving, and the +outer multiplication transfer. + +## 8. The ordinary BIT saving and explicit template constants + +The retained stopped recurrence gives + +\[ +T(n,w)=O(n+n^{1-C_1}w^{1-a_{\rm old}}),\qquad +a_{\rm old}=384599/10^{10}. +\] + +The old atom exponent `1/1000` cannot be reused here: its linear `n` term +would limit the ordinary saving to `0.001`. Instead choose +`delta=3/1000` and `w=ceil(e^delta)` from the original chunk width `e`. +For the whole compiled program set + +\[ +W(w)=B|\operatorname{GL}_N(\mathbb F_q)|q^{N^2(w-1)}. +\] + +A safe reserve is `W(w)^D * S_old`, with +`D >= floor(log_N ceil(e/w))`; all final ordinary children have rank at +most `floor(n/N)`. Therefore the borrowed high-digit count satisfies + +\[ +k\le D\left(N^2(w-1)+ +\left\lceil\log_q(B|\operatorname{GL}_N(\mathbb F_q)|)\right\rceil\right) ++\left\lceil\log_qS_{\rm old}\right\rceil+1 +=O_{N,B,q}(w\log e). +\] + +This is `o(e)`. For sufficiently large `e`, borrow `ka_BIT` and `delta<1-a_BIT` hold strictly. The linear adapter +term and the borrowed-stock logarithm are lower order. One may relax the +ordinary saving to the simpler rational `27/10000=0.0027`. +`BIT-ALLSIZE-PARAMETERS.json` records all strict rational gaps and the +exact mixed margin at `C0`. This remains conditional on the finite uniform +compiler premise; the enormous word is not materialized in this package. + +The final ambient dimension is `N`, the productive role count is `B`, and +the rank-one leaf count is `P`. They are not the old `64`, `661`, `3739`, +or the base unit's literal counts. Let `C` be the total allocated owned +array fields, `L` the literal scalar/copy/erase count, and `R` all fixed +right routes including inverses. Keep the full finite matrix and +coefficient-height list. The new fixed tape inventory can use one stream +per productive or owned role, with the inherited parking stack; it is +finite in `B+C`. Every route is charged, and every final leaf has its own +normalization and possible fallback. A rank-one generic normalizer and +its inverse use at most `4N^2-2N` elementary lower/cross-bank shears; the inherited bad +normalizer uses at most `32N^2` recursive calls of width at most `f`. + +These constants can be enormous and affect the eventual threshold. Their +dependence on the fixed compiled template does not introduce a new power +of the later input length. The mixed-flow argument is used to bound the +normalized number of paid rank-one leaves; it must not assume that dense +matrix routing costs stay uniformly bounded while the candidate template +dimension `N` is increased in the existence search. + +## 9. Exact finite audit + +Run: + +```sh +python3 -B research/kappa-rebuild/bit/delayed_cover_bridge.py +``` + +The audit enumerates every one of the 3,888 rows of `GL_2(Z/9Z)` for each +of two independently matched target roles. It checks 7,776 exact physical +projector identities, both full cover bijections, the affine high-row carry +formula, and every one of the 6,561 addresses for common-gauge scalar +commutation. Its external weight is `(2,4)`, so it is not restricted to an +unweighted or constant-across-axis input. The emitted leaf-weight histogram +is nonconstant. Two explicit negative controls reject omitting a matcher +and allowing the external weight to depend on the fresh cover row. + +These are independent checks of concrete algebra and a genuine local ring. +The general argument is the conjugacy calculation above, not an inference +from the finite sample. + +## Open next questions + +1. Independently audit that the finite lockstep compiler only substitutes + whole arbitrary-input jobs and gives each simultaneously live child role + a distinct physical array. The row matching here assumes that ownership. +2. Bind the new BIT p3 native physical projector list and its exact local + primitive into the abstract finite compiler, including all COPY centers. +3. Write the parameter substitutions for the eventual row reserve and the + final BIT/complex outer exponent. A finite numerical mixed moment alone + is still insufficient for a new multiplication claim. diff --git a/research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.json b/research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.json new file mode 100644 index 0000000000..19b27c6e40 --- /dev/null +++ b/research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.json @@ -0,0 +1,149 @@ +{ + "cases": [ + { + "N": { + "H1": 276540184361, + "encoding": "2^H1" + }, + "delta": "1/2000000", + "eta_strict_lower": "1/4", + "exact_integer_test": { + "N_exponent": 15589, + "P_and_B_exponent": 15625 + }, + "exit_power_gap": "0", + "family": "complex", + "final_strict_power_gap": "1/2000000", + "h": "1/10", + "induction_constant_A": "n0^(1-z0)", + "k_min": 6, + "m": 57, + "m_to_h_integer_comparison": { + "left": 57, + "right": 1024 + }, + "materialized_winning_word": false, + "n0": { + "H0": 60000040, + "encoding": "2^H0" + }, + "negative_controls": { + "one_less_H0_fails_chosen_exit_bound": true, + "one_less_H1_fails_strict_final_bound": true, + "requested_004_not_supported_by_this_unit": true + }, + "paid": { + "1": 17623, + "2": 5065, + "3": 1738, + "4": 714, + "5": 254 + }, + "proven_uniform_moment": "P_N/B_N < N^z", + "r_max": 5, + "rank_one_surplus": 224, + "strict_test_margin": { + "lower": "0.00872690086259165952018340218333643", + "upper": "0.00872690086259165952018340218333644" + }, + "t": "199539/200000", + "targets": { + "6": 192, + "7": 56, + "8": 93, + "9": 1229, + "25": 448, + "57": 224 + }, + "template_definition": "Apply the integer, ordered, denominator-cleared compiler to this exact N. Keep every scalar/route operation and one owned bank per finite unit instance; only final rank-one leaves remain paid.", + "tested_mixed_saving": "461/200000", + "theta_integer_comparison": { + "left": 9765625, + "right": 10077696 + }, + "theta_upper": "9/10", + "uniform_saving": "36/15625", + "z": "15589/15625", + "z0": "1995391/2000000" + }, + { + "N": { + "H1": 6552928412, + "encoding": "2^H1" + }, + "delta": "9/2000000", + "eta_strict_lower": "1/4", + "exact_integer_test": { + "N_exponent": 24931, + "P_and_B_exponent": 25000 + }, + "exit_power_gap": "3/32000000", + "family": "BIT", + "final_strict_power_gap": "9/2000000", + "h": "1/16", + "induction_constant_A": "n0^(1-z0)", + "k_min": 8, + "m": 50, + "m_to_h_integer_comparison": { + "left": 50, + "right": 65536 + }, + "materialized_winning_word": false, + "n0": { + "H0": 10666731, + "encoding": "2^H0" + }, + "negative_controls": { + "one_less_H0_fails_chosen_exit_bound": true, + "one_less_H1_fails_strict_final_bound": true, + "requested_004_not_supported_by_this_unit": true + }, + "paid": { + "1": 9261, + "2": 9394, + "3": 553, + "4": 308, + "5": 714, + "6": 77, + "7": 1465 + }, + "proven_uniform_moment": "P_N/B_N < N^z", + "r_max": 7, + "rank_one_surplus": 225, + "strict_test_margin": { + "lower": "0.06709318391020230634322405194711404", + "upper": "0.06709318391020230634322405194711405" + }, + "t": "997231/1000000", + "targets": { + "8": 3073, + "22": 444, + "50": 222 + }, + "template_definition": "Apply the integer, ordered, denominator-cleared compiler to this exact N. Keep every scalar/route operation and one owned bank per finite unit instance; only final rank-one leaves remain paid.", + "tested_mixed_saving": "2769/1000000", + "theta_integer_comparison": { + "left": 33232930569601, + "right": 35184372088832 + }, + "theta_upper": "15/16", + "uniform_saving": "69/25000", + "z": "24931/25000", + "z0": "1994471/2000000" + } + ], + "new_kappa_claimed_by_this_file": false, + "proof_dependency": "The written native finite-precompilation theorem, including arbitrary-input closure and every exact ordered batch. This receipt checks its quantitative sufficient inequalities, not the theorem as a formal proof.", + "schema": "explicit-compressed-uniform-template-ranks/1", + "scope": "Explicit fixed ranks are specified in compressed form. No near-threshold word, GL cover, B_N, P_N or U_N is materialized. Their exact finite algorithms and replacement constants remain part of the construction.", + "source_sha256": { + "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf", + "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f", + "research/kappa-rebuild/controller/explicit_template_bounds.py": "4b3fbc216c32821729403d32efa8f75a418079b3bb57eb6204e044411d7d7f6f", + "research/kappa-rebuild/transfer-audit/AUDIT.md": "032488343667d19613cab84df5dad554cfd2a283fb4fc0d4c9b4d165cfa04669", + "research/kappa-rebuild/transfer-audit/finite_dag_audit.py": "f842f0e07ca40a181782a565a381b0ee20c6a4b08b8c2b8a4d5d630381bd1e8e" + }, + "status": "PASS_EXACT_SUPERPOTENTIAL_AND_COMPRESSED_RANK_BOUNDS" +} diff --git a/research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.md b/research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.md new file mode 100644 index 0000000000..b00acfbe8b --- /dev/null +++ b/research/log-potential-template-ranks/vendor/EXPLICIT-TEMPLATE-BOUNDS.md @@ -0,0 +1,108 @@ +# Explicit finite ranks, without an unperformed search for the first success + +Apache-2.0. Substantial OpenAI assistance. The integer lockstep flow is Jacob +Alan Sussman's Theorem 1G. The native finite precompilation argument and its +independent audit are in `../architecture/FINITE-PRECOMPILATION.md` and +`../transfer-audit/AUDIT.md`. This note strengthens the quantitative choice +of the fixed template rank. It does not claim to materialize that template. + +## 1. Use a strict superpotential rather than an unknown exact root + +Write `L(n)=P_n/B_n` for the exact normalized number of paid rank-one leaves +in the integer compiler, including source complements and every exit batch. +Choose rational `0theta`, and put `h=1-theta_bar>0` and +`delta=z0-t>0`. In our two cases the exact integer inequalities prove +`m^h<2` and `2*r_max<=16`. Since `n>=m`, + +``` +m*E(n)/n < 16*n^(-h). +sum_e x_e*e^z0 <= (16*n^(-h))^delta * sum_s w_s*s^z0. +``` + +The source complements pay for this exit term. Concavity gives + +``` +n^z0-sum_s w_s*(n-s)^z0 >= eta*sum_s w_s*s^z0, +eta=z0*m^(z0-1). +``` + +The exact logarithm intervals check `z0>1/2` and `m^(1-z0)<2`, hence +`eta>1/4`. Set + +``` +H0=ceil((3+4*delta)/(h*delta)), n0=2^H0. +``` + +This exceeds the finite base range. For every `n>=n0`, the exit coefficient +is at most `1/80}`, `k_min=min{k:W_k>0}`, and +`r_max=max{r_j}`. Require `r_max g*S`, keeps one +external weight throughout the entire finite circuit, and lowers only its +final rank-one leaves. All rational matchers, role routes and their inverses +are fixed before choosing the odd prime and its exclusions. Every route +uses complete equal-multiplicity cover fibers and the retained, costed row +permutation primitive. This gives the same finite DAG argument in the +rational-cover program category. The BIT binding supplies the actual native +projectors; a rank count alone would not provide this implementation. + +## 2. Proposed conclusion + +Suppose the preceding hypotheses hold and the mixed balance has root +`tau` in `(0,1)`: + +``` +sum_j r_j^tau = sum_k W_k k^tau. +``` + +For every `z` with `tau=2`, a fixed number `B_N` of productive arrays, +and only rank-one paid children, whose number `P_N` satisfies + +``` +P_N < B_N * N^z. +``` + +Every productive output is the full rank-`N` job. The construction may have +an enormous finite scalar word, role inventory and owned-storage requirement. +Those quantities affect constants and the eventual input threshold. They are +not omitted and are not credited as extra output jobs. + +If this uniform supplier is admitted under the retained native, precision and +fixed-tape premises, the existing uniform recursion applies directly. A new +dynamic RAM-to-Turing-machine simulation is not being assumed here. + +## 3. The integer lockstep flow at a fixed rank + +This is the part of Theorem 1G used by the compiler. At one fixed top rank +`N`, its units, source jobs and exit jobs have integer multiplicities. +For a multi-index `a` on the target types define + +``` +c(a) = product_k k^(a_k), +u(a) = multinomial(|a|;a) * product_k W_k^(a_k). +``` + +The exact Pascal identity is + +``` +u(b) = sum_{k:b_k>0} W_k*u(b-e_k). +``` + +Let `G` be the largest `|a|` with `m*c(a)<=N`. A class is indexed by a +sequence of paid rounds `s` of length `d<=G`; its dilation is +`rho_s=product r_j`. It contains `u(a)` units at column `rho_s*c(a)` for +each `a` with `|a|=G-d` and `m*rho_s*c(a)<=N`. + +For one parent paid round, the Pascal bijection matches its job copies to +target roles of the child class, at exactly equal integer ranks. Missing +demands are top sources. Separation ensures every parent job is consumed. +The source ranks lie in `(N/m,N]`; only the deepest classes produce exit +jobs, all strictly smaller than `N` once `N` is outside the finite base range. + +Process a class in word order. At round `j`, suspend every unit of that +class, complete the entire child class fed by that round, and only then +advance the parents to round `j+1`. This forbids a unit from requiring both +an earlier and a later round of the same suspended parent. The resulting +dependency graph is finite and acyclic. Its edges carry complete array jobs, +not individual scalar values copied for free. + +These integer quantities exist before normalizing the sources to total +weight one. Let `S_s` be the number of source jobs of rank `s`, let +`S=sum_s S_s`, and let the ordered exit batches be `(e,t)` with `t` jobs +of rank `e` each. This finite integer flow is the compiler input. + +## 4. Clear every batch denominator constructively + +Induct on the integer top rank `N`. For each smaller rank `e` the compiler +has already constructed a uniform program on `B_e` arbitrary arrays, +computing full rank `e` with `P_e` paid rank-one calls. For a sufficiently +small rank use the ordinary sequential program: `B_e=1`, `P_e=e`. + +For the current flow choose an integer `a` divisible by every `B_e` needed +for an exit and every `B_(N-s)` needed for a nonzero source remainder. +The product of those finitely many positive integers is a valid choice; +their least common multiple is a smaller optional choice. Set + +``` +B_N = a*S. +``` + +Assign `a*S_s` of the input arrays to each source rank `s`. On each of those +arrays, first complete its `N-s` complementary coordinates using the +already-compiled smaller uniform program. All such batches are integral +because `a` is divisible by their program widths. This preliminary action +commutes with the intended `s`-coordinate job and fixes its input coordinates. + +Make `a` copies of the integer lockstep flow. Route its source arrays to +their exact input slots using permitted whole-array adapters. At a deepest +exit batch, `a*t` is divisible by `B_e`; replace that batch by copies of +the smaller uniform rank-`e` program. Restore its role ordering and adapters +before resuming the suspended parent class. Execute the finite DAG in the +lockstep order, and finally restore the original source-array ordering. + +Every array has now received its disjoint complementary job and source job, +hence the full rank-`N` transform. No copied scalar input or blank helper is +treated as another independent output. Every original array occurs exactly +once as a source; interior target slots are jobs on those arrays, not new +productive inputs. + +Induction removes all recursive calls: the only remaining paid children +have rank one. Clearing denominators multiplies productive arrays and paid +operations equally, so it preserves the per-array leaf count. In formulas, + +``` +P_N/B_N = (1/S) * [ + sum_s S_s * (P_(N-s)/B_(N-s)) + + sum_(ordered exit batches e,t) t * (P_e/B_e) +]. +``` + +Zero-rank terms vanish. Any plain rank-one exits are the ordinary base +program. Scalar and routing passes have their own analogous nonnegative +count and must be included in the asymptotic cost used to choose `N`. + +This construction uses full integer batches; it does not assume that +fractional pieces of a physical array can be routed at zero cost. Its exact +replication factors can be impractically large, which is acceptable for a +fixed finite supplier existence statement but must be disclosed. + +## 5. Why some fixed N has the required saving + +The independent audit sharpened this step to a direct count of paid leaves. +It does not require a running-time comparison between a RAM flow and native +tapes. Let `L(n)=P_n/B_n`, let `w_s=S_s/S`, and let `x_e` be the exit counts +normalized by the number S of source arrays. The actual integer compiler +satisfies + +``` +L(n) = sum_s w_s L(n-s) + sum_e x_e L(e), +sum_s w_s = 1, +sum_e x_e e^tau = sum_s w_s s^tau. +``` + +The last equality follows by canceling every internal matched job in the +exact tau-potential balance. The source ranks satisfy `n/m0`, concavity gives + +``` +n^z0 - sum_s w_s (n-s)^z0 >= eta * sum_s w_s s^z0. +``` + +Indeed, for `t=s/n` in `[1/m,1]`, +`1-(1-t)^z0 >= z0*t >= eta*t^z0`. For every sufficiently large n the +exit coefficient is less than `eta/2`. Every complement and exit has +smaller rank than n, so strong induction on the exact recurrence proves +`L(n)<=A*n^z0`, with finite A chosen to cover the smaller ranks. Eventually +`L(N) 25,600,000*N^5, odd, avoiding every fixed native/matcher denominator and rank witness", + "row_reserve": "For the new finite N and role/word constants, log_q S(e,w)=O(w log e); w=ceil(e^(3/1000)).", + "saving_after_cover": { + "decimal": "0.00275", + "rational": "11/4000" + }, + "saving_before_cover": { + "decimal": "0.00276", + "rational": "69/25000" + } + }, + "paid": { + "1": 9261, + "2": 9394, + "3": 553, + "4": 308, + "5": 714, + "6": 77, + "7": 1465 + }, + "precompilation_saving": { + "decimal": "0.00276", + "rational": "69/25000" + }, + "strict_mixed_margin": { + "lower": "0.79440312869001840349907639031552322", + "upper": "0.79440312869001840349907639031552323" + }, + "targets": { + "22": 444, + "50": 222, + "8": 3073 + }, + "uniform_template_definition": "First finite N in the specified exact compiler for which P_N/B_N < N^(1-C). Existence and native closure require the separate written proofs." + }, + "complex": { + "margin_at_004": { + "lower": "-163.47161919550931457258600794984177083", + "upper": "-163.47161919550931457258600794984177082" + }, + "paid": { + "1": 17623, + "2": 5065, + "3": 1738, + "4": 714, + "5": 254 + }, + "precompilation_saving": { + "decimal": "0.002304", + "rational": "36/15625" + }, + "strict_mixed_margin": { + "lower": "0.10548315917752229262732557699459137", + "upper": "0.10548315917752229262732557699459138" + }, + "targets": { + "25": 448, + "57": 224, + "6": 192, + "7": 56, + "8": 93, + "9": 1229 + }, + "uniform_template_definition": "First finite N in the specified exact compiler for which P_N/B_N < N^(1-C). Existence and native closure require the separate written proofs." + } + } +} diff --git a/research/log-potential-template-ranks/vendor/OUTER-TRANSFER-AUDIT.md b/research/log-potential-template-ranks/vendor/OUTER-TRANSFER-AUDIT.md new file mode 100644 index 0000000000..e8b7ef8956 --- /dev/null +++ b/research/log-potential-template-ranks/vendor/OUTER-TRANSFER-AUDIT.md @@ -0,0 +1,426 @@ +# Independent transfer audit for the conditional kappa = 0.0023 construction + +Status: the changed supplier interfaces close under the inherited analytic, +ordered-movement and fixed-tape hypotheses. This is a mathematical audit +with independently generated exact receipts, not a formal proof certificate +or an unconditional integer-multiplication theorem. Substantial OpenAI +assistance. Apache-2.0. + +The conclusion uses the **actual complete p3 programs**, the finite native +precompiler, the delayed BIT cover, fresh precision and stock constants, +and the nearly critical outer assembly. It does not infer a multiplication +bound from a favorable recursive-cost histogram alone. + +## 1. Conclusion and quantitative separation + +The independently checked conditional outer target is + +``` +kappa = 23/10000 = 0.0023. +``` + +Every one of the nine retained outer cost rows has a strictly larger saving. +The smallest saving is `0.00230197698`; its margin above the declared target +is exactly `98849/50000000000 = 0.00000197698`. + +The construction is deliberately separated into the following interfaces. + +| Interface | Independently checked result | +| --- | --- | +| Complete complex mixed unit | 2,242 arbitrary productive fields, one uncredited owned center; full physical phase, owner and scalar bill | +| Complete BIT mixed unit | 3,739 arbitrary productive fields, one uncredited owned center; 63 paid calls on copied-center data | +| Finite complex uniform program | Fixed rank `N=2^276540184361`, saving `0.002304` | +| Finite BIT uniform projector program | Fixed rank `N=2^6552928412`, saving `0.002760` before its cover | +| Covered BIT uniform program | Saving `0.002750`, including every bad-class fallback | +| Ordinary arbitrary-width BIT | Saving `27418653797/10^13 = 0.0027418653797`; conservatively admit `0.0027` | +| Effective outer supplier saving | `0.0023025` | +| Completed selected-axis complex layer | Linear semantic guard `C0*d`, with a new computable fixed `C0` | +| Conditional outer result | `kappa=0.0023` | + +The ranks above are exact compressed integers, not suggested search bounds. +The winning words are defined by finite integer algorithms at those ranks. +Their enormous instruction lists and constants have not been materialized. +The fully materialized rank-57 complex and rank-50 BIT examples are useful +ownership/complement tests; neither small example attains the limiting +savings in this table. + +## 2. The finite bridge preserves complete jobs and actual ownership + +The reviewed native precompilation theorem is +[`../architecture/FINITE-PRECOMPILATION.md`](../architecture/FINITE-PRECOMPILATION.md). +Its integer lockstep flow is based on Jacob Alan Sussman's Theorem 1G; +the independent chronological reconstruction and challenge cases are in +[`AUDIT.md`](AUDIT.md) and `FINITE-DAG-AUDIT.json`. + +At a fixed ambient rank `n`, every productive source is a complete arbitrary +array on all `n` coordinates. Its designated rank-`s` job is supplemented +by a paid complementary rank-`n-s` job. The complement is run first. +The completed mixed word then supplies the designated endpoint, and the +product is the full transform. This uses autonomy of the completed endpoint; +it does not require the complement to commute with intermediate operations +of the mixed circuit. + +All normalized source counts and all occurrences of lower-rank batches are +cleared by one explicit finite integer multiplier. An ordered batch uses +distinct physical fields. Each recursive demand occurs strictly after its +input exists and before its parent continues; every recursive rank is +smaller. The independent graph audit rejects aliased input slots, incomplete +batch clearing and cycles. It includes paid demands on owned fields. + +A parent-owned copied center can be passed as one arbitrary input to a +lower-rank unit. Correlation with another array is harmless: the child +identity holds for every assignment of its distinct physical input slots. +The parent copy remains present until the actual call returns, and its +eventual erasure is legal only after the prescribed restoration. A fresh +child center has a separate owner tag. No copied center becomes another +productive source, and simultaneous suspended centers are not merged into +one bank merely because they have the same recursion depth. Conservatively +allocate one full center per finite mixed-unit instance and charge every +initialization, pass and erasure. These are fixed constants of the compiled +uniform word. + +### Explicit termination and one specified winning rank + +Let `L(n)=P_n/B_n` be the exact average number of rank-one leaves per +productive full-rank source, including complements and owned-field calls. +For the complex case the strict mixed test is at saving `0.002305`; for BIT +it is at `0.002769`. Put `t=1-C_test`. Cancellation in the finite flow gives +an inequality, not an assumed equality: + +``` +sum_e x_e*e^t <= sum_s w_s*s^t, +L(n) = sum_s w_s*L(n-s) + sum_e x_e*L(e), +sum_s w_s = 1. +``` + +The separate positive rank-one surplus gives `L(n)<=n` by induction. With +source ranks `n/m0`. Concavity shows that the source complements leave at least +`eta*sum_s w_s*s^z0`, where `eta=z0*m^(z0-1)>1/4`. Choose + +``` +H0 = ceil((3+4*delta)/(h*delta)), +n0 = 2^H0, +A = n0^(1-z0). +``` + +Then the exit coefficient is at most `1/8` for every `n>=n0`. The base +bound `L(n)<=n` covers `n<=n0`; strong induction gives `L(n)<=A*n^z0` +for every rank. Finally + +``` +H1 = floor(H0*(1-z0)/(z-z0))+1, +N = 2^H1 +``` + +ensures `L(N) -> i^(a+q(x)) |M*x+b>` lifts to the same address recipe on each column, +with phase `a*f+sum_j q(x_j)` modulo four. Complete spectator coordinates +remain present. This substitutes physical operators in the already checked +role-level linear identity; it does not assume tensor power is additive. +The final normalizers make every productive endpoint the canonical +positive tensor job. Coordinate permutations place these on any required +disjoint axes. Remainder axes at an arbitrary width receive individual +paid kernels and remain completed spectators of the lifted word. + +[`FINITE-TEMPLATE-CLOSURE.md`](FINITE-TEMPLATE-CLOSURE.md) supplies fresh +coefficient, owned-space, row and precision constants. In particular, for +the completely expanded word with rank `N`, productive width `W`, rank-one +paid count `P`, unit count `U`, and conservative owned count `O=U`, put + +``` +Z = W+O, +G = 1494376*U, +E = 64*(Z+N+P+G+1)^3, +B = P+E, +C0 = 32*N*B^2, +C1 = 1. +``` + +The completed-child semantic recurrence is +`A(e)<=A(floor(e/N))+P*floor(e/N)+E`. It gives `A(e)<=2B*e`; completed +disjoint outer pieces and retained phases fit below `C0*d`. This measures +completed returned values without rounding or re-encoding children. +The large temporary values inside a child are not also unfinished parent +operands. All storage stays on one common fine grid. + +For `d<=c*p^epsilon` with `epsilon<1`, the explicit threshold in that note +ensures `C0*d<=p/4`, hence total component width at most `2p`. The new `C0` +may be enormous, but it is fixed. There is no inherited small numerical +guard constant and no appeal to the obsolete pathwise precision exponent. + +## 4. BIT uses one delayed ambient cover and one common weight + +The argument reviewed is +[`../bit/DELAYED-COVER-BRIDGE.md`](../bit/DELAYED-COVER-BRIDGE.md). +`BIT-BRIDGE-AUDIT.json` supplies a separate exact implementation audit. +The essential order is to precompile the entire finite projector program +first, and only then apply a single whole-ambient `GL_N` cover and external +weight. Internal jobs are not prematurely lowered to differently weighted +canonical children. + +For a rational idempotent `P` in ambient dimension `N`, write + +``` +D_P = [[I-P, P*C_N], [C_N*P, I-C_N*P*C_N]], +Q_S = diag(S, C_N*S*C_N). +``` + +Direct multiplication gives `Q_S D_Q Q_S^-1=D_(SQS^-1)` and +`D_P D_(I-P)=D_I`, including nonsymmetric projectors. Equal-rank rational +idempotents admit a fixed rational matcher `S` by matching image and kernel +bases. After the finite program is fixed, choose an odd prime avoiding all +its finitely many denominators, determinants and rank witnesses. All lifts +use these same rational matrices, so this choice is independent of the +eventual column multiplicity. + +Use the full cover `g in GL_N(Z/q^w Z)`. To match a parent request `P` to a +child endpoint `Q`, route that child's complete role fiber by `g -> gS`, +execute the entire child, and undo the route. Its autonomous endpoint is +exactly `D_(gPg^-1)`. Separate target roles may use separate matchers: each +route is a bijection of a full fiber carrying arbitrary data. Native port +charts and local helper ownership remain inside the schematic program; +they are not silently discarded when the ambient dimension grows. + +This is a paired whole-job construction. It does not implement arbitrary +isolated dense address maps by renaming rows, and it does not assume a +generic RAM-to-tape simulation. + +The inherited weight `A` is common to all fresh roles and independent of +the current complete cover field. Consequently `Lambda_A=diag(A,I)` +commutes with every internal role route and every pointwise scalar/COPY +operation. The completed source/complement endpoint is therefore the +required weighted full interchange. Only final rank-one leaves are lowered +to weighted canonical children. Their pivot weights depend on this parent +cover row, which is ancestor data when the child's fresh fields are exposed. +Different leaves can have different weights without violating the common +weight requirement inside any one child. + +At `f` columns the inherited reversed pairing is essential. The actual +lift uses `P tensor I_f` with full tail reversal `C_(Nf)`, or equivalently +conjugates the straightforward tensor lift by the blockwise `C_f` reversal. +The independent audit checks this on nonsymmetric rational projectors and +rejects dropping that reversal. It also checks arbitrary common external +weights depending on axes and columns. Current-cover-dependent weights +remain forbidden. + +The independent native replay covers all 636 rational frames, 2,386 nested +MOVE pairs, both 661-column local words, 111 ports and 666 embedded charts, +3,073 helper owners, and all 63 paid COPY-center calls. The rank-50 full-job +example has `W=3739`, `P=186725` and surplus `50*3739-186725=225`. +Additional checks include nonsymmetric rational matchers, a genuine +non-field ring, and 7,776 inverse/carry tests over `GL_2(Z/9Z)`. The last +tests retain all q-adic digits of the matcher; dropping its higher digits +has an explicit failing control. + +### Paid cover, atom conversion, and ordinary endpoint + +Right multiplication on `g=g0+qG1` is a finite low-type permutation plus a +fixed affine high-matrix map with its correct carry. The retained native +cover-routing lemma charges it as `O(V*w^(1-a_old))`. The finite number of +routers changes the constant, not this exponent. All bad generic classes +receive their actual fallback. With the explicit choice + +``` +q > 25,600,000*N^5 +``` + +and the finite denominator exclusions, the complete covered moment is at +most `400001/400002<1`. This includes the full fallback bill without +subtracting the good-class calls or assuming bad classes are independent. + +Use atom width `w=ceil(e^0.003)` and the retained old ordinary saving +`a_old=384599/10^10`. The resulting saving is + +``` +(1-0.003)*0.002750 + 0.003*a_old + = 27418653797/10^13 + > 0.0027. +``` + +The linear adapters are paid because `0.003` exceeds this saving. The +borrowed row stock satisfies `log S(e)=O(e^0.003 log e)` and is lower order +because `0.003<1-a_BIT`. Its complete borrowed field is restored. Padding +of full rows is performed once for the whole invocation and removed after +the completed endpoint. Numeric padding to atom lengths costs only a +fixed `q`-dependent factor. + +The ordinary wrapper uses two completed reversed calls and three charged +bank additions, in chronological order: + +``` +D <- D-H; F_n; D <- D+H; F_n; D <- H-D. +``` + +For `(H,D)` this gives successively `(H,D-H)`, `(C(D-H),CH)`, +`(C(D-H),CD)`, `(D,D-H)`, `(D,H)`. Thus it really supplies the ordinary +interchange, at constant multiplicative overhead and `O(Vn)` extra work. +No unshown batch or free half-swap is required. + +## 5. The changed row reserve fits the support-local outer wrapper + +This is an essential functional obligation, not another numerical moment +test. The applicable retained wrapper is the global support-local wrapper +in `vendor/pr1673/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md` and its +`SUPPORT-ADVERSARIAL-AUDIT.md`, under the current outer package. Its completed +supplier calls cover the **whole global dyadic tensor**. Calling separately +inside fixed coarse-label microboxes would not satisfy the interface. + +For a phase with `h` selected bits, take `G=4*ceil(log2 p)+6` and complete +neighborhoods of width `K=128G`, one inside each selected original axis. +The axis length grows like `p^(1-epsilon)`, so every fixed multiple of +`log p` fits eventually. Exposing the complete neighborhoods moves at most +`2hK` bit positions. Native binary matrices have fixed rank, so their +column lifts factor into finitely many parallel row additions on these +selected bits. Unit phases have fixed formulas of the same selected-bit +support. They do not introduce dependence on unrelated coarse labels. + +Reserve whole selected chunks for the two front controls, back control and +row prefix. **Do not first transform their selected bits.** The completed +active invocation is identity on every reserved coordinate for arbitrary +contents; those selected-axis kernels can be completed in later shrinking +phases. The finite guard condition used by the retained router is directly +satisfied by `K=128G`; no claim is made that this constant ratio satisfies +the older, stronger wording `K/log p -> infinity`. + +The new BIT stock cannot simply be inserted into the old statement +`O(log h)` for all nested reserves. Its own ordinary full-field interface +supplies its rows internally. Alternatively, the following conservative +external product bound explicitly covers simultaneous stock. A BIT call +has width at most `C*h*(log p)^2`. Its logarithmic stock is +`O(h^0.003*(log p)^(2*0.003+1))`. Including a further `O(log h)` nesting +factor and the complex stock gives, after enlarging one fixed constant, + +``` +q0(h,p) <= C*(log2 h + h^0.003*(log2 p)^3 + 1) +``` + +reserved complete chunks. This bound retains the **product** of stock +requirements; using their maximum would be invalid. Since `0.003<1`, there +is an explicit fixed polylogarithmic threshold `H(p)` above which +`q0(h,p)+O(1)<=h/64`. For example one may enlarge a fixed multiple of +`[1024*C*(log2 p)^3]^(1/(1-0.003))` to cover the logarithmic term and all +finite-template base thresholds. Consequently + +``` +R(h) <= 3h/128 + q0(h,p) + O(1) <= h/16 +``` + +for all sufficiently large active phases. The remaining `h<=H(p)` bits are +handled individually in `O(V*polylog p)` time. Thus successive active +widths shrink by at least a factor 16, and their sublinear costs sum to a +constant multiple of the first phase's cost. + +Each phase pads its complete row count once by a factor below two. Its +completed endpoint preserves the row coordinate, so appended zero rows +can be deleted before inverse exposure and before the next phase. This +prevents an accumulating factor of two per phase. The exposure is restored +before any next diagonal depending on coarse labels is applied. + +The support router's additional control reservoirs occupy +`O(h*(log p)^2)` positions and fit the full `Theta(p)`-bit tensor because +`group_beta<1`. A complete untouched `log^2 p` suffix is chosen and placed +first for short-record grouping; all subsequent reservoirs and routers +stay in its complement. The retained full-span route handles the bounded +regime where this gap argument fails. A single original axis is never +asked to hold all of the `hG` control bits. + +## 6. Fresh constants satisfy every changed outer interface + +The actual parameter point is in +[`../controller/OUTER-PARAMETERS.json`](../controller/OUTER-PARAMETERS.json). +The independent audit reproduces its nine cost rows directly, without +importing either outer ledger. It also checks the functional inequalities +needed above, including + +``` +epsilon = 0.99999 < 1, +group_beta = 0.99997 < epsilon, +1-epsilon-r0 > 0, +1-(2*xi-2)-r0-group_beta > 0, +group_beta*(1-0.003) > 0. +``` + +The first two absorb every new fixed semantic, movement and row constant; +the next two retain the precision and fine-prime spare powers. The last +ensures the changed BIT reserve is sublinear in the active grouped width, +even after the polylogarithmic factors above. The stopped supplier's +internal and leaf exponents are strictly below the selected `lambda` and +`lambda_prime`, respectively. The effective BIT saving is below both the +actual ordinary BIT saving and the selected complex saving. + +Every compiled-word constant, rational denominator and description degree +is fixed before the input length varies. Polynomial description/preparation +costs are absorbed by the retained complete superpolynomial record fibers +when `epsilon<1`, after increasing an effective threshold. A finite program +on fixed tapes remains a native program on fixed tapes; this argument does +not hide random-access gathering inside the coefficient allowance. + +The nearly critical halo calculation uses the retained explicit-metadata +branch with `halo_power=48` and `core_power=128`. It does not use the old +`K0^2=o(p)` shortcut, which is unavailable near this parameter point. The +boundary exponent uses the exact Strassen comparison `7^16<2^45`; no new +unstated stable-matrix algorithm is required. + +The outer analytic decomposition, ordered movement implementations, +fixed-tape model, prime padding, and exact integer recovery are the same +conditional hypotheses as in the reviewed outer package. The changed +mixed-job, native adapter, weighted-child, row-stock and semantic-precision +obligations have been supplied explicitly here. The conclusion is therefore +a source-bound **conditional research result** at `kappa=0.0023` under +those inherited hypotheses. It is not a claim of practical constants or of +an unconditional theorem. + +## 7. Reproducible independent checks + +From the repository root: + +```sh +python3 -B research/kappa-rebuild/transfer-audit/bit_bridge_audit.py +python3 -B research/kappa-rebuild/transfer-audit/outer_transfer_audit.py +``` + +The first binds the independent BIT checks to the exact current native and +bridge sources. The second uses its own 256-bit directed rational grid, +finite-series logarithm/exponential bounds, exact rank comparisons, and +fresh outer equations. `OUTER-TRANSFER-AUDIT.json` records all source hashes, +strict intervals, compressed ranks, nine outer savings and functional gaps. +The directory manifest binds this written audit and the complete source set. diff --git a/research/log-potential-template-ranks/vendor/P3-NATIVE-COVER.json.gz b/research/log-potential-template-ranks/vendor/P3-NATIVE-COVER.json.gz new file mode 100644 index 0000000000..51a09b3952 Binary files /dev/null and b/research/log-potential-template-ranks/vendor/P3-NATIVE-COVER.json.gz differ diff --git a/research/log-potential-template-ranks/vendor/check_ledger.py b/research/log-potential-template-ranks/vendor/check_ledger.py new file mode 100644 index 0000000000..d3b6149c5c --- /dev/null +++ b/research/log-potential-template-ranks/vendor/check_ledger.py @@ -0,0 +1,260 @@ +#!/usr/bin/env python3 +"""Exact ledger for fine-prime padding (PR1786, chafreaky / Chafik Boukhalfa, with Tim Trudgian's prime theorem) at the free point epsilon = 1 - (1025/1024)*10^-(DIG+80), explicit Strassen boundary, retuned to the fixed-grid maximum kappa = C - 1/FLOOR - BACKOFF. + +Adapted from PR1786's ledger, itself adapted from PR1731's cost ledger, credited to Jeremy Kothe et al. and +Vlado Vojdanovski (PR1673); uses PR1758's gauge-free chirp and per-visit tag +accounting. New source-prime, coefficient-setup and halo lemmas are in +FINE-PRIME-PADDING.md. Finite arithmetic does not prove the all-size theorem. +""" +from fractions import Fraction as Q +from decimal import Decimal, localcontext +from pathlib import Path +from math import factorial +import hashlib, json, sys +sys.set_int_max_str_digits(0) + +if not __debug__: raise RuntimeError('Assertions must be enabled') +HERE=Path(__file__).resolve().parent +WORK=HERE.parent +SPEC=WORK/'new/SPEC.json' +CLAIM=WORK/'CLAIM.json' +BJ=json.loads((HERE/'B.json').read_text()) +spec=json.loads(SPEC.read_text()) +# Free strict slacks of the PR1673 proof (retuned in this package, see RETUNED-SLACKS.md); every one only needs to be > 0. +DIG=spec['outer_refinement']['endpoint_digits'] # the supplier endpoint is certified to 10^-DIG (accept at the endpoint, reject at endpoint + 10^-DIG); every slack sits 10 digits below +# Fixed-grid maximum (PR2180 / PR2161, dataisfire; proof PROOF-GRID-MAX.md): the free gaps shrink together to R0 = 10^-(DIG+80); grid, backoff and certified endpoint are unchanged. +R0=Q(1,10**(DIG+80)); ZETA=R0/100; SLACK=R0; GAP=R0; STOP=R0/10**6 +FLOOR=10**(DIG+46); BACKOFF=Q(1,10**(DIG+22)); B_GAP=R0 +# Fine prime padding: theta is between 1/(4p^2) and 1/(2p^2-1). +# Online chirp guard beta+2*xi-2<1; coefficient setup uses O(p^2 log p) bits. +# epsilon = 1 - DELTA_E is a FREE parameter (outer/FINE-PADDING-COMPOSITION.md sec. 2): every row is strictly satisfied for every DELTA_E > r0 = 10^-(DIG+80); beta = 1 - 3 DELTA_E lies in the admissible window +# [1 - DELTA_E (1 + 1/q), 1 - 2 DELTA_E). DELTA_E = (1025/1024) r0 keeps the gamma spare power 1-eps-r0 = r0/1024 > 0 and puts C - eps*q below 1/FLOOR (PROOF-GRID-MAX.md). +DELTA_E=Q(1025,1024)*R0 +EPS=1-DELTA_E +BETA=1-3*DELTA_E +THETA_POWER=Q(2) +HALO_POWER=48 +CORE_POWER=128 +STRASSEN_TAU=Q(45,16) +KAPPA_1828=Q('0.0016797549561255445213356709939207025769983114385025802954603275201627999999999999999999999999979966404900867489109573286580121585') # exact kappa of rohanarun's PR1828 (slack refinement of PR1800 at 1e-96), from its body +KAPPA_1839=Q('0.0016797549561255445213356709939207025769983114385025802954603275201628645482603256388263049999999997996640490086748910957328658012158594') # exact kappa of PR1839 (previous package: 1e-90 endpoint) +KAPPA_1875=Q('0.0016797549561255445213356709939207025769983114385025802954603275201628645482603256388263056561328446322744513169085862209720704481201654121427713006366929567157349625273906229277148454180995537563371124755588139767841405530386745578819565618798006892541712197674874836946756930569827889227573192555649999999997996640490086748910957328658012158594') # exact kappa of rohanarun's PR1875 (1e-300 endpoint), from its body +KAPPA_1876=Q('0.001679754956125544521335670993920702576998311438502580295460327520162864548260325638826305656132844632274451316908586220972070448120165412142771300636692956715734962527390622927714845418099553756337112475558813976784140553038674557881956561879800689254171219767487483694675693056982788922757319255565606685566411725238449650999339827075715283714270157705762309226038611771955655377501414652136546310799999999999999999997996640490086748910957328658012158594846') # exact kappa of rohanarun's PR1876 (1e-400 endpoint), from its body +KAPPA_1897=Q('0.001679754956125544521335670993920702576998311438502580295460327520162864548260325638826305656132844632274451316908586220972070448120165412142771300636692956715734962527390622927714845418099553756337112475558813976784140553038674557881956561879800689254171219767487483694675693056982788922757319255565606685566411725238449650999339827075715283714270157705762309226038611771955655377501414652136546310881185746917580802513640545967852810801680966856133978576162943792322682482152988532923811998938861379689883167389728443314312230815059559906903773756886872476136837071871203030423643505345473735135533') # exact kappa of M6LI's PR1897 (1e-500 grid), from its body +KAPPA_1786=Q('0.0016797547881500489087805478664999999999999999999999999999999998000000199999') # exact kappa of chafreaky's PR1786 ledger (EXPECTED-BALANCE.json), headline 0.001679754788150048 +KAPPA_PKG5=Q('0.001677992607205282520732088774830808372222877897034109604209719298829805473412451530867883424937597') # previous package (rectangular k=2, tau_eff=2.2500351) +KAPPA_PKG4=Q('0.0016778199023144364336310551358776001013829401215770658599799349282716974076737897457922714197448847') # previous package (radix union schedule, square boundary tau=2.372864) +KAPPA_1712=Q('0.0016776417313433545642517275958639984231708545722735432722117400060454625429077941422798526440584702') # pkg of PR1712 (Le Gall tau=12/5, old union row) +KAPPA_1699=Q('0.001677641731343354564251058287063644749065568493') # exact kappa of PR1699's ledger (Chafik Boukhalfa), same supplier profile +certified_complex=Q(spec['expected']['complex_lower']) +bit=Q('0.001733427039589844234749') +# Keep short independently checkable decimals strictly inside both endpoints. +b=certified_complex-B_GAP # strictly inside the certified supplier endpoint; B.json carries the same exact value +assert b==Q(BJ['b']) +q=b-GAP +a=(q+b)/2 +online=Q(spec['expected']['kappa']) +old=Q('0.001673360105405778') +assert b0 +assert m==73 and W==896*T and W==BJ['live'] +EXPECTED_PROFILE={int(k):v for k,v in BJ['profile'].items()} +assert profile==EXPECTED_PROFILE + +GB=int((DIG+130)*3.3220)+16 # enclosure grid 2^-GB, about 50 digits below the slacks +ONE=1<=2:x/=2;k+=1 + lo,hi=unit_log(x) + return down(lo+k*ln2[0]),up(hi+k*ln2[1]) +def exp(x): + assert 0<=x>GB)//j;th=_cd(-((-th*xu)>>GB),j);sl+=tl;sh+=th + tn=_cd(-((-th*xu)>>GB),EN) # x^EN/EN! (rounded up); the tail is at most twice this + return Q(int(sl),ONE),Q(int(sh+2*tn+2),ONE) +def moment(endpoint): + lo=hi=Q(0) + for r,n in profile.items(): + l,h=log(Q(m,r)); weight=Q(n*r,m*W) + lo+=weight*exp(endpoint*l)[0] + hi+=weight*exp(endpoint*h)[1] + return down(lo),up(hi) + +native=moment(b) +assert native[1]<1 +b_up=Q(BJ['b_above_endpoint']) +assert b_up>certified_complex and moment(b_up)[0]>1 # a larger test endpoint is rejected + +def ledger(kind, *, q_=q, zeta=ZETA, slack=SLACK, + old_scan=False, full_gauge=False, full_key=False, old_union=False, old_theta=False, old_linear=False, old_tag=False, + eps_=EPS, beta_=BETA, tau_eff=STRASSEN_TAU, halo_power=HALO_POWER, core_power=CORE_POWER): + r=R0; stop=STOP + # Existing explicit Strassen format, 7^16<2^45; c=3/32. + # Union: radix-distributed schedule (outer/UNION-SCHEDULE.md, new in this package): row exponent eps+1/2-xi. The boundary row binds with main; the Gaussian row has slack at this explicit point. + c=(3-tau_eff)/2 + eps=eps_; beta=beta_ + xi=eps*(1+q_)-c+slack + saving=eps*q_ + # Deliberate strict gap (BACKOFF) after decimal truncation to the FLOOR grid. + kappa=Q((saving*FLOOR).__floor__(),FLOOR)-BACKOFF + # kappa is derived, not silently asserted to equal an expected decimal. + tau=1-a; sigma=1-b + internal=tau+(1-stop)*max(sigma-tau,Q(0)) + leaf=sigma+stop*(1-sigma) + lam=1-(q_+a)/2 + key=beta+1-eps + margins={ + 'main_transform':saving, + 'global_coordinate_router':a, + 'fused_gaussian':1-eps+q_*beta, + 'group_bit_router':1-eps+a*beta, + 'group_scans':1-eps+beta, + 'boundary_algebraic_matrix':c+xi-eps, + 'sparse_union_movement':xi+Q(1,2)-eps, + 'polynomial_products':eps, + 'microbox_face_corrections':1-(eps+beta+halo_power-core_power+2), + } + if old_union:margins['old_g_factor_union_row']=1-eps-beta-Q(1,2)+xi + if old_scan:margins['old_per_axis_scan']=1-eps + if full_key:margins['unnecessary_full_key_sort']=margins['sparse_union_movement']-key + checks={ + 'actual_bit_above_effective':bit-a, + 'complex_above_effective':b-a, + 'q_positive':q_, 'complex_endpoint':b-q_, + 'q_below_effective':a-q_, 'stop_positive':stop, + 'stop_below_one':1-stop, + 'leaf_saving_above_effective':(1-stop)*b-a, + 'q_below_internal':1-internal-q_, 'q_below_leaf':1-leaf-q_, + 'lambda_above_tau':lam-tau, 'lambda_above_sigma':lam-sigma, + 'lambda_above_internal':lam-internal, + 'lambda_prime_above_lambda':1-q_-lam, + 'lambda_prime_above_leaf':1-q_-leaf, + 'epsilon_positive':eps,'epsilon_below_one':1-eps, + 'cap_above_band':xi-Q(1,2),'cap_below_cell':eps-xi, + 'group_positive':beta,'group_below_dimension':eps-beta, + 'support_router_span':1-beta, + 'group_gauge_power_slack':1-(2*xi-THETA_POWER)-r-beta, + 'actual_logarithmic_group_guard':1-(2*xi-THETA_POWER)-beta, + 'global_gamma_power_slack':1-eps-r, + 'actual_logarithmic_gamma_guard':1-eps, + 'alpha_logarithm_absorption':r, + 'group_key_fits_record':1-key, + 'membership_arithmetic_fits_record':1-beta-2*(1-eps), + 'microbox_halo_volume':core_power-halo_power-beta, + 'positive_layout_slack':slack, + 'short_record_fallback':eps-a, + 'improvement_over_online_final':kappa-online, + 'improvement_over_previous_local_final':kappa-old, + 'complex_below_one_over_32':Q(1,32)-b, + } + checks['strassen_integer_power_gap']=Q(2**tau_eff.numerator-7**tau_eff.denominator) + checks['theta_positive_polynomial_power']=THETA_POWER + checks['cap_below_phase_cell_power']=THETA_POWER-xi + checks['halo_covers_generic_inverse_radius']=Q(halo_power-43) + checks['union_tag_work_per_visit_fits_record']=1-beta + checks['union_header_fits_record']=1-beta + checks['source_axis_superpolynomial']=1-eps + checks['improvement_over_pr1786']=kappa-KAPPA_1786 + checks['improvement_over_pr1828']=kappa-KAPPA_1828 + checks['improvement_over_pr1839']=kappa-KAPPA_1839 + checks['improvement_over_pr1875']=kappa-KAPPA_1875 + checks['improvement_over_pr1876']=kappa-KAPPA_1876 + checks['improvement_over_pr1897']=kappa-KAPPA_1897 + checks['improvement_over_pr1758']=kappa-Q('0.001679745508802299051546533685199973672313473419790800679752457380932784242972585600630181672224983') + checks['improvement_over_pr1699']=kappa-KAPPA_1699 + checks['improvement_over_pr1712']=kappa-KAPPA_1712 + checks['improvement_over_previous_package']=kappa-KAPPA_PKG4 + checks['improvement_over_pkg_k2']=kappa-KAPPA_PKG5 + if full_gauge:checks['unrecentered_group_gauge']=1-THETA_POWER-r-beta + if old_theta:checks['old_theta_chirp_guard']=1-(2*xi-eps)-r-beta + if old_linear:checks['old_linear_guard']=1-xi-r-beta + if old_tag:checks['old_union_tag_2beta']=1-2*beta + # Main-binding family invariant (PR2180): the Gaussian saving stays above the main saving. The fixed kappa grid (FLOOR) is coarser than the free gaps, + # so the *_above_kappa rows alone would no longer exclude a beta outside the main-binding window; this row is delta*(1-2q) > 0. + checks['gaussian_above_main']=margins['fused_gaussian']-saving + checks.update({n+'_above_kappa':v-kappa for n,v in margins.items()}) + assert margins['boundary_algebraic_matrix']==saving+slack + assert margins['sparse_union_movement']==saving+slack+(tau_eff-2)/2 + return {'kind':kind,'kappa':kappa,'epsilon':eps,'xi':xi,'beta':beta, + 'q':q_,'a':a,'r0':r,'zeta':zeta,'slack':slack, + 'margins':margins,'strict_checks':checks} + +def encode(x): + if isinstance(x,Q): + with localcontext() as c: + c.prec=DIG+200 + return {'rational':str(x),'decimal':str(Decimal(x.numerator)/Decimal(x.denominator))} + if isinstance(x,dict):return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)):return [encode(v) for v in x] + return x + +rows={};controls={} +for kind in ['struct_boundary_radix_union']: + row=ledger(kind) + assert all(v>0 for v in row['strict_checks'].values()) + assert min(row['margins'].values())==row['margins']['main_transform'] + # fixed-grid maximum: C*FLOOR is an integer and 0 < C - eps*q < 1/FLOOR, so floor(FLOOR*eps*q)/FLOOR = C - 1/FLOOR exactly and kappa attains the grid/backoff ceiling + assert (certified_complex*FLOOR).denominator==1 and 0= 1/(4 p^THETA_POWER)), an exponential factor <= p^2 eventually, +# alpha^5 polylogarithmic; a further half power is allowed for the polylogarithmic and bounded-constant factors of the augmented matrices. The umbrella must exceed that budget. +UMBRELLA_POWER=10 +def umbrella_margin(theta_power):return UMBRELLA_POWER-(2*theta_power+2+Q(1,2)) +assert umbrella_margin(THETA_POWER)>0 and umbrella_margin(Q(15,4))<=0 # control: the umbrella would fail silently for THETA_POWER >= 3.75 +HALO_UMBRELLA={'umbrella_power':UMBRELLA_POWER,'theta_power':THETA_POWER,'exponent_budget':2*THETA_POWER+2+Q(1,2),'margin':umbrella_margin(THETA_POWER),'fails_from_theta_power':Q(15,4)} +out={'status':'PASS_FINE_PRIME_PADDING_EXACT_ARITHMETIC', + 'scope':'Conditional fine-prime padding composition. Fresh native admission is required by verify.py. The cited prime theorem, written gauge-free theorem and inherited all-size interfaces are not proved by this arithmetic. No independent human review is claimed.', + 'geometry_changes':{'theta_power':THETA_POWER,'halo_power':HALO_POWER,'core_power':CORE_POWER,'matrix_exponent':STRASSEN_TAU}, + 'halo_umbrella':HALO_UMBRELLA,'complex_lower_short':b,'complex_lower_pinned':certified_complex, + 'native_moment':native,'profile':profile,'m':m,'W':W, + 'online_final_kappa':online,'rows':rows,'rejecting_controls':controls, + 'pr1673_kappa':Q('0.001677160151714381'),'improvement_over_pr1673':rows['struct_boundary_radix_union']['kappa']-Q('0.001677160151714381'), + 'source_sha256':{p.relative_to(WORK).as_posix():hashlib.sha256(p.read_bytes()).hexdigest() for p in [SPEC,CLAIM]}} +(HERE/'LEDGER.json').write_text(json.dumps(encode(out),indent=2)+'\n') +print(out['status']) +for name,row in rows.items(): + print(name,'FINAL KAPPA',encode(row['kappa'])['decimal'], + 'positive checks',len(row['strict_checks']), + 'gain over online',encode(row['kappa']-online)['decimal']) diff --git a/research/log-potential-template-ranks/verify.py b/research/log-potential-template-ranks/verify.py new file mode 100644 index 0000000000..2e61e38575 --- /dev/null +++ b/research/log-potential-template-ranks/verify.py @@ -0,0 +1,369 @@ +#!/usr/bin/env python3 +"""Exact premises of README.md's logarithmic leaf-count majorant. + +Leaf arithmetic is separately implemented. The pinned outer ledger function +is executed as a second arithmetic oracle; this is not native/outer admission. +zxv, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import ast +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.dont_write_bytecode = True + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +@lru_cache(None) +def log_bounds(n): + """ln(n): rational 2*atanh series after binary range reduction.""" + need(isinstance(n, int) and n >= 1, 'positive integer logarithm') + + def series(x): + u = (x-1)/(x+1) + power, total, count = u, Q(0), 80 + for j in range(count): + total += 2*power/(2*j+1) + power *= u*u + tail = 2*power/((2*count+1)*(1-u*u)) + return total, total+tail + + k = n.bit_length()-1 + a, b = series(Q(2)) + c, d = series(Q(n, 2**k)) + return k*a+c, k*b+d + + +def exp_bounds(x): + """Positive Taylor terms with a geometric bound on the omitted tail.""" + need(0 <= x < 1, 'exponential enclosure domain') + total = term = Q(1) + count = 48 + for j in range(1, count+1): + term = term*x/j + total += term + following = term*x/(count+1) + return total, total+following/(1-x/(count+2)) + + +@lru_cache(None) +def rank_power(n, saving): + a, b = log_bounds(n) + return Q(n)/exp_bounds(saving*b)[1], Q(n)/exp_bounds(saving*a)[0] + + +def display(pair): + scale = 10**30 + low, high = pair + a = low.numerator*scale//low.denominator + b = -((-high.numerator*scale)//high.denominator) + + def fixed(v): + sign = '-' if v < 0 else '' + s = str(abs(v)).rjust(31, '0') + return sign+s[:-30]+'.'+s[-30:] + + return {'lower': fixed(a), 'upper': fixed(b)} + + +def moment_margin(targets, paid, saving): + signed = Counter(targets) + signed.subtract(paid) + low = high = Q(0) + for n, count in signed.items(): + a, b = rank_power(n, saving) + low += count*(a if count >= 0 else b) + high += count*(b if count >= 0 else a) + return low, high + + +def eta_power(m, saving, q): + # eta=(1-saving)*m^(-saving). + a, b = log_bounds(m) + return ((1-saving)**q/exp_bounds(q*saving*b)[1], + (1-saving)**q/exp_bounds(q*saving*a)[0]) + + +def final_test(H, gap, q): + """(H+1) < 2^(q*gap*H), by exact integer powers.""" + power = q*gap*H + return (H+1)**power.denominator < 2**power.numerator + + +def grid_rank(gap, q, step=1000): + # g(H)=q*gap*H*ln(2)-ln(H+1) has g(0)=0, g'(0)<0, g''>0. + # It has one positive crossing, so binary search cannot skip a win. + need(0 < q*gap < 1, 'one positive crossing') + low, high = 0, 1 + while not final_test(step*high, gap, q): + low, high = high, high*2 + while high-low > 1: + mid = (low+high)//2 + if final_test(step*mid, gap, q): + high = mid + else: + low = mid + return step*high + + +def profile(raw): + result = {int(k): v for k, v in raw.items()} + need(result and all(k >= 1 and isinstance(v, int) and v > 0 + for k, v in result.items()), 'positive integer histogram') + return result + + +def check_case(name, targets, paid, saving, uniform_saving, theta, q, previous, step=1000): + targets, paid = profile(targets), profile(paid) + m, kmin, rmax = max(targets), min(targets), max(paid) + need(1 <= rmax < kmin <= m, 'strict mixed separation') + need(0 < uniform_saving < saving < 1 and 0 < theta < 1, 'strict exponents') + need(isinstance(q, int) and q >= 1, 'positive integer q') + margin = moment_margin(targets, paid, saving) + need(margin[0] > 0, 'unit t-superpotential') + a, b = theta.numerator, theta.denominator + need(rmax**b < kmin**a, 'exit power bound') + shift_left, shift_right = 2**(b-a)*rmax**b, m**a + need(shift_left <= shift_right, 'shifted logarithm contraction') + eta = eta_power(m, saving, q) + need(eta[0] > theta, 'eta^q > theta') + base_upper = exp_bounds(q*saving*log_bounds(m)[1])[1] + need(base_upper < 2, 'ordinary base ranks fit the majorant') + gap = saving-uniform_saving + H = grid_rank(gap, q, step) + need(H >= m.bit_length(), 'winning rank exceeds the base') + need(final_test(H, gap, q), 'strict final uniform moment') + need(not final_test(H-step, gap, q), 'previous grid rank fails') + need(eta_power(m, saving, q+1)[1] < theta, 'q+1 fails this contraction') + need(previous['targets'] == {str(k): v for k, v in targets.items()} + and previous['paid'] == {str(k): v for k, v in paid.items()} + and Q(previous['tested_mixed_saving']) == saving + and Q(previous['theta_upper']) == theta, 'unchanged predecessor invoice') + power = q*gap*H + old_H = previous['N']['H1'] + return { + 'family': name, 'targets': targets, 'paid': paid, + 'tested_mixed_saving': str(saving), 'uniform_saving': str(uniform_saving), + 't': str(1-saving), 'z': str(1-uniform_saving), + 'theta_upper': str(theta), 'logarithm_power': str(Q(1, q)), + 'strict_unit_moment_margin': display(margin), + 'eta_to_q': display(eta), + 'eta_to_q_minus_theta': display((eta[0]-theta, eta[1]-theta)), + 'shift_integer_test': {'left': shift_left, 'right': shift_right}, + 'base_m_to_q_saving_upper': display((Q(1), base_upper))['upper'], + 'majorant': 'L(n) <= n^t * (1+log2(n))^(1/q), n>=1; L(0)=0', + 'N': {'encoding': '2^H', 'H': H}, + 'final_integer_test': { + 'left_base': H+1, 'left_exponent': power.denominator, + 'right_base': 2, 'right_exponent': power.numerator, 'relation': '<'}, + 'previous_H': old_H, 'exponent_reduction_factor': str(Q(old_H, H)), + 'grid_step': step, + 'previous_uniform_saving': previous['uniform_saving'], + 'controls': {'previous_grid_point_fails_final_majorant': True, + 'q_plus_one_fails_contraction': True}, + 'materialized_word': False, + } + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def authenticate_sources(): + inputs = {} + for row in read(HERE/'VENDOR.json')['files']: + need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], + 'changed predecessor input: '+row['path']) + inputs[row['path']] = row['sha256'] + return inputs + + +def retuned_outer(complex_case, bit_case): + """Reprice the complete nine-row ledger and all inherited predicates. + + The AST oracle executes only the pinned ledger function and its historic + comparison constants. Its old m=73 native admission code is never run. + """ + old = read(HERE/'vendor/OUTER-PARAMETERS.json') + p = {k: Q(v['rational']) if isinstance(v, dict) and 'rational' in v else v + for k, v in old['outer']['parameters'].items()} + conversion = read(HERE/'vendor/BIT-ALLSIZE-PARAMETERS.json') + atom, old_leaf = Q(conversion['atom_power']), Q(conversion['old_ordinary_saving']) + bare = Q(bit_case['uniform_saving']) + cover_gap = Q(conversion['C0_minus_C1']) + covered = bare-cover_gap + ordinary = (1-atom)*covered+atom*old_leaf + p.update(b=Q('0.0023004'), q=Q('0.0023002'), + effective_saving=Q('0.0023003'), BIT_saving=Q('0.002301'), + complex_uniform_saving=Q(complex_case['uniform_saving'])) + eps, beta, outer_q, effective = (p[k] for k in + ('epsilon', 'group_beta', 'q', 'effective_saving')) + p['lambda'] = 1-(outer_q+effective)/2 + p['lambda_prime'] = 1-outer_q + c = (3-p['Strassen_exponent'])/2 + p['cap_xi'] = eps*(1+outer_q)-c+p['layout_slack'] + xi, target, stop = p['cap_xi'], p['kappa'], p['stop'] + own = { + 'main_transform': eps*outer_q, + 'global_coordinate_router': effective, + 'fused_gaussian': 1-eps+outer_q*beta, + 'group_bit_router': 1-eps+effective*beta, + 'group_scans': 1-eps+beta, + 'boundary_algebraic_matrix': c+xi-eps, + 'sparse_union_movement': xi+Q(1, 2)-eps, + 'polynomial_products': eps, + 'microbox_face_corrections': 1-(eps+beta+p['halo_power']-p['core_power']+2), + } + need(all(v > target for v in own.values()), 'retuned nine outer cost rows') + sigma, tau = 1-p['b'], 1-effective + internal = tau+(1-stop)*max(sigma-tau, Q(0)) + leaf = sigma+stop*(1-sigma) + checks = { + 'uniform_complex_above_b': p['complex_uniform_saving']-p['b'], + 'ordinary_BIT_above_admitted': ordinary-p['BIT_saving'], + 'admitted_BIT_above_effective': p['BIT_saving']-effective, + 'selected_complex_above_effective': p['b']-effective, + 'lambda_above_internal': p['lambda']-internal, + 'lambda_above_sigma': p['lambda']-sigma, + 'lambda_prime_above_lambda': p['lambda_prime']-p['lambda'], + 'lambda_prime_above_leaf': p['lambda_prime']-leaf, + 'semantic_main_guard': 1-eps, + 'semantic_group_guard': 1-beta, + 'BIT_row_stock_sublinear': beta*(1-atom), + 'group_below_dimension': eps-beta, + 'global_gamma_spare': 1-eps-p['r0'], + 'fine_prime_group_guard': 1-(2*xi-2)-p['r0']-beta, + 'descriptor_complete_fiber': 1-eps, + 'explicit_metadata_halo': p['core_power']-p['halo_power']-eps-beta-1, + 'membership_record_budget': 1-beta-2*(1-eps), + 'short_record_fallback': eps-effective, + 'BIT_linear_adapter': atom-ordinary, + 'BIT_borrowed_stock': 1-ordinary-atom, + 'BIT_cover_gap': cover_gap, + 'fine_prime_umbrella': 10-(2*p['theta_power']+2+Q(1, 2)), + } + need(all(v > 0 for v in checks.values()), 'retuned functional interfaces') + need(cover_gap == Q(1, 100000), 'unchanged delayed-cover prime bound') + fallback = (1+cover_gap/4)/(1+cover_gap/2) + need(fallback == Q(conversion['prime_rule']['complete_moment_upper']), + 'same fully charged cover/fallback moment') + source = ast.parse((HERE/'vendor/check_ledger.py').read_text()) + function = next(node for node in source.body + if isinstance(node, ast.FunctionDef) and node.name == 'ledger') + constants = [node for node in source.body if isinstance(node, ast.Assign) + and any(isinstance(t, ast.Name) and t.id.startswith('KAPPA_') + for t in node.targets)] + baseline = Q('0.001730970419199163702738') + env = {'Q': Q, 'R0': p['r0'], 'ZETA': Q(1, 10**8), 'SLACK': p['layout_slack'], + 'STOP': stop, 'FLOOR': 10**7, 'BACKOFF': Q(1, 10**7), + 'EPS': eps, 'BETA': beta, 'THETA_POWER': Q(p['theta_power']), + 'HALO_POWER': p['halo_power'], 'CORE_POWER': p['core_power'], + 'STRASSEN_TAU': p['Strassen_exponent'], + 'b': p['b'], 'q': outer_q, 'a': effective, 'bit': p['BIT_saving'], + 'online': baseline, 'old': baseline} + module = ast.fix_missing_locations(ast.Module(body=constants+[function], type_ignores=[])) + exec(compile(module, 'pinned check_ledger.py:ledger', 'exec'), env) + oracle = env['ledger']('retuned_kappa_0023_smaller_ranks') + need(oracle['kappa'] == target == Q('0.0023'), 'same declared kappa after grid/backoff') + need(oracle['margins'] == own, 'all nine rows match the inherited oracle') + need(len(oracle['strict_checks']) == 63 and + all(v > 0 for v in oracle['strict_checks'].values()), 'all 63 inherited predicates') + controls = {} + for name, options in ( + ('epsilon_one', {'eps_': Q(1)}), + ('zero_layout_slack', {'slack': Q(0)}), + ('group_equals_dimension', {'beta_': eps}), + ('unfunded_old_per_axis_scan', {'old_scan': True}), + ): + invalid = env['ledger']('reject_'+name, **options) + failed = sorted(k for k, v in invalid['strict_checks'].items() if v <= 0) + need(failed, 'outer control accepted: '+name) + controls[name] = failed + return { + 'parameters': {k: str(v) for k, v in p.items()}, + 'nine_cost_savings': {k: str(v) for k, v in own.items()}, + 'minimum_saving_minus_kappa': str(min(own.values())-target), + 'functional_gaps': {k: str(v) for k, v in checks.items()}, + 'inherited_predicates': {k: str(v) for k, v in oracle['strict_checks'].items()}, + 'grid_floor': 10**7, 'grid_backoff': '1/10000000', + 'BIT_before_cover': str(bare), 'BIT_after_cover': str(covered), + 'BIT_ordinary_saving': str(ordinary), + 'BIT_atom_power': str(atom), 'BIT_old_leaf_saving': str(old_leaf), + 'BIT_prime_coefficient': str(256/cover_gap), + 'BIT_fallback_moment_upper': str(fallback), 'rejected_controls': controls, + 'scope': 'Exact parameter compatibility under the pinned native/cover/support/outer hypotheses; not a fresh native admission or full replay.', + } + + +def verify(): + sources = authenticate_sources() + old = read(HERE/'vendor/EXPLICIT-TEMPLATE-BOUNDS.json')['cases'] + cover = read(HERE/'vendor/P3-NATIVE-COVER.json.gz')['cover'] + bit = next(row for row in read(HERE/'vendor/MIXED-PRODUCTIVE-BIT.json')['candidates'] + if row['pairs'] == 3 and row['keep_idle_mask'] == 43) + args = [ + ('complex/same-savings', cover['targets'], cover['paid'], Q('0.002305'), Q('0.002304'), Q(9, 10), 9, old[0]), + ('BIT/same-savings', bit['targets'], bit['paid'], Q('0.002769'), Q('0.002760'), Q(15, 16), 4, old[1]), + ('complex/kappa-0023', cover['targets'], cover['paid'], Q('0.002305'), Q('0.0023005'), Q(9, 10), 9, old[0]), + ('BIT/kappa-0023', bit['targets'], bit['paid'], Q('0.002769'), Q('0.002318'), Q(15, 16), 4, old[1], 100), + ] + cases = [check_case(*arg) for arg in args] + rejected = [] + for arg in args: + bad_paid = dict(arg[2]) + bad_paid['1'] = 10**9 + mutations = ( + ('lost_unit_superpotential', (*arg[:2], bad_paid, *arg[3:]), 'unit t-superpotential'), + ('lost_strict_separation', (arg[0], {'1': 1}, *arg[2:]), 'strict mixed separation'), + ('q_plus_one', (*arg[:6], arg[6]+1, *arg[7:]), 'eta^q > theta'), + ) + for label, mutated, expected in mutations: + try: + check_case(*mutated) + except ValueError as error: + need(str(error) == expected, 'wrong rejection point: '+label) + rejected.append({'family': arg[0], 'mutation': label, 'rejected_at': str(error)}) + else: + raise ValueError('negative control accepted: '+label) + return { + 'schema': 'logarithmic-uniform-template-ranks/1', + 'status': 'PASS_LOGARITHMIC_MAJORANT_RANKS', 'cases': cases, + 'kappa_0023_retuned_outer': retuned_outer(cases[2], cases[3]), + 'rejected_mutations': rejected, 'input_sha256': sources, + 'verifier_sha256': sha256(Path(__file__).read_bytes()).hexdigest(), + 'proof_dependency': 'README.md and PR4359 finite source/exit compiler with its native closure hypotheses', + 'scope': 'Smaller sufficient ambient ranks; no emitted supplier, complete constant bounds, native admission, or new kappa.', + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path, help='write a new receipt instead of comparing RESULT.json') + args = parser.parse_args() + result = verify() + encoded = json.dumps(result, indent=2, sort_keys=True)+'\n' + if args.out: + need(not args.out.exists(), 'output must be a new file') + args.out.write_text(encoded) + else: + need(read(HERE/'RESULT.json') == json.loads(encoded), 'committed receipt differs') + print(json.dumps({'status': result['status'], 'ranks': [ + {'family': row['family'], 'N': row['N']} for row in result['cases']], + 'rejected_mutations': len(result['rejected_mutations'])})) + + +if __name__ == '__main__': + main()