diff --git a/research/selected-complex-width-envelope/README.md b/research/selected-complex-width-envelope/README.md new file mode 100644 index 0000000000..b59d4127cc --- /dev/null +++ b/research/selected-complex-width-envelope/README.md @@ -0,0 +1,252 @@ +# A two-sided complex row-depth coefficient for the #4470 nested compiler + +**Scoped written bound with author-checked exact arithmetic; no new κ.** +The selected conditional exponent remains `60403/20000000`. This answers the +open coefficient-bracket question of James Reed's [PR4972](https://github.com/CrocSwap/integer-mult-bounds/pull/4972). +It does not compute an astronomical word or change the compiler. + +Put `H = 64215200000000`, `N = 2^H`, and + +``` +K = ceil(log2 B_N) / H. +``` + +For the actual #4470 product/completion/splitting rule and **#4436's nested +divisible-width realization**, the written argument below proves + +``` +(2943/1000) N < K < (3639/1000) N. +``` + +The endpoint ratio is below `5/4`. The older lower bound used only +`S_n >= 2`, while the upper bound counted paid rank mass as paid calls and +used `G(N) <= H`. Counting actual root sources, charging every split and +completion, and using the productive floor give the sharper bounds. +These are bounds on the same permitted realization, not a search for +smaller batching widths. #4470 does not specify a unique minimal `B_N`. + +In the **same conservative outer-accounting formula** as #4972, retaining +its `c_row = 1`, support-width tariff `Cw = 232960`, BIT share, nesting and +sum allowances, `K < 4N` gives: + +| Quantity | PR4972 | This bound | +| --- | ---: | ---: | +| Complex-share `log2` upper bound | 64,215,200,000,022 | 64,215,200,000,008 | +| `log2 C` upper bound | 64,215,200,000,024 | 64,215,200,000,010 | +| Displayed sufficient-fit `log2 p` | 64,473,100,659,050 | 64,473,100,659,036 | + +The factor-`5/4` bracket is for **K**, not for an optimal `C`. The outer +figures retain the predecessor's deliberately loose tariffs and do not +admit them independently. The numerical threshold comparison is a +consequence of the new source-count bound, not a second cutoff search. + +## Source-bound rule and realization + +At base `bee95ce88f9f19802f0613f92838895cd0e14a1f`, +`joint-helper-lattice/RESULT.json` and `PROOF.md` §§4–6 give: + +``` +raw productive count W0 = 10928; raw paid count Q0 = 64620; +raw paid rank mass R0 = 239134; raw ambient rank m0 = 145; +v = 1024; productive floor b = 21; paid cutoff c = 20. +``` + +The product has `W = W0^v` productive fields. Complete each target of rank +below `L = b^v` to rank L on disjoint coordinates of that same field, then +split every paid job at `J = c^v`. Its ambient rank is `M = m0^v` and its +minimum productive rank is L. Completion and splitting retain all paid +charges and do not add productive fields. Native correctness, whole-job +adapters and physical tariffs remain the source hypotheses. + +Exactly 7792 raw productive fields have rank at most 21. The ordered +product choices using only those fields give at least + +``` +A = 7792^1024 +``` + +distinct final targets of rank **exactly L**: their original product rank +is at most L, and paid completion raises it to L when necessary. This is +a lower bound on one target multiplicity, not credit for all W targets. + +Use the default-height flow of `direct-mixed-flow/README.md` §§2–3: + +``` +G(n) = max {g >= 0 : M L^g <= n}, n >= M; +B_n = 1 below M; +a_n = B_(n-1), B_n = a_n S_n; +B_N = product_(n=M..N) S_n. +``` + +`S_n` counts all distinct top sources at rank n. The nested widths make +every complement/exit batch integral. #4507's least chronological widths +and #4483's changed-height compiler are different choices and are not used. + +## Proof of the two bounds + +**1. Fully charged paid-count upper bound.** Let Q be the final number of +paid calls. For any positive rank R, splitting at J produces +`ceil(R/J) <= 1 + R/J` calls. Original product calls have count `Q0^v` and +total rank mass `R0^v`. Every completion has rank below L, and there are +at most W completions. Hence the integer bound + +``` +Q <= Qbar = Q0^v + ceil(R0^v/J) + W ceil(L/J) +``` + +charges original calls, every original rounding surcharge and every +completion. A completion of rank zero contributes no actual call; the +bound may still overcount it. Write `C0 = W + Qbar + 1`. + +**2. A root-source injection.** In the source flow, the root multi-index +having G copies of the minimum target type is eligible because +`M L^G <= n`. It has at least `A^G` unit instances. Each has W distinct +productive target slots; all these root slots are top sources, at rank +at most n. Therefore + +``` +S_n >= W A^G(n). +``` + +These slots are distinct source arrays in the integer flow, not copied +values or extra productive credit. The source's full-layer count also gives + +``` +S_n <= W (W+Q+1)^(G(n)+1) <= W C0^(G(n)+1). +``` + +**3. Height bounds without logarithmic approximations.** For a positive +integer x, `bit_length(x)-1 <= log2(x) < bit_length(x)`. Thus + +``` +hlo = floor((H - bit_length(M)) / bit_length(L)) + = 14276389504; +hhi = floor((H - (bit_length(M)-1)) / (bit_length(L)-1)) + = 14279564152; +hlo <= G(N) <= hhi. +``` + +The lower estimate certifies `M L^hlo <= N`. For every integer +`n >= M L^(hlo-1)`, `G(n) >= hlo-1`. This interval contains at least +`N(1-1/L)` indices because `M L^(hlo-1) <= N/L`. Since `hlo >= 1`, +the interval lies in the nonbase range. All other factors `S_n` are positive +integers, so their logarithms cannot decrease the lower bound. + +Define the following small, exactly computable integers: + +``` +Xlo = (bit_length(W)-1) + (hlo-1)(bit_length(A)-1) + = 188990844254451; +Xhi = bit_length(W) + (hhi+1)bit_length(C0) + = 233670787813430. +``` + +Summing the source logarithms proves + +``` +N(1-1/L) Xlo <= log2 B_N <= N Xhi. +``` + +The upper endpoint `N Xhi` is an integer, so it also bounds +`ceil(log2 B_N)`. Exact integer comparisons now give + +``` +1000 (L-1) Xlo > 2943 L H; +1000 Xhi < 3639 H; +4 Xhi L < 5 (L-1) Xlo. +``` + +Divide by NH to obtain the stated coefficient bracket and its ratio. +No integer of size N, no full target inventory and no uniform word is +constructed in these checks. All integer powers computed here have only +tens of thousands of bits. + +**4. Conditional outer substitution.** `batched-complex-rows.tex` and +#4972 identify the row-depth coefficient as K under their stated contract. +The previous formula multiplies K by an upward width factor `2^5` and +a nesting factor 2. Since `Xhi < 4H`, `K < 4N`, so its complex share is +below `2^(H+8)`. The unchanged BIT bound is `2^51973930319885`; the +unchanged old-stock allowance is `2^74`. The predecessor's factor-four +sum allowance gives `log2 C <= H+10`. + +For its displayed sufficient condition +`(log2 C+10+3 ulog2(Lp))/(1-1/250) <= (69999991/70000000) Lp`, +the verifier partitions positive integers Lp by bit length and solves +each resulting rational linear inequality. This gives the least integer +for that particular upward-rounded formula without assuming its stepwise +predicate is monotone. It is not an exact physical input threshold. + +## Reproduction and verification scope + +From the repository root, Python 3.12, standard library only: + +```sh +python3.12 -I -W error -B research/selected-complex-width-envelope/verify.py +python3.12 -I -O -W error -B research/selected-complex-width-envelope/verify.py +python3.12 -B scripts/research_package.py --package research/selected-complex-width-envelope +``` + +The read-only verifier authenticates every live input by SHA-256 and Git +blob identity before and after replay. It loads only the authenticated +#4436 flow bytes, compares merged and literal chronological flows on small +instances, checks source/nested-width bounds and twelve exact product/ +completion/splitting cases, and requires five mathematical rejection +controls. `RESULT.json` binds the deterministic arithmetic and finite scope. +Direct commands support a Git-free export; metadata/provenance checks +separately require Git. `--emit` prints the receipt to stdout. + +Author validation used Linux x86_64 and Python 3.12.15. Both registered +normal/optimized modes pass: 366 small source flows, 12 literal comparisons, +332 nested lower checks, 16 height checks, 12 product/pad/split cases and +six reduced-power (`v=1`) calibrations of the actual #4470 raw invoice at +rank/height boundaries. Five mathematical controls reject. Allow a minute +for the bounded replay. Committed-byte and Git-free export checks are +separate publication evidence; the optional full-history ancestry preflight +is not claimed in this shallow checkout. + +Finite checks corroborate the written inequalities; they are not a proof +by enumeration of every rank or native operator. All evidence from this +session is **author-checked**, including the separately implemented +arithmetic. No independent reviewer or proof kernel is claimed. + +Not checked: exact `B_N`, least/alternative batching widths, a physical +compiled word, all-column/native correctness, owned-bank and route bodies, +precision or fixed tapes, BIT/outer supplier admission, analytic/prime/ +recovery hypotheses, or the full selected cold replay. The `c_row`, `Cw` +and unchanged BIT/old-stock tariffs are explicit inherited premises in the +outer substitution. No selected record, predecessor or frozen source is edited. + +## Open next questions + +1. **Sharpen the root/source census rather than change batching.** The + coefficient bracket is below 5/4 but not exact. Derive a uniform bound + on all eligible root multi-indices and nonroot source classes for this + same fixed rule. First compare those counts on the literal small flows; + stop if the additional estimate only renames the existing bounds. + The missing ingredient is a quantified truncated-source estimate, not + another numerical outer-root calculation. +2. **Bind the inherited physical stock interface.** This count result + supplies B_N for one permitted finite realization. A full implementation + still needs the actual fixed-program stock, routing, owned-storage and + precision/tape contracts. Begin with one named source-bound invocation + and its complete ownership ledger; the enormous uniform word is not + materialized here. + +## Attribution and task + +Card `selected-stock-envelope`, adversarial-audit, priority revision 7, +refined to PR4972's open next question. Seed +`12681598eca9c3a85296c48193125739`; exact sources and card are in +`SOURCES.json` and `TASK.json`. + +Credit James Reed / jwr404 (#4972 coefficient and handoff, #4970 old leaf); +Mark / Matarener (#4612 and `lockstep-live-role-audit`); zxv (#4436 nested +widths, higher-moment strictification and retained native/stock sources); +Cinna Davis / 1337isnot1337 and zxv (#4440/#4470); Jacob Alan Sussman +(Theorem 1G multinomial lockstep flow); Ryanson Jonathan (#4476 separate +width checks); and mihir-s-05 / #4507 and its #4519 recount for the distinct +chronological batching boundary. All retained source notices remain intact. + +Prepared by Sagar Thakrar with substantial OpenAI Codex assistance, solo. +New material is Apache-2.0. The claim and subsequent handoff are linked in +the contribution PR; no scientific acceptance is inferred from publication. diff --git a/research/selected-complex-width-envelope/RESULT.json b/research/selected-complex-width-envelope/RESULT.json new file mode 100644 index 0000000000..1e70560467 --- /dev/null +++ b/research/selected-complex-width-envelope/RESULT.json @@ -0,0 +1,97 @@ +{ + "conditional_outer_accounting": { + "assumed_c_row": 1, + "inherited_Cw": 232960, + "inherited_log2_A_old_upper": 64, + "new_complex_share_log2_upper": 64215200000008, + "new_fit_log2_p": 64473100659036, + "new_log2_C_upper": 64215200000010, + "previous_complex_share_log2_upper": 64215200000022, + "previous_fit_log2_p": 64473100659050, + "previous_log2_C_upper": 64215200000024, + "scope": "Same conservative outer-accounting formula and inherited tariffs; not optimal C or supplier admission.", + "unchanged_BIT_share_log2_upper": 51973930319885 + }, + "envelope": { + "A_log2_lower": 13238, + "H": 64215200000000, + "K_over_N_strict_bounds": [ + "2943/1000", + "3639/1000" + ], + "N": "2^64215200000000", + "W_log2_upper": 13738, + "W_plus_paid_bound_plus_one_log2_upper": 16364, + "ambient_base": 145, + "ambient_log2_bounds": [ + 7352, + 7353 + ], + "bracket_ratio_strict_upper": "5/4", + "cutoff_base": 20, + "floor_base": 21, + "floor_log2_bounds": [ + 4497, + 4498 + ], + "height_lower": 14276389504, + "height_upper": 14279564152, + "raw_paid_count": 64620, + "raw_paid_mass": 239134, + "raw_productive_count": 10928, + "raw_targets_at_most_floor": 7792, + "tensor_power": 1024, + "x_lower": 188990844254451, + "x_upper": 233670787813430 + }, + "evidence_level": "author-checked", + "finite_checks": { + "height_bound_checks": 16, + "literal_flows": 12, + "negative_controls": [ + "omitted-completion", + "omitted-split-rounding", + "all-targets-counted-at-floor", + "inflated-root-lower-bound", + "height-rounding-direction" + ], + "nested_width_lower_checks": 332, + "product_pad_split_cases": 12, + "selected_v1_source_calibration": [ + [ + 145, + 0, + 10928 + ], + [ + 3044, + 0, + 10928 + ], + [ + 3045, + 1, + 328391680 + ], + [ + 63944, + 1, + 119421184 + ], + [ + 63945, + 2, + 7885246941440 + ], + [ + 63946, + 2, + 7885246941440 + ] + ], + "source_flows": 366, + "source_rows_sha256": "1a394cbb8e6c6e2c56fccae0c9884072d171dca4ae9dea024c6d8e8360fc6f43" + }, + "schema_version": 1, + "selected_kappa_unchanged": "60403/20000000" +} diff --git a/research/selected-complex-width-envelope/SOURCES.json b/research/selected-complex-width-envelope/SOURCES.json new file mode 100644 index 0000000000..73e62eff0b --- /dev/null +++ b/research/selected-complex-width-envelope/SOURCES.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/direct-mixed-flow/README.md", + "usage": "input", + "git_blob": "3be00f754b9ffa23e64b3eafe7706e3ac139993a", + "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8" + }, + { + "path": "research/direct-mixed-flow/flow.py", + "usage": "input", + "git_blob": "07175cd6e1f2c2367c2e78eca7f163fef18d301d", + "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a" + }, + { + "path": "research/higher-moment-strictification/README.md", + "usage": "input", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d" + }, + { + "path": "research/joint-helper-lattice/PROOF.md", + "usage": "input", + "git_blob": "e41106031da41fade7a7419c17a32c1bd9aa103b", + "sha256": "43ef4251cc300f1b18cbe8cdb060f96f95748e6797d2478b4c04b79a8373ef91" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "research/lockstep-live-role-audit/constant_c.py", + "usage": "input", + "git_blob": "a0fc4aecb910a353dd049926e25e13c20324112c", + "sha256": "74939dfa06092a6ea2cc7c94ce376f89d08c60c66af46ce5923341ed356ab51f" + }, + { + "path": "research/lockstep-live-role-audit/README.md", + "usage": "input", + "git_blob": "158858c0a330465589c6b584926ec8b050191490", + "sha256": "0f3de4ae60ec52ad8096f5979db88e9949d8a54b50364b902ffb66a9b39eb075" + }, + { + "path": "research/selected-complex-row-coefficient/README.md", + "usage": "input", + "git_blob": "621abc3cee53c441b4d841f696c70acdb1140ab5", + "sha256": "c5935be7ced8c36aae80d40dea36335f468a447d59fd0a58f8329c3cf24ab7a0" + }, + { + "path": "notes/batched-complex-rows.tex", + "usage": "input", + "git_blob": "e13bd96eb29bdc6526f10dc32e0a146bc17848a4", + "sha256": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c" + }, + { + "path": "research/kappa-rebuild/transfer-audit/AUDIT.md", + "usage": "input", + "git_blob": "ee8c49a3450f812011eb3f7f40c25f5ade26b2d0", + "sha256": "032488343667d19613cab84df5dad554cfd2a283fb4fc0d4c9b4d165cfa04669" + }, + { + "path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "usage": "input", + "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535", + "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779" + } + ] +} diff --git a/research/selected-complex-width-envelope/TASK.json b/research/selected-complex-width-envelope/TASK.json new file mode 100644 index 0000000000..80a4f99b64 --- /dev/null +++ b/research/selected-complex-width-envelope/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md", + "research/stock-margin-chain/README.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption.", + "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990", + "2972", + "stock-margin-chain", + "actual_stock_coefficient" + ], + "existing_checks": [ + { + "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.", + "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation", + "remaining": "Derive one actual reserve/depth coefficient from the selected producer.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Bound the actual PR4470 complex row-depth coefficient K=ceil(log2 B_N)/log2 N for PR4436 nested divisible widths, following PR4972 open next question 1; propagate only into the same explicitly conditional outer accounting.", + "scope_change_reason": "The card's old bootstrap starting points predate the selected PR4470. The live PR4972 handoff asks for a source-bound coefficient bracket. This package counts actual root sources and paid split/completion calls for that selected unit; it does not repeat cutoff arithmetic or change the compiler.", + "bottleneck_link": "Supplies a quantified two-sided productive-width coefficient for one permitted realization, replacing the coarse source-count and height bounds while leaving physical/compiler admission premises explicit.", + "budget_minutes": 480, + "seed": "12681598eca9c3a85296c48193125739", + "stop_rule": "Stop at one written width-envelope lemma and exact bounded checks. No enormous word, alternative batching search, frontier change, or full multiplier replay.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/selected-complex-width-envelope", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial OpenAI Codex assistance; solo, no subagents or independent human review.", + "open_questions": [ + { + "question": "Can a quantified truncated-source count sharpen the same nested-width coefficient beyond the factor-5/4 bracket?", + "why_it_matters": "The current root injection and full-layer upper count are deliberately different relaxations of one fixed source census.", + "first_step": "Compare all eligible root multi-indices and nonroot source classes on the registered literal small flows, then prove one uniform count estimate.", + "blocked_by": "A source-bound truncated-source estimate; not another outer root or a larger unmotivated scan." + }, + { + "question": "Can one actual fixed-program invocation realize its productive-width, route, owned-storage and precision/tape ledger?", + "why_it_matters": "A symbolic productive count does not supply physical compiler/stock admission.", + "first_step": "Name one invocation and its complete ownership and inherited primitive contracts before implementing its stock/route generator.", + "blocked_by": "Unmaterialized fixed program and inherited physical, primitive, precision and tape contracts." + } + ] +} diff --git a/research/selected-complex-width-envelope/VERIFY.json b/research/selected-complex-width-envelope/VERIFY.json new file mode 100644 index 0000000000..d9127683d0 --- /dev/null +++ b/research/selected-complex-width-envelope/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/direct-mixed-flow/README.md", + "research/direct-mixed-flow/flow.py", + "research/higher-moment-strictification/README.md", + "research/joint-helper-lattice/PROOF.md", + "research/joint-helper-lattice/RESULT.json", + "research/query-thinned-controllers/RESULT.json", + "research/lockstep-live-role-audit/constant_c.py", + "research/lockstep-live-role-audit/README.md", + "research/selected-complex-row-coefficient/README.md", + "notes/batched-complex-rows.tex", + "research/kappa-rebuild/transfer-audit/AUDIT.md", + "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Authenticated source-count proof arithmetic, literal/merged small flows, exact product/completion/split accounting, five mathematical failure controls, and same-model conditional outer comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Same complete bounded checks with Python assertions disabled; all guards are explicit." + } + ] +} diff --git a/research/selected-complex-width-envelope/verify.py b/research/selected-complex-width-envelope/verify.py new file mode 100644 index 0000000000..1646809e8a --- /dev/null +++ b/research/selected-complex-width-envelope/verify.py @@ -0,0 +1,291 @@ +#!/usr/bin/env python3 +"""Exact bounds for one nested-width realization; no native or outer admission. + +Sagar Thakrar, with substantial OpenAI Codex assistance. Apache-2.0. +The finite-flow oracle is zxv's unchanged PR4436 implementation of the +Jacob Alan Sussman construction; it is authenticated before execution. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha1, sha256 +import json +from pathlib import Path +import sys +from types import ModuleType + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticated_inputs(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + result = {} + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = ROOT / row["path"] + need(all(not p.is_symlink() for p in (path, *path.parents) if p != ROOT.parent), + "symlinked input: " + row["path"]) + raw = path.read_bytes() + need(sha256(raw).hexdigest() == row["sha256"], "changed input: " + row["path"]) + blob = b"blob " + str(len(raw)).encode("ascii") + b"\0" + raw + need(sha1(blob).hexdigest() == row["git_blob"], "changed Git blob: " + row["path"]) + result[row["path"]] = raw + return result + + +def ceildiv(n, d): + return (n + d - 1) // d + + +def legacy_ulog2(x): + """The predecessor's deliberately upward bit-length bound, including at powers of two.""" + x = Q(x) + return x.numerator.bit_length() - (x.denominator.bit_length() - 1) + + +def product_inventory(inv, power): + out = Counter({1: 1}) + for _ in range(power): + following = Counter() + for x, nx in out.items(): + for y, ny in inv.items(): + following[x * y] += nx * ny + out = following + return out + + +def literal_completion(targets, paid, power, floor, cutoff): + """Small exact product/pad/split oracle, not an emitted native word.""" + t = product_inventory(targets, power) + p = product_inventory(paid, power) + L, J = floor ** power, cutoff ** power + completed = Counter() + for rank, count in t.items(): + completed[max(L, rank)] += count + if rank < L: + p[L - rank] += count + split = Counter() + for rank, count in p.items(): + q, r = divmod(rank, J) + split[J] += q * count + if r: + split[r] += count + return +completed, +split + + +def paid_count_bound(targets, paid, power, floor, cutoff): + W = sum(targets.values()) ** power + original = sum(paid.values()) ** power + mass = sum(k * n for k, n in paid.items()) ** power + L, J = floor ** power, cutoff ** power + return original + ceildiv(mass, J) + W * ceildiv(L, J) + + +def floor_multiplicity_lower(targets, power, floor): + return sum(count for rank, count in targets.items() if rank <= floor) ** power + + +def height_bounds(H, M, L): + lower = (H - M.bit_length()) // L.bit_length() + upper = (H - (M.bit_length() - 1)) // (L.bit_length() - 1) + return lower, upper + + +def rejects(check, name): + try: + check() + except ValueError: + return name + raise ValueError("negative control accepted: " + name) + + +def finite_checks(Flow, selected): + profiles = [({2: 2, 5: 1}, {1: 2}), + ({2: 1, 5: 1}, {1: 2, 4: 1}), + ({3: 2}, {1: 3, 2: 1}), + ({3: 1, 9: 1}, {1: 1})] + rows, literal_cases, nested_cases, height_cases = [], 0, 0, 0 + for targets, paid in profiles: + m, L = max(targets), min(targets) + W, A, C = sum(targets.values()), targets[L], sum(targets.values()) + sum(paid.values()) + 1 + B = 1 + for n in range(m, 97): + flow = Flow(targets, paid, n) + got = flow.merged() + h, S = got["height"], got["source_count"] + if n & (n - 1) == 0: + lo, hi = height_bounds(n.bit_length() - 1, m, L) + need(lo <= h <= hi, "height bounds against exact source flow") + height_cases += 1 + need(W * A ** h <= S <= W * C ** (h + 1), "finite source-count envelope") + B *= S + need(B <= (W * C ** (h + 1)) ** n, "finite nested-width upper bound") + if h >= 1: + need(B >= (W * A ** (h - 1)) ** (n - n // L), "finite nested-width lower bound") + nested_cases += 1 + if n in {m, m * L, m * L * L}: + word = [r for r, count in paid.items() for _ in range(count)] + literal = flow.literal(word) + need(literal["sources"] == got["sources"] and literal["exits"] == got["exits"], + "literal/merged chronological flow disagreement") + literal_cases += 1 + rows.append([sorted(targets.items()), sorted(paid.items()), n, h, S]) + products = 0 + for targets, paid, b, c in [({2: 2, 5: 1}, {1: 2, 3: 1}, 3, 2), + ({2: 1, 9: 1}, {1: 3}, 3, 2), + ({2: 10, 5: 1}, {1: 1}, 4, 2)]: + for v in range(1, 5): + t, p = literal_completion(targets, paid, v, b, c) + A = floor_multiplicity_lower(targets, v, b) + need(t[b ** v] >= A, "completed minimum-target multiplicity") + need(sum(p.values()) <= paid_count_bound(targets, paid, v, b, c), "complete paid-count bound") + target_mass = sum(k * count for k, count in t.items()) + paid_mass = sum(k * count for k, count in p.items()) + expected_surplus = sum(k * count for k, count in targets.items()) ** v - sum(k * count for k, count in paid.items()) ** v + need(target_mass - paid_mass == expected_surplus, "product/completion/split rank-mass conservation") + products += 1 + raw_t = {int(k): n for k, n in selected["targets"].items()} + raw_p = {int(k): n for k, n in selected["paid"].items()} + b, c = selected["strictification"]["floor"], selected["strictification"]["cutoff"] + reduced_t, reduced_p = literal_completion(raw_t, raw_p, 1, b, c) + m, L, W, A = max(reduced_t), min(reduced_t), sum(reduced_t.values()), reduced_t[min(reduced_t)] + C = W + sum(reduced_p.values()) + 1 + calibration = [] + for n in (m, m * L - 1, m * L, m * L * L - 1, m * L * L, m * L * L + 1): + got = Flow(reduced_t, reduced_p, n).merged() + h, S = got["height"], got["source_count"] + need(W * A ** h <= S <= W * C ** (h + 1), "selected v=1 source calibration") + calibration.append([n, h, S]) + controls = [] + t, p = literal_completion({2: 10, 5: 1}, {1: 1}, 1, 4, 2) + controls.append(rejects(lambda: need(sum(p.values()) <= 2, "omitted paid completion"), "omitted-completion")) + controls.append(rejects(lambda: need(10 <= ceildiv(10, 2), "omitted per-call rounding"), "omitted-split-rounding")) + t, _ = literal_completion({2: 1, 9: 1}, {1: 1}, 1, 3, 2) + controls.append(rejects(lambda: need(t[3] >= 2, "unqualified productive floor credit"), "all-targets-counted-at-floor")) + tiny = Flow({3: 1, 9: 1}, {1: 1}, 27).merged() + controls.append(rejects(lambda: need(tiny["source_count"] >= 2 * 2 ** tiny["height"], "inflated root multiplicity"), "inflated-root-lower-bound")) + actual_height = Flow({3: 1, 9: 1}, {1: 1}, 256).G + wrong_upper = (8 - (9).bit_length()) // (3).bit_length() + controls.append(rejects(lambda: need(actual_height <= wrong_upper, "wrong height rounding direction"), "height-rounding-direction")) + return {"source_flows": len(rows), "literal_flows": literal_cases, + "nested_width_lower_checks": nested_cases, "height_bound_checks": height_cases, + "product_pad_split_cases": products, + "selected_v1_source_calibration": calibration, + "source_rows_sha256": sha256(json.dumps(rows, separators=(",", ":")).encode()).hexdigest(), + "negative_controls": controls} + + +def selected_envelope(j): + targets = {int(k): n for k, n in j["targets"].items()} + paid = {int(k): n for k, n in j["paid"].items()} + v, b, c = (j["strictification"][k] for k in ("power", "floor", "cutoff")) + H = j["compiler"]["H"] + need((v, b, c, H) == (1024, 21, 20, 64215200000000), "selected PR4470 parameter context") + W, L, M = sum(targets.values()) ** v, b ** v, max(targets) ** v + A = floor_multiplicity_lower(targets, v, b) + pbar = paid_count_bound(targets, paid, v, b, c) + C = W + pbar + 1 + # M*L^h <= 2^H: upper logs give a lower height; lower logs give an upper height. + h_lower, h_upper = height_bounds(H, M, L) + need(h_lower >= 1, "nonempty lower slab") + x_lower = W.bit_length() - 1 + (h_lower - 1) * (A.bit_length() - 1) + x_upper = W.bit_length() + (h_upper + 1) * C.bit_length() + # These compare coefficients, with N canceled; N itself is never instantiated. + need(1000 * (L - 1) * x_lower > 2943 * L * H, "lower K/N > 2943/1000") + need(1000 * x_upper < 3639 * H, "upper K/N < 3639/1000") + need(4 * x_upper * L < 5 * (L - 1) * x_lower, "coefficient bracket ratio < 5/4") + need(x_upper < 4 * H, "K < 4N for conservative outer substitution") + return {"H": H, "N": f"2^{H}", "tensor_power": v, + "raw_productive_count": sum(targets.values()), "raw_paid_count": sum(paid.values()), + "raw_paid_mass": sum(k * n for k, n in paid.items()), + "raw_targets_at_most_floor": floor_multiplicity_lower(targets, 1, b), + "floor_base": b, "cutoff_base": c, "ambient_base": max(targets), + "floor_log2_bounds": [L.bit_length() - 1, L.bit_length()], + "ambient_log2_bounds": [M.bit_length() - 1, M.bit_length()], + "height_lower": h_lower, "height_upper": h_upper, + "W_log2_upper": W.bit_length(), "A_log2_lower": A.bit_length() - 1, + "W_plus_paid_bound_plus_one_log2_upper": C.bit_length(), + "x_lower": x_lower, "x_upper": x_upper, + "K_over_N_strict_bounds": ["2943/1000", "3639/1000"], + "bracket_ratio_strict_upper": "5/4"} + + +def fit(log2_C): + """Least positive integer L for the predecessor's displayed upward threshold. + + Partition by bit length instead of presuming the stepwise predicate is monotone. + """ + delta, beta = Q(1, 250), Q(69999991, 70000000) + candidates = [] + for bits in range(1, 65): + required = Q(log2_C + 10 + 3 * bits) / ((1 - delta) * beta) + L = max(1 << (bits - 1), ceildiv(required.numerator, required.denominator)) + if L < 1 << bits: + candidates.append(L) + need(bool(candidates), "threshold search range exhausted") + answer = min(candidates) + predicate = lambda L: Q(log2_C + 10 + 3 * legacy_ulog2(L)) / (1 - delta) <= beta * L + need(predicate(answer) and not predicate(answer - 1), "adjacent threshold signs") + return answer + + +def outer_accounting(j, old): + H = j["compiler"]["H"] + v = j["strictification"]["power"] + W = sum(j["targets"].values()) ** v + MP = sum(int(k) * n for k, n in j["paid"].items()) ** v + b = j["strictification"]["floor"] + old_x = legacy_ulog2(W) + (H + 1) * legacy_ulog2(W + MP + W * b ** v + 1) + width_factor = legacy_ulog2(legacy_ulog2(232960) + 3) + previous_complex = H + legacy_ulog2(Q(old_x + 1, H)) + width_factor + 1 + need(previous_complex == 64215200000022, "PR4972 complex-share positive control") + Hb = old["bit_strictification"]["uniform_H1"] + bit_small = legacy_ulog2(Q(2 * (5 * Hb + 27) + 1, Hb)) + inherited_bit = 2 * Hb + bit_small + 1 + width_factor + 1 + need(inherited_bit == 51973930319885, "unchanged predecessor BIT-share arithmetic") + # K < 4N replaces only the complex-width bound; retain c_row=1 and all other tariffs. + new_complex = H + 2 + width_factor + 1 + previous_C = max(previous_complex, inherited_bit, 74) + 2 + new_C = max(new_complex, inherited_bit, 74) + 2 + need((previous_C, new_C) == (64215200000024, 64215200000010), "outer accounting comparison") + return {"assumed_c_row": 1, "inherited_Cw": 232960, "inherited_log2_A_old_upper": 64, + "unchanged_BIT_share_log2_upper": inherited_bit, + "previous_complex_share_log2_upper": previous_complex, + "new_complex_share_log2_upper": new_complex, + "previous_log2_C_upper": previous_C, "new_log2_C_upper": new_C, + "previous_fit_log2_p": fit(previous_C), "new_fit_log2_p": fit(new_C), + "scope": "Same conservative outer-accounting formula and inherited tariffs; not optimal C or supplier admission."} + + +def main(): + need(sys.argv[1:] in ([], ["--emit"]), "usage: verify.py [--emit]") + inputs = authenticated_inputs() + module = ModuleType("authenticated_pr4436_flow") + name = "research/direct-mixed-flow/flow.py" + exec(compile(inputs[name], name, "exec"), module.__dict__) + j = json.loads(inputs["research/joint-helper-lattice/RESULT.json"]) + old = json.loads(inputs["research/query-thinned-controllers/RESULT.json"]) + result = {"schema_version": 1, "evidence_level": "author-checked", + "selected_kappa_unchanged": "60403/20000000", + "envelope": selected_envelope(j), "finite_checks": finite_checks(module.Flow, j), + "conditional_outer_accounting": outer_accounting(j, old)} + need(authenticated_inputs() == inputs, "source bytes changed during replay") + if sys.argv[1:] == ["--emit"]: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(result == json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")), "changed result receipt") + print("PASS_SELECTED_COMPLEX_WIDTH_ENVELOPE " + json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError) as exc: + print("FAIL_SELECTED_COMPLEX_WIDTH_ENVELOPE: " + str(exc), file=sys.stderr) + sys.exit(1)