diff --git a/research/selected-bit-parent-reserve/README.md b/research/selected-bit-parent-reserve/README.md new file mode 100644 index 0000000000..86dacf2f68 --- /dev/null +++ b/research/selected-bit-parent-reserve/README.md @@ -0,0 +1,157 @@ +# An explicit parent reserve for the selected BIT bootstrap + +Under the **retained full-cover and completed ordinary-leaf interfaces**, the selected PR589 nine-stage BIT stopped producer has the uniform parent-stock envelope + +\[ +\log_q S(e,w)\le 8194\,w(1+\log_2 e). +\] + +This supplies the numerical coefficient in PR1965's H3 for the first native bootstrap stage. Its recorded cutoff passes that paper's sufficient stock-fit guard with `sigma=8194`. The result is a conditional space implication, not an implementation of the inherited interfaces, a proof of H2, a new supplier, a new exponent, or adoption of the outer proof. + +The new step is the **selected-producer divisor/depth/restoration argument**, not another headroom calculation. The source pricer already contains the arithmetic `2*(64^2+1)=8194` as part of an outer row allowance. This package explains why that term bounds the stopped parent's stock when ordinary leaves are internally completed, and why the other outer allowances need not be inserted into it. + +## Which producer is being bounded? + +The source-pinned selected assembler in PR1094's `upstream1087.tar.gz`, member `code/assemble.py`, names PR589's ordinary BIT supplier, sets `BIT_L=9`, `BIT_T=32`, `BIT_M=1+7*BIT_L=64`, and binds the complete PR589 receipt by Git blob. The same file prices the **different** complex supplier at `m=73`. The bootstrap parameter is constrained by both savings, but the ordinary stopped producer is the BIT side. + +| Source-bound quantity | Selected value | +|---|---:| +| Atom dimension `m=1+7L`, `L=9` | 64 | +| Live roles | 28,416 | +| Physical roles, including the nine additional work roles | 28,425 | +| Largest good child rank | 42 | +| Bad-class fallback child rank | at most 1 | +| Halving degree | 2, since `2*42^2=3528 < 4096=64^2` | +| Parent reserve coefficient | `2*(64^2+1)=8194` | + +`research/e8-bit-p111-tuned/tune/EXPECTED.json` is the exact blob cited by the selected assembly. The vendored PR510 `assemble9.py` reads the hosted profile and computes `row=DEPTH*(m*m+1)+9909+252=18355`. The selected `adapt9p.py` changes the port/deficit binding, not this row formula. `emit_k.py` records `physical=LIVE+9`. These are authenticated source statements, not a new cold replay of PR589's circuit. + +The historical five-stage `m=120` coefficient 57,604 is not used. Neither is 252 treated as a measured selected leaf reserve. PR1990 correctly leaves a selected binding open; the BIT/complex distinction is material when closing this particular ordinary-bootstrap obligation. + +## Retained hypotheses and exact domain + +Fix one eligible odd prime `q>2^80`, avoiding the selected recipe's finite denominator/rank exclusions, before choosing the widths. Let `e,w` be positive integers and let the coarse atom count satisfy `0<=n<=e`; at the native stage of interest `w=ceil(e^s)` and the body has at most `floor(e/w)` atoms. + +The proof uses the following inherited interfaces explicitly: + +1. **Selected full-cover realization.** The selected `m=64` finite physical recipe is realized over `GL_64(Z/q^w Z)`, with one fresh complete physical-role packet per active coarse level. Its role packet has `P=28425` slots, including work roles. A sufficient level divisor is + `W_q(w)=P*|GL_64(F_q)|*q^(4096*(w-1))`. + The selected all-size/compiler and hosting assumptions are still required to identify these packet slots with the physical word. A finite receipt alone does not construct that identification. +2. **Fixed atom width along a coarse call.** An internal child has atom count at most `r*floor(n/64)`, where `r<=42`; the conservative bad-class compiler has children at most `floor(n/64)`. Calls with `n<64`, peeled remainders, routing and high-part exchanges use completed ordinary operations, rather than another same-level coarse call. +3. **Fresh fields and restoration.** A child can use only the unused quotient of its parent's row packet; already exposed ancestor fields remain complete spectators. Every child returns its supplied row coordinate unchanged. Successive residuals, the two-call ordinary wrapper and other sequential calls reuse restored stock. +4. **Completed leaves.** The previous ordinary algorithm handles all required widths and complete spectators, borrows its own high digits internally and restores its row coordinate. It needs **no additional externally supplied row factor**. This is the reviewed PR185 contract retained by PR387, not an estimate of the leaf's internal memory or running time. + +The generic full-cover cardinality and fixed-width recurrence are in `three-stage-cover-bit.tex`, lines 197–218 and 253–264. That file's displayed geometry is historical `m=67`; its numerical parameters are **not** copied. The present proof derives the cardinality identity for general `m`, then instantiates the selected `m=64` recipe under hypothesis 1. The reviewed PR185 proof, paragraphs “Nested row restoration and fixed tapes”, provides hypothesis 4. The original rows note's inherited old-leaf factor must not be retained a second time when its use is replaced by this stronger completed interface. + +## Reserve theorem + +### 1. Charge the entire level divisor + +Reduction modulo `q` maps `GL_m(Z/q^w Z)` onto `GL_m(F_q)`. Every invertible residue matrix has exactly `q^(m^2*(w-1))` lifts; a matrix over this local ring is invertible exactly when its reduction is. Consequently + +\[ +|GL_m(\mathbb Z/q^w\mathbb Z)| +=|GL_m(\mathbb F_q)|q^{m^2(w-1)}=2`, + +\[ +D(n)\le2\lceil\log_2 n\rceil; +\] + +for `n=0,1` it is zero. Thus in all cases with `n<=e`, + +\[ +D(n)\le2\lceil\log_2\max(1,e)\rceil +\le2(1+\log_2 e). \tag{2} +\] + +No unnamed additive `O(1)` is used. One-level halving is false: `n=128` permits the selected rank-42 child `84>64`. + +### 3. Construct divisible stock, not a product over all calls + +For the same fixed `w`, define + +\[ +S(n,w)=W_q(w)^{D(n)}. +\] + +At a coarse node with depth `d>0`, split a complete row index into its role remainder modulo `W_q(w)` and an unused quotient of size `W_q(w)^(d-1)`. Every child has depth at most `d-1`, so that quotient is divisible by its required reserve. Any excess quotient is an additional complete spectator. Because the child restores its row, the quotient can be reused for each later child. The node's complete endpoint restores its own exposed role field. Induction supplies all nested calls and restores the entire row. + +At a leaf there is no external factor: the ordinary operation supplies its own borrowing under hypothesis 4. Consequently the recurrence is multiplication by **one level divisor along an active path**, not multiplication over siblings, residuals, the two wrapper calls, or bootstrap levels. This is also why the previous ordinary **time** constant does not enter the reserve. If a leaf instead needs external factor `B>1`, the base case becomes `S_leaf=B`; the zero-external conclusion no longer follows. That is a genuine hypothesis, not something finite examples can infer. + +Combining (1) and (2), for the parent construction at every integer `e,w>=1`, + +\[ +\log_q S(n,w)<4097wD(n) +\le8194w(1+\log_2 e). +\] + +Use non-strict `<=` to include the zero-depth case. This is PR1965's H3 with **sigma=8194** under the stated interfaces. At fixed completed bootstrap depth the same proof can be reused, but this package binds and checks only the first native stage. It does not claim a new implementation or all fourteen independently admitted stages. + +## First native cutoff + +From the selected assembly, with exact rational arithmetic, + +``` +s = min(bit_lower, (1-10^-24)*complex_lower) - 10^-27 +a0 = 384599/10^10 +a1 = (1-s)*s + s*a0 +delta = min(s-a1, 1-a1-s, 1-a1-s*(1-a0), 1-s) +L = 4785575287428 +``` + +The independently derived coefficient needs only `ell=ceil(log2(8*8194))=17`. The exact checks prove + +``` +L >= 2 +L*delta^2 >= 36 +L*delta >= 2*(4+17) = 42 +0 < delta <= 1-s +``` + +These are PR1965's sufficient fit premises, so `k=ceil(log_q S(e,w))=2^L`, with `w=ceil(e^s)`. The inherited sufficient-headroom value `floor(L*delta/2)-4=6562783` is included only to show the comparison; it is predecessor arithmetic, not the novelty. The powers `2^L` and huge stock sizes are not materialized. + +This closes the *numerical parent-stock coefficient implication* at this stage under the explicit full-cover/completed-leaf assumptions. H2's cutoff-independent stopped time bound, any other primitive fit condition, and all selected all-size/compiler, common-label, mutable-source, hosting, precision/tape, exact-recovery and analytic obligations remain. The selected result and frozen proofs are unchanged. + +## Reproduction and evidence + +From the repository root, using standard-library CPython 3.12: + +```sh +uv run --python 3.12 --no-project python -I -B research/selected-bit-parent-reserve/verify.py +uv run --python 3.12 --no-project python -I -O -B research/selected-bit-parent-reserve/test_verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/selected-bit-parent-reserve +``` + +The verifier authenticates every external input before reading its semantic fields and authenticates the archive member before parsing it. No predecessor Python is imported or executed. It derives the selected parameters, complete level charge, exact halving and cutoff comparison; independently checks the floor-depth recurrence over 20,001 atom counts; and uses small exact local-ring matrices and row permutations as finite controls for the proof's failure modes. Acceptance uses explicit exceptions, not removable `assert` statements. The regenerated `RESULT.json` payload must compare canonically with the committed one. `--write-result PATH` creates an external receipt and refuses overwrite. + +The finite fixtures support the argument but do not prove its all-width quantifiers; those are proved above. Neither a complete selected cold replay nor a formal kernel is run here. See [TASK.json](TASK.json) for scope, provenance and open questions, [SELECTION.json](SELECTION.json) for the unchanged selection, and [SOURCES.json](SOURCES.json) for exact byte pins. + +## Open next questions + +1. **Realize the retained interfaces.** Construct the selected all-size GL64 role-packet/compiler map with fresh descendant fields and complete spectator preservation. Begin with one parent/child split and the common-label/mutable-source mapping. This would replace hypothesis 1's inherited implementation assumption; the finite cardinality proof cannot do so. +2. **Complete the time implication.** Trace every routing, padding, weighted-leaf, descriptor and high-part-exchange toll to prove H2 whenever stock fits with a cutoff-independent constant. The first step is an explicit quantified stopped recurrence. H3 alone cannot adopt PR1965's outer-proof repair. + +## Attribution and limits + +DreamingOfClouds supplied the selected tuned P111 word and parameterized PR589 pipeline, on eumemic's PR555 base and DreamingOfClouds' PR510 nine-stage work, with the credited geometry, whole-call hosting and compiler lineage. The finite-cover/local-ring and reviewed PR185/PR387 completed-leaf sources supply the retained interfaces. Josie Elliston's PR1956 and PR1965 isolate the carried-constant problem and time/space repair; ToikY's PR1990 independently checks the headroom and insists on the missing selected-source coefficient. Rohan Arun supplied the selected PR1094 assembly on Jeremy Kothe's PR1087 predecessor. Their results and numerical receipts are not claimed as new. + +Prepared by Adam Gall with substantial OpenAI Codex assistance. No independent human review or unconditional multiplication theorem is claimed. Apache-2.0, following the repository and retained source notices. diff --git a/research/selected-bit-parent-reserve/RESULT.json b/research/selected-bit-parent-reserve/RESULT.json new file mode 100644 index 0000000000..aa7ad75794 --- /dev/null +++ b/research/selected-bit-parent-reserve/RESULT.json @@ -0,0 +1,89 @@ +{ + "archive_member_sha256": "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a", + "claim": "Conditional selected BIT parent stock; not all-size implementation or H2", + "finite_floor_depth": { + "atom_counts": 20001, + "maximum": 20000, + "maximum_observed_depth": 12, + "minimum": 0, + "one_level_halving_counterexample": { + "child": 84, + "half": 64, + "parent": 128 + } + }, + "finite_local_rings": [ + { + "invertible": 48, + "m": 2, + "q": 3, + "roles": 2, + "w": 1 + }, + { + "invertible": 3888, + "m": 2, + "q": 3, + "roles": 2, + "w": 2 + }, + { + "invertible": 480, + "m": 2, + "q": 5, + "roles": 2, + "w": 1 + } + ], + "finite_row_reuse": { + "all_rows_restored": true, + "complete_wrapper_calls": 2, + "depth": 3, + "divisor": 3, + "external_leaf_factor": 1, + "rows": 27 + }, + "first_native_cutoff": { + "branch": "native", + "cutoff_log2": 4785575287428, + "exponent": "2676351903605968510955225199374139336419692211991205809803291212685832779316802617926399111/1600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "fit": "k < e/2 for every integer e >= 2^L, under the stated interfaces", + "gap": "4388379286997125724770519885577770614671108008794190196708787314167220683197382073600889/1600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "guard_headroom": 6562783, + "required_log2_8sigma": 17, + "s": "67018507072324140916999892981492927675859083/40000000000000000000000000000000000000000000000", + "sigma": 8194, + "stage": 1 + }, + "selected": { + "halving_degree": 2, + "halving_inequality": [ + 4096, + 3528 + ], + "inherited_outer_row": 18355, + "live": 28416, + "m": 64, + "maxchild": 42, + "parent_sigma": 8194, + "per_level_constant": 1, + "per_level_linear": 4096, + "physical": 28425 + }, + "source_sha256": { + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "research/bootstrap-cutoff-time-space-split/README.md": "e7f215a11a81c02b657bac9ebb904f346d1ae95446f32fda74a4084360c79a86", + "research/bootstrap-depth-audit/sources/pr387/bootstrap-sources/research/community-round8-audit/pr185-proof-reviewed.md": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa", + "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "research/complex-t16-rare-pattern-exchanges/SOURCE.json": "4cfd44cebfe88f4450294239fbea8feecb564338dc3027b76065227f5d19cb6f", + "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86", + "research/e8-bit-p111-tuned/code/adapt9p.py": "14365d0eb8f4a7352edd28816196148fd28d5bbcb36044ebeeb15ca051bca9de", + "research/e8-bit-p111-tuned/tune/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/emit_k.py": "298b16c3d4f58a468ad1a64564c8500cb281414a3f3c0428fd467908eeb4a4b4", + "research/five-stage-source527-banks/proof/three-stage-cover-bit.tex": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511", + "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8", + "research/selected-bootstrap-stock-audit/README.md": "0f3cda98c8382d41dc4f5d905460a4b4ed2854d6f94f20035b150e14825827c6" + }, + "status": "PASS_SELECTED_BIT_PARENT_RESERVE" +} diff --git a/research/selected-bit-parent-reserve/SELECTION.json b/research/selected-bit-parent-reserve/SELECTION.json new file mode 100644 index 0000000000..c140a1ae89 --- /dev/null +++ b/research/selected-bit-parent-reserve/SELECTION.json @@ -0,0 +1,132 @@ +{ + "seed": "19a31e1280d5046cfc25b85ee44c9719", + "track": "adversarial-audit", + "suggestions": [ + { + "task_id": "uniform-transfer-audit", + "scope_key": "603f341b99f590f17a76", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "method": "Prove one missing implication with explicit quantified hypotheses.", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "selected-stock-envelope", + "scope_key": "eee4a5467dd91c47ef45", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "method": "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "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" + ], + "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 #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.", + "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 of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.", + "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." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "supplier-boundary-audit", + "scope_key": "66632af6c86d34fb0fdc", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "method": "Trace one hypothesis through the source, checker and complete caller.", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "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", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/selected-bit-parent-reserve/SOURCES.json b/research/selected-bit-parent-reserve/SOURCES.json new file mode 100644 index 0000000000..9ca42df408 --- /dev/null +++ b/research/selected-bit-parent-reserve/SOURCES.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/bootstrap-cutoff-time-space-split/README.md", + "usage": "input", + "git_blob": "59986cb4b0a912ab18883a4f41dedae0fda1a5ae", + "sha256": "e7f215a11a81c02b657bac9ebb904f346d1ae95446f32fda74a4084360c79a86" + }, + { + "path": "research/bootstrap-depth-audit/sources/pr387/bootstrap-sources/research/community-round8-audit/pr185-proof-reviewed.md", + "usage": "input", + "git_blob": "93a588a73a38050dfa0a383cb44f228aff6f243e", + "sha256": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/SOURCE.json", + "usage": "input", + "git_blob": "1e43afd08c060373b6fde3c775c23c180cb6a794", + "sha256": "4cfd44cebfe88f4450294239fbea8feecb564338dc3027b76065227f5d19cb6f" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "usage": "input", + "git_blob": "2970ef79b0441e937449bed30f68f2e0558186ba", + "sha256": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86" + }, + { + "path": "research/e8-bit-p111-tuned/code/adapt9p.py", + "usage": "input", + "git_blob": "96bbc2ba9bb11984736e34db8b65c1a91e8f842e", + "sha256": "14365d0eb8f4a7352edd28816196148fd28d5bbcb36044ebeeb15ca051bca9de" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "usage": "input", + "git_blob": "238226c568742dd5723b03eabae564a2eaa2bda9", + "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/emit_k.py", + "usage": "input", + "git_blob": "b84c795a045143639efe6aefb0562b3c20a2c9d7", + "sha256": "298b16c3d4f58a468ad1a64564c8500cb281414a3f3c0428fd467908eeb4a4b4" + }, + { + "path": "research/five-stage-source527-banks/proof/three-stage-cover-bit.tex", + "usage": "input", + "git_blob": "f05225d21f92cf8cef21b6e12601d5b4d61991f0", + "sha256": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511" + }, + { + "path": "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex", + "usage": "input", + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8" + }, + { + "path": "research/selected-bootstrap-stock-audit/README.md", + "usage": "input", + "git_blob": "bba25c7feca4f7b6872f550ed4c874b6fe979f62", + "sha256": "0f3cda98c8382d41dc4f5d905460a4b4ed2854d6f94f20035b150e14825827c6" + } + ] +} diff --git a/research/selected-bit-parent-reserve/TASK.json b/research/selected-bit-parent-reserve/TASK.json new file mode 100644 index 0000000000..27aa3869af --- /dev/null +++ b/research/selected-bit-parent-reserve/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 4, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "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" + ], + "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 #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.", + "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 of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.", + "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." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990" + ] + }, + "scope_status": "refined", + "actual_scope": "Derive the parent row-reserve envelope of the selected PR589 nine-stage BIT stopped producer at native bootstrap stage one: m=64, maximum child rank 42, 28425 physical roles. Prove the full-cover divisor/depth recurrence with completed ordinary leaves, then compare the resulting coefficient with the existing stage-one fit guard.", + "scope_change_reason": "The selected assembler's ordinary bootstrap uses the BIT producer with BIT_M=64; the complex m=73 supplier constrains s but is not the ordinary stopped producer. Historical m=120 accounting and the outer 252 allowance are not selected reserve coefficients. This refinement targets H3, not the separate cutoff-independent time hypothesis H2.", + "bottleneck_link": "A source-bound uniform parent-stock envelope can discharge the numerical H3 coefficient needed by the recorded cutoff under the retained full-cover and completed-leaf interfaces, without claiming all-size implementation or a new kappa.", + "budget_minutes": 60, + "stop_rule": "Accept only a quantified proof for all integer e,w>=1 with n<=e, a derivation from the selected divisor and maximum child, exact source authentication, and semantic negative controls. If the full-cover/leaf interface is absent, state it as an explicit conditional premise rather than asserting physical adoption. Do not rerun moment roots or change selected sources.", + "outcome": "completed", + "evidence": "Written conditional reserve proof and RESULT.json: selected m=64, maxchild=42, physical=28425, parent sigma=8194, native stage-one fit at cutoff_log2=4785575287428. Exact generation passed PASS_SELECTED_BIT_PARENT_RESERVE with 20001 floor cases, 3 local-ring counts and 27 row states. Registered replay also exercises semantic/source controls.", + "author": "Adam Gall with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for source analysis, proof, implementation and documentation; no independent human review claimed.", + "assignment_seed": "19a31e1280d5046cfc25b85ee44c9719", + "selection": "SELECTION.json", + "method": "Derive |GL_m(Z/q^w)| from reduction modulo q; use all physical roles, exact floor recursion and restored-row reuse; compare sigma with the sufficient guard by integer arithmetic.", + "domain": "One fixed native stage with e>=1, atom width w=ceil(e^s), coarse atom count n<=e, fixed eligible odd prime q>2^80, and the selected full-cover compiler and completed ordinary-leaf contracts retained as hypotheses.", + "changed_premise": "Replace unquantified parent stock O(w log e) by the explicit selected BIT full-cover recurrence; do not add an external reserve for internally completed leaves.", + "optimistic_complete_bill": "No synthesis or scalar saving proposed. Every selected physical role, every nested active cover factor and the bad-class fallback depth are charged; restored sequential calls reuse one stock. The paid moment, ordinary time bill and selected kappa remain unchanged. Under the retained contracts the proved parent logarithmic coefficient is 2*(64^2+1)=8194, not an inherited time constant.", + "freshness": { + "upstream_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "submission_checked_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "submission_compatibility": "Read the refreshed workflow guidance; catalogue, selected record and scientific inputs unchanged. Original scientific pins retained.", + "priority_revision": 4, + "open_pr_snapshot_utc": "2026-10-14T19:00:33.696741+00:00", + "discussion_snapshot_utc": "2026-10-14T19:02:09.707625+00:00", + "coverage": "353 open PRs including drafts and 738 discussion/comment/reply records; complete pagination. Refreshed offline targeted overlap at 19:04:04Z returned ten matches, including this package, prior stock audits and separate m=73 depth work. Live PR1965/1990 heads match retained sources; live coefficient search returned none and parent-reserve search found unrelated reserved-scratch echo PR887. Search limits remain; not a novelty certificate.", + "public_discussion_posts": false + }, + "predecessors": [ + {"pr": 589, "author": "DreamingOfClouds", "credit": "Selected tuned P111 nine-stage BIT producer and receipt, on eumemic's PR555 base."}, + {"pr": 510, "author": "DreamingOfClouds", "credit": "Nine-stage row formula, inherited geometry and hosting lineage."}, + {"pr": 185, "author": "retained reviewed PR185 lineage", "credit": "Completed ordinary leaves borrow internally and impose no additional external row stock."}, + {"pr": 1965, "author": "Josie Elliston", "credit": "Time/space cutoff separation and sufficient fit guard."}, + {"pr": 1990, "author": "ToikY", "credit": "Independent stock-headroom audit and explicit missing selected-coefficient boundary."}, + {"pr": 1094, "author": "Rohan Arun", "credit": "Selected assembly, on Jeremy Kothe's PR1087 source."} + ], + "open_questions": [ + { + "question": "Can the selected all-size GL64 full-cover implementation and completed-leaf row interface be constructed without inherited assumptions?", + "why_it_matters": "The reserve proof quantifies those retained interfaces; it does not produce their fixed-tape implementation.", + "first_step": "Implement one parent/child row-field split with the selected common-label and mutable-source compiler, preserving complete spectator prefixes.", + "blocked_by": "The selected record expressly retains all-size/compiler, hosting, precision and tape assumptions." + }, + { + "question": "Does the selected stopped time estimate hold whenever the stock fits, with a cutoff-independent constant?", + "why_it_matters": "H3 alone does not complete PR1965's H2 time premise or adopt the outer proof.", + "first_step": "Trace all scalar, routing, padding, stopped-leaf and high-part-exchange tolls with their quantified width domains.", + "blocked_by": "This package proves a space envelope only, not the separate time/descriptor implementation bound." + } + ] +} diff --git a/research/selected-bit-parent-reserve/VERIFY.json b/research/selected-bit-parent-reserve/VERIFY.json new file mode 100644 index 0000000000..431de0dc9b --- /dev/null +++ b/research/selected-bit-parent-reserve/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/bootstrap-cutoff-time-space-split/README.md", + "research/bootstrap-depth-audit/sources/pr387/bootstrap-sources/research/community-round8-audit/pr185-proof-reviewed.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/complex-t16-rare-pattern-exchanges/SOURCE.json", + "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "research/e8-bit-p111-tuned/code/adapt9p.py", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/emit_k.py", + "research/five-stage-source527-banks/proof/three-stage-cover-bit.tex", + "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex", + "research/selected-bootstrap-stock-audit/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate selected source and archive member; derive BIT64 parent sigma and native stage-one fit; compare canonical RESULT; exact floor-depth, local-ring and arbitrary-row fixtures." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Fourteen tests under optimization, including source/member corruption, wrong producer, missing work roles, false halving, lost high fibers, insufficient divisible stock, external-leaf countermodel, dirty-row restoration and guard mutations." + } + ] +} diff --git a/research/selected-bit-parent-reserve/test_verify.py b/research/selected-bit-parent-reserve/test_verify.py new file mode 100755 index 0000000000..8b5669bf3e --- /dev/null +++ b/research/selected-bit-parent-reserve/test_verify.py @@ -0,0 +1,120 @@ +#!/usr/bin/env python3 +"""Semantic/source controls, also required under python -O. Apache-2.0.""" +from __future__ import annotations + +import copy +import importlib.util +import io +import json +from pathlib import Path +import tarfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('parent_reserve', HERE / 'verify.py') +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class ReserveTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.data = v.inputs() + cls.assembly, cls.bit, cls.m = v.bind_sources(cls.data) + cls.values = v.parameters(cls.bit, cls.m) + cls.stage = v.cutoff(cls.assembly, cls.values['parent_sigma']) + + def test_selected_dimension_not_complex_or_historical(self): + for m in (73, 120): + with self.subTest(m=m), self.assertRaisesRegex(v.Rejected, 'ordinary dimension'): + v.parameters(self.bit, m) + + def test_all_physical_work_roles_are_charged(self): + mutant = copy.deepcopy(self.bit) + mutant['nine']['bit']['physical'] -= 9 + with self.assertRaisesRegex(v.Rejected, 'nine additional roles'): + v.parameters(mutant, self.m) + + def test_one_level_halving_is_false(self): + self.assertEqual(42 * (128 // 64), 84) + self.assertGreater(84, 128 // 2) + mutant = copy.deepcopy(self.bit) + mutant['nine']['bit']['halving_depth'] = 1 + with self.assertRaisesRegex(v.Rejected, 'halving degree'): + v.parameters(mutant, self.m) + + def test_uncharged_larger_child_is_rejected(self): + mutant = copy.deepcopy(self.bit) + mutant['nine']['profile']['46'] = mutant['nine']['profile'].pop('42') + with self.assertRaisesRegex(v.Rejected, 'maximum child'): + v.parameters(mutant, self.m) + self.assertGreater(2 * 46 ** 2, 64 ** 2) + + def test_high_matrix_fibers_do_not_cancel_from_stock(self): + actual = 2 * v.gl_size(3, 2, 2) + omitted_fibers = 2 * v.gl_size(3, 2, 1) + self.assertEqual(actual, omitted_fibers * 3 ** 4) + with self.assertRaisesRegex(v.Rejected, 'divisible descendant stock'): + v.require_stock(omitted_fibers, actual, 1) + + def test_role_factor_is_not_free(self): + group = v.gl_size(3, 2, 2) + with self.assertRaisesRegex(v.Rejected, 'divisible descendant stock'): + v.require_stock(group, 2 * group, 1) + + def test_one_missing_nested_packet_is_rejected(self): + v.require_stock(27, 3, 3) + with self.assertRaisesRegex(v.Rejected, 'divisible descendant stock'): + v.require_stock(9, 3, 3) + + def test_sequential_calls_reuse_but_do_not_erase_leaf_obligation(self): + self.assertEqual(v.row_smoke()['rows'], 27) + with self.assertRaisesRegex(v.Rejected, 'divisible descendant stock'): + v.require_stock(27, 3, 3, external_leaf=3) + + def test_arbitrary_dirty_row_requires_every_restoration(self): + for failed_depth in (1, 2, 3): + with self.subTest(depth=failed_depth): + outputs = [v.row_program(row, 3, 3, failed_depth) for row in range(27)] + self.assertNotEqual(outputs, list(range(27))) + + def test_existing_sufficient_guard_rejects_next_headroom_bit(self): + row = self.stage + v.fit_guard(row['cutoff_log2'], v.Q(row['gap']), v.Q(row['s']), + row['guard_headroom']) + with self.assertRaisesRegex(v.Rejected, 'stock-fit guard'): + v.fit_guard(row['cutoff_log2'], v.Q(row['gap']), v.Q(row['s']), + row['guard_headroom'] + 1) + self.assertEqual(row['sigma'], 8194) + self.assertEqual(row['required_log2_8sigma'], 17) + + def test_recorded_stage_cannot_be_rebound(self): + mutant = copy.deepcopy(self.assembly) + mutant['bootstrap'][0]['cutoff_log2'] = str(self.stage['cutoff_log2'] - 1) + with self.assertRaisesRegex(v.Rejected, 'cutoff reconstruction'): + v.cutoff(mutant, 8194) + + def test_source_tamper_is_rejected_before_semantic_read(self): + pins = json.loads((HERE / 'SOURCES.json').read_bytes())['files'] + pin = next(p for p in pins if p['path'] == v.BIT) + with self.assertRaisesRegex(v.Rejected, 'source SHA256'): + v.authenticate(self.data[v.BIT] + b' ', pin) + + def test_archive_member_pin_is_not_just_container_success(self): + member = v.archive_member(self.data, 'code/assemble.py') + b'\n# mutation\n' + output = io.BytesIO() + with tarfile.open(fileobj=output, mode='w:gz') as archive: + info = tarfile.TarInfo('code/assemble.py') + info.size = len(member) + archive.addfile(info, io.BytesIO(member)) + mutant = dict(self.data) + mutant[v.ARCHIVE] = output.getvalue() + with self.assertRaisesRegex(v.Rejected, 'archive member SHA256'): + v.archive_member(mutant, 'code/assemble.py') + + def test_small_local_ring_census_is_not_float_arithmetic(self): + self.assertEqual([row['invertible'] for row in v.local_ring_smoke()], [48, 3888, 480]) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/selected-bit-parent-reserve/verify.py b/research/selected-bit-parent-reserve/verify.py new file mode 100755 index 0000000000..8b3ecc7e37 --- /dev/null +++ b/research/selected-bit-parent-reserve/verify.py @@ -0,0 +1,290 @@ +#!/usr/bin/env python3 +"""Selected BIT parent-reserve implication; stdlib only, no predecessor execution. + +Adam Gall with substantial OpenAI Codex assistance. Apache-2.0. +""" +from __future__ import annotations + +import argparse +import ast +import hashlib +import io +import json +import math +from pathlib import Path +import tarfile +from fractions import Fraction as Q + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +BIT = 'research/e8-bit-p111-tuned/tune/EXPECTED.json' +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' +ARCHIVE = 'research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz' +ARCHIVE_SOURCE = 'research/complex-t16-rare-pattern-exchanges/SOURCE.json' +PRICER = 'research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py' +ADAPT = 'research/e8-bit-p111-tuned/code/adapt9p.py' +EMITTER = ('research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/' + 'e8-r715-eleven-stage-whole/code/emit_k.py') + + +class Rejected(ValueError): + """A source, semantic premise or certificate failed.""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise Rejected(message) + + +def sha(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def blob(data: bytes) -> str: + return hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + + +def authenticate(data: bytes, pin: dict) -> bytes: + require(sha(data) == pin['sha256'], 'source SHA256: ' + pin['path']) + require(blob(data) == pin['git_blob'], 'source Git blob: ' + pin['path']) + return data + + +def inputs() -> dict[str, bytes]: + manifest = json.loads((PACKAGE / 'SOURCES.json').read_bytes()) + require(manifest['base_commit'] == '564148b82ae9df72163f22106f15e73efca8aff2', + 'scientific base') + return {p['path']: authenticate((ROOT / p['path']).read_bytes(), p) + for p in manifest['files'] if p['usage'] == 'input'} + + +def assignment(tree: ast.AST, name: str) -> ast.expr: + matches = [node.value for node in ast.walk(tree) if isinstance(node, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == name for t in node.targets)] + require(len(matches) == 1, 'unique source assignment: ' + name) + return matches[0] + + +def expression(tree: ast.AST, name: str, expected: str) -> None: + actual = ast.dump(assignment(tree, name), include_attributes=False) + want = ast.dump(ast.parse(expected, mode='eval').body, include_attributes=False) + require(actual == want, 'source expression: ' + name) + + +def archive_member(data: dict[str, bytes], name: str) -> bytes: + pins = json.loads(data[ARCHIVE_SOURCE])['files'] + with tarfile.open(fileobj=io.BytesIO(data[ARCHIVE]), mode='r:gz') as archive: + member = archive.getmember(name) + require(member.isfile(), 'archive member is regular file') + stream = archive.extractfile(member) + require(stream is not None, 'archive member data') + result = stream.read() + require(sha(result) == pins[name], 'archive member SHA256: ' + name) + return result + + +def bind_sources(data: dict[str, bytes]) -> tuple[dict, dict, int]: + selected = json.loads(data['certificates/selected-result.json']) + require(selected['certificate'] == ASSEMBLY, 'selected assembly path') + require(selected['certificate_sha256'] == sha(data[ASSEMBLY]), 'selected certificate digest') + assembly = json.loads(data[ASSEMBLY]) + require(assembly['kappa'] == selected['kappa'], 'selected kappa unchanged') + citation = assembly['bit_supplier'] + require(citation['pr'] == 589 and citation['path'] == BIT, 'selected BIT producer') + require(citation['commit'] == 'a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46', 'PR589 source head') + require(citation['git_blob_sha1'] == blob(data[BIT]), 'selected BIT blob') + bit = json.loads(data[BIT]) + require(assembly['bit_lower'] == bit['nine']['bit_lower'], 'selected BIT saving') + source = archive_member(data, 'code/assemble.py') + tree = ast.parse(source) + expression(tree, 'BIT_M', '1 + 7 * BIT_L') + expression(tree, 'BIT_K', '(BIT_L - 1) // 2') + tuples = [n for n in tree.body if isinstance(n, ast.Assign) + and any(isinstance(t, ast.Tuple) + and [x.id for x in t.elts if isinstance(x, ast.Name)] == ['BIT_L', 'BIT_T'] + for t in n.targets)] + require(len(tuples) == 1, 'selected stage/replica binding') + stages, replicas = ast.literal_eval(tuples[0].value) + require((stages, replicas) == (9, 32), 'selected nine-stage recipe') + expression(tree, 'BIT_BLOB', repr(blob(data[BIT]))) + pricer = ast.parse(data[PRICER]) + expression(pricer, 'physical', 'W + 9') + expression(pricer, 'row', 'DEPTH * (m * m + 1) + 9909 + 252') + # Adaptation's only pricer edits bind ports and deficit; no source is executed. + adapt = ast.parse(data[ADAPT]) + edits = assignment(adapt, 'EDITS') + require(isinstance(edits, ast.Dict), 'adaptation edit map') + pricer_edits = [v for k, v in zip(edits.keys, edits.values) + if isinstance(k, ast.Constant) and k.value == 'assemble9.py'] + require(len(pricer_edits) == 1, 'unique selected pricer adaptation') + replacements = ast.literal_eval(pricer_edits[0].elts[1]) + require(len(replacements) == 2, 'selected pricer adaptation count') + require(all('row' not in old + new and 'physical' not in old + new + for old, new in replacements), 'reserve formula unchanged by adaptation') + emitter = ast.parse(data[EMITTER]) + physical = [n.value for n in ast.walk(emitter) if isinstance(n, ast.keyword) + and n.arg == 'physical'] + require(len(physical) == 1 and ast.dump(physical[0]) == ast.dump( + ast.parse('LIVE + 9', mode='eval').body), 'selected hosted physical roles') + return assembly, bit, 1 + 7 * stages + + +def ceil_q(value: Q) -> int: + return -(-value.numerator // value.denominator) + + +def ceil_log2(n: int) -> int: + require(type(n) is int and n >= 1, 'positive integer logarithm input') + return (n - 1).bit_length() + + +def parameters(bit: dict, m: int) -> dict: + nine = bit['nine'] + profile = {int(r): count for r, count in nine['profile'].items()} + require(m == 64, 'selected ordinary dimension, not complex or historical dimension') + require(all(type(c) is int and c > 0 and 1 <= r < m for r, c in profile.items()), + 'positive proper child inventory') + record = nine['bit'] + live = 2 * 4 * bit['word']['v'] * 32 + require(live == record['live'] == 28416, 'selected live roles') + physical = live + 9 + require(physical == record['physical'] == 28425, 'all nine additional roles charged') + require(max(profile) == record['maxchild'] == 42, 'selected maximum child') + require(sum(r * c for r, c in profile.items()) == record['rank_mass'], 'selected rank mass') + degree = record['halving_depth'] + require(type(degree) is int and degree == 2, 'selected halving degree') + require(2 * max(profile) ** degree < m ** degree, 'strict halving') + coefficient = degree * (m * m + 1) + require(record['row_coefficient'] == coefficient + 9909 + 252, 'inherited row decomposition') + require(physical < 2 ** 80, 'all physical roles below eligible q') + return dict(m=m, live=live, physical=physical, maxchild=max(profile), + halving_degree=degree, halving_inequality=[m ** degree, 2 * max(profile) ** degree], + per_level_linear=m * m, per_level_constant=1, + parent_sigma=coefficient, inherited_outer_row=record['row_coefficient']) + + +def fit_guard(L: int, gap: Q, s: Q, ell: int) -> None: + require(L >= 2 and L * gap ** 2 >= 36 and L * gap >= 2 * (4 + ell), + 'sufficient stock-fit guard') + require(0 < gap <= 1 - s, 'stock exponent gap') + + +def cutoff(assembly: dict, sigma: int) -> dict: + require(type(sigma) is int and sigma > 0, 'positive integral stock coefficient') + s = min(Q(assembly['bit_lower']), (1 - Q(1, 10 ** 24)) * Q(assembly['complex_lower'])) - Q(1, 10 ** 27) + a0 = Q(384599, 10 ** 10) + a1 = (1 - s) * s + s * a0 + gap = min(s - a1, 1 - a1 - s, 1 - a1 - s * (1 - a0), 1 - s) + require(0 < a0 < a1 < s < 1 - a1, 'selected native stage domain') + recorded = assembly['bootstrap'][0] + L = int(recorded['cutoff_log2']) + require(Q(recorded['exponent']) == a1 and Q(recorded['gap']) == gap, 'selected native stage binding') + require(L == max(ceil_q(36 / gap ** 2), ceil_q(1032 / gap)), 'recorded cutoff reconstruction') + ell = ceil_log2(8 * sigma) + fit_guard(L, gap, s, ell) + return dict(stage=1, branch='native', s=str(s), exponent=str(a1), gap=str(gap), + cutoff_log2=L, sigma=sigma, required_log2_8sigma=ell, + guard_headroom=(L * gap // 2) - 4, + fit='k < e/2 for every integer e >= 2^L, under the stated interfaces') + + +def depth_smoke(profile: dict[str, int], m: int, limit: int = 20000) -> dict: + ranks = sorted(int(r) for r in profile) + depths = [0] * (limit + 1) + for n in range(m, limit + 1): + children = [r * (n // m) for r in ranks] + require(all(0 <= child < n for child in children), 'proper floor child') + depths[n] = 1 + max(depths[child] for child in children) + require(depths[n] <= 2 * ceil_log2(n), 'all-rank finite depth bound') + x, greedy = n, 0 + while x >= m: + x = max(ranks) * (x // m) + greedy += 1 + require(depths[n] == greedy, 'independent greedy/all-rank depth comparison') + return dict(atom_counts=limit + 1, minimum=0, maximum=limit, + maximum_observed_depth=max(depths), + one_level_halving_counterexample={'parent': 128, 'child': 84, 'half': 64}) + + +def gl_size(q: int, m: int, w: int) -> int: + require(q >= 2 and m >= 1 and w >= 1, 'cardinality domain') + return math.prod(q ** m - q ** j for j in range(m)) * q ** (m * m * (w - 1)) + + +def local_ring_smoke() -> list[dict]: + rows = [] + for q, w in ((3, 1), (3, 2), (5, 1)): + modulus = q ** w + count = sum(math.gcd(a * d - b * c, modulus) == 1 + for a in range(modulus) for b in range(modulus) + for c in range(modulus) for d in range(modulus)) + expected = gl_size(q, 2, w) + require(count == expected, 'independent local-ring determinant census') + require(2 * count < q ** (4 * w + 1), 'charged toy physical-role divisor') + rows.append(dict(q=q, w=w, m=2, invertible=count, roles=2)) + return rows + + +def row_program(row: int, divisor: int, depth: int, omit_restore_at: int = -1) -> int: + """Finite semantic fixture: two sequential children and a restored fresh role.""" + if depth == 0: + return row + unused, role = divmod(row, divisor) + routed = (role + 1) % divisor + for _ in range(2): + unused = row_program(unused, divisor, depth - 1, omit_restore_at) + restored = routed if depth == omit_restore_at else (routed - 1) % divisor + return unused * divisor + restored + + +def require_stock(stock: int, divisor: int, depth: int, external_leaf: int = 1) -> None: + required = divisor ** depth * external_leaf + require(stock > 0 and stock % required == 0, 'complete divisible descendant stock') + + +def row_smoke() -> dict: + divisor, depth = 3, 3 + stock = divisor ** depth + require_stock(stock, divisor, depth) + for row in range(stock): + first = row_program(row, divisor, depth) + second = row_program(first, divisor, depth) + require(first == second == row, 'arbitrary row restoration and sequential reuse') + return dict(divisor=divisor, depth=depth, rows=stock, complete_wrapper_calls=2, + all_rows_restored=True, external_leaf_factor=1) + + +def result() -> dict: + data = inputs() + assembly, bit, m = bind_sources(data) + values = parameters(bit, m) + return dict(status='PASS_SELECTED_BIT_PARENT_RESERVE', + claim='Conditional selected BIT parent stock; not all-size implementation or H2', + source_sha256={path: sha(value) for path, value in sorted(data.items())}, + archive_member_sha256=sha(archive_member(data, 'code/assemble.py')), + selected=values, first_native_cutoff=cutoff(assembly, values['parent_sigma']), + finite_floor_depth=depth_smoke(bit['nine']['profile'], m), + finite_local_rings=local_ring_smoke(), finite_row_reuse=row_smoke()) + + +def compare(actual: dict, expected: dict) -> None: + require(actual == expected, 'canonical RESULT payload mismatch') + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', type=Path, help='create a new external receipt, never overwrite') + args = parser.parse_args() + observed = result() + if args.write_result is not None: + require(args.write_result.resolve() != (PACKAGE / 'RESULT.json').resolve(), 'external receipt only') + with args.write_result.open('x') as stream: + json.dump(observed, stream, indent=2, sort_keys=True) + stream.write('\n') + else: + compare(observed, json.loads((PACKAGE / 'RESULT.json').read_bytes())) + print(observed['status'], 'm=64 sigma=8194 stage=1 floor_cases=20001 local_rings=3 row_states=27') + + +if __name__ == '__main__': + main()