From 0645bf7da2f979194a3fa29acae9d4885f5bad0f Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 15:02:34 -0400 Subject: [PATCH 1/3] Prove conditional uniform bootstrap time bound --- .../selected-bootstrap-uniform-time/README.md | 262 ++++++++++++ .../RESULT.json | 51 +++ .../SELECTION.json | 65 +++ .../SOURCES.json | 80 ++++ .../selected-bootstrap-uniform-time/TASK.json | 102 +++++ .../VERIFY.json | 41 ++ .../selected-bootstrap-uniform-time/verify.py | 390 ++++++++++++++++++ 7 files changed, 991 insertions(+) create mode 100644 research/selected-bootstrap-uniform-time/README.md create mode 100644 research/selected-bootstrap-uniform-time/RESULT.json create mode 100644 research/selected-bootstrap-uniform-time/SELECTION.json create mode 100644 research/selected-bootstrap-uniform-time/SOURCES.json create mode 100644 research/selected-bootstrap-uniform-time/TASK.json create mode 100644 research/selected-bootstrap-uniform-time/VERIFY.json create mode 100755 research/selected-bootstrap-uniform-time/verify.py diff --git a/research/selected-bootstrap-uniform-time/README.md b/research/selected-bootstrap-uniform-time/README.md new file mode 100644 index 0000000000..fd173fe16e --- /dev/null +++ b/research/selected-bootstrap-uniform-time/README.md @@ -0,0 +1,262 @@ +# A cutoff-independent time bill for the selected bootstrap + +This package proves a **conditional uniform lifting lemma** for the time +hypothesis (H2) in [Josie Elliston's PR1965](https://github.com/CrocSwap/integer-mult-bounds/pull/1965). +It separates the uniform recurrence and completed-wrapper premises from the +conclusion instead of promoting an asymptotic estimate to an all-width one. +For the **native first stage** of selected PR1094, the inherited paid moment +certificate gives an explicit bound + +``` +K = C * max(401501, 2*sigma) +``` + +when every named primitive coefficient below is at most C. This is a bound in +unknown implementation and stock constants, **not** their measurement. No +stock coefficient is supplied, no cutoff is changed, and no new supplier, +kappa, full all-size implementation or formal-kernel theorem is claimed. + +PR1956 identified the carried-time-constant problem; PR1965 proved that time +constants can be absorbed after H2 is available; [ToikY's PR1990](https://github.com/CrocSwap/integer-mult-bounds/pull/1990) +explicitly retained both H2 uniformity and the unknown H3 stock coefficient. +The contribution here is the uniform implication with a complete bill and a +source-bound rational constant. It does not repeat their fourteen stock +headrooms or import the historical m=120 reserve coefficient. + +## Precise premises + +Fix q >= 2, 0 <= a <= s < 1 with s > 0, p = 1-a and tau = 1-s. All widths +are positive integers. The radix and primitive implementations are fixed +before widths and any bootstrap cutoff are chosen. Write a' = (1-s)s+s*a. + +1. **Uniform stopped primitive.** For nonnegative coefficients c_r on integers + 1 <= r < m and m >= 2, normalized time T(n,w) satisfies, for every w >= 1, + + ``` + T(0,w) = 0 + T(n,w) <= Cleaf*w^p (1 <= n < m) + T(n,w) <= sum_r c_r*T(r*floor(n/m),w) + + Cadapt*n + Cpeel*w^p (n >= m). + ``` + + The constants are nonnegative, independent of n, w and the cutoff, and + uniform over the allowed complete spectators and generated prefix controls. + The same normalized recurrence is stated in `notes/stopped-product-interface.tex`, + lines 31-53. The uniform primitive implementation, especially the logical + volume normalization, remains an inherited premise; the finite word does + not prove it. Let g1 and gt be certified positive lower bounds on + `1-sum c_r*(r/m)` and `1-sum c_r*(r/m)^tau`. +2. **Completed endpoints and wrapper tolls.** Each reversed call restores its + row, preserves complete spectators, and has the stated endpoint. Each of + the three ordinary-wrapper shifts costs at most Cshift*n per unit logical + volume. One outer row padding/unpadding, including its scans and bookkeeping, + costs at most Cpad*V, and the padded volume is less than 2V. The completed + old algorithm exchanges residual digits for at most Crem*V*w^p and the + high parts for at most Chi*V*k^p. These are actual charge hypotheses, not + free operations. The constants include radix-to-binary conversions inside + old leaves, their fixed multiplicities, and permitted spectator handling. + PR185's reviewed contract and the retained `three-stage-cover-rows.tex` + explain these calls and restore their rows before reuse. +3. **Fit and stock.** At the particular width e under consideration, set + `w=ceil(e^s)`, take an integer `0 <= k < e/2`, and require + `k <= ceil(sigma*w*(1+log2(e)))`, for fixed sigma >= 0. The actual borrowed + width `ceil(log_q S(e,w))` satisfies this implication if H3 holds. We do not + derive H3 or assume its historical 252 or 57604 constants. Put + `n=floor((e-k)/w)`; the residual contains fewer than w digits. + +These premises are stronger than an eventual big-O statement. A finite spike +in a leaf's cost can satisfy an eventual estimate while violating a proposed +all-width coefficient. The verifier includes such a counterexample. No +unknown spike is silently placed below the selected recorded cutoff. + +## Uniform lifting lemma and proof + +Define + +``` +A = Cadapt/g1 +B = max(Cleaf, Cpeel/gt). +``` + +Strong induction on n proves `T(n,w) <= A*n+B*n^tau*w^p` for every w and n. +At a non-leaf, `r*floor(n/m) <= (r/m)*n < n`. The linear term leaves at +least `g1*A*n = Cadapt*n`. The stopped term leaves at least +`gt*B*n^tau*w^p >= Cpeel*w^p`. For 1 <= n < m, `n^tau >= 1` and B >= Cleaf; +n=0 is the empty body. This is the inherited weighted induction with its +constants and all-width quantifiers made explicit; it is not a new recurrence. + +The complete normalized bill, before estimating powers, is + +``` +(4*A + 6*Cshift)*n + 4*B*n^tau*w^p + + Cpad + Crem*w^p + Chi*k^p. (1) +``` + +The factor four pays **two** reversed calls on a row volume less than **twice** +the original volume. The factor six pays three shifts on that padded volume. +Padding occurs once outside the recursion. The residual and high-part calls +are completed ordinary calls after restriction to the genuine row range; +their internal borrowing is included in Crem and Chi. The five-operation +ordinary wrapper is chronological, not a raw reversed call substituted for +an ordinary one. Nothing in (1) changes recursive child multiplicities. + +For every e >= 1, `e^s <= w <= 2*e^s`, `n <= e/w <= e^(1-s)`, and + +``` +n^tau*w^p <= e^tau*w^(s-a) + <= 2^(s-a)*e^(tau+s*(s-a)) + <= 2*e^(1-a'). +``` + +The nonnegative exponent s-a is a stated premise. For integer k >= 1, +`k^p <= k`; for k=0 both are zero. Thus + +``` +k^p <= 2*sigma*e^s*(1+log2(e)) + 1. +``` + +The ceiling's extra one and Cpad are absorbed by `e^(1-s) >= 1`, not omitted. +Consequently (1) is at most + +``` +K * [e^(1-s) + e^(1-a') + e^s*(1+log2(e)) + w^(1-a)], + +K = max(4*A+6*Cshift+Cpad+Chi, 8*B, 2*sigma*Chi, Crem). (2) +``` + +This is H2 on **every width where the named primitive contracts and stock fit +hold**, with no occurrence of a cutoff L or a carried factor `2^(L*Delta a)`. +The inequality is a mathematical implication, not a proof that all selected +primitive implementations meet its premises. It even handles an empty atom +body, which a purely large-width derivation need not discuss. + +For a binary width E, numerical padding to `q^e`, where +`e=ceil(E/log2(q))`, increases logical volume by less than q^2 and has e <= E. +Thus the same conclusion follows with `q^2*K` and powers of E whenever the +radix-width premises hold; fixed conversion scans must be included in Cpad. +This does not assert that a cutoff stated for radix width e is automatically +the same cutoff for binary width E. + +## Polynomial descriptor preparation without another cutoff + +There is one common source of an implicit extra width threshold. The retained +bit proof, lines 136-145, amortizes polynomial generated-descriptor preparation +against a **complete** q^w target fiber. Suppose its work per prefix is bounded +uniformly by `Cdesc*e^d*w^b`, with fixed nonnegative integer d,b. Put +`D=b+ceil(d/s)`. Since e^s <= w, + +``` +Cdesc*e^d*w^b/q^w <= Cdesc*w^D/2^w <= Cdesc*2^D*D! (3) +``` + +for every integer w >= 1. For D >= 1, +`w^D <= D!*binom(w+D-1,D)`, and the positive generating series gives +`sum_(w>=1) binom(w+D-1,D)/2^w = 2^D`; one summand is no larger than the sum. +For D=0 the bound is immediate. This exact factorial overcharge can be folded +into the relevant Cadapt, Cpeel or Cshift coefficient, multiplied by the number +of charged preparation sites. It adds no new cutoff or unit-cost arithmetic +assumption. A separate uniform bound on d,b,Cdesc and the number of sites is +still required. An incomplete fiber cannot use (3); that failure is an exact +negative control, not an assertion about the selected implementation. + +## Native selected first-stage binding + +All source pins are in [SOURCES.json](SOURCES.json), on main +`564148b82ae9df72163f22106f15e73efca8aff2`, priority revision 4. The chooser's +independent seed is `3c6ed534c7c882d069b0dc2c8cd99397` ([SELECTION.json](SELECTION.json)). +The selected record binds the assembly and its PR589 BIT supplier. The latter +has **m=64**, W=28416, maximum child 42 and the paid profile in `EXPECTED.json`. +The selected complex m=73 producer is not substituted for it. + +The frozen PR1087 assembler specifies the surcharge +`10^-16 * 32*m^2*sum(H_r)/W` additional rank-one children and + +``` +s = min(bit_lower, (1-10^-24)*complex_lower) - 10^-27, +a = 384599/10^10. +``` + +The selected receipt certifies the surcharged moment at bit_lower; both +retained exact upper endpoints are strictly below one. **We authenticate and +reuse that certificate, not recalculate another moment root or claim an +independent supplier replay.** The first-stage exponent is checked against +its recorded value. Exact rational arithmetic gives + +``` +g1 = 16326904278023 / 2890625000000000, +gt = (11/32)*(bit_lower-s) + = 25504319623965913202561177203577795565550087 + / 1280000000000000000000000000000000000000000000000. +``` + +Here gt is a new explicit **sufficient gap transfer**, not an estimated moment: +for x <= rho=42/64 and d=bit_lower-s in (0,1), concavity gives +`x^d <= 1-d*(1-x) <= 1-d*(1-rho)` (the tangent at one). Multiplying the inherited +moment terms at exponent `1-bit_lower` yields `mu_(1-s) < 1-gt`. All coefficients, +including the rank-one surcharge, are nonnegative. Hence `A <= C/g1` and +`B <= C/gt` if all seven coefficients in the premises are at most C. Exact +cross multiplication certifies + +``` +4/g1+8 < 717, +8/gt < 401501, +``` + +so (2) follows with `K=C*max(401501,2*sigma)`. This conservatively pays every +term in (1). It proves no bound on C or sigma and does not assert favorable +practical constants. For example, descriptor degree d=1,b=0 alone becomes +D=597 in (3); that remains a fixed finite time constant, not a stock charge. + +## Reproduction and evidence boundary + +``` +uv run --python 3.12 --no-project python -I -B research/selected-bootstrap-uniform-time/verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/selected-bootstrap-uniform-time +``` + +The registered replay runs the exact checker both normally and under `-O`. +Source hashes are checked before data are consumed; archived Python is read, +never executed. The checker compares the canonical regenerated JSON object +with [RESULT.json](RESULT.json). The finite evidence includes independent +recursion-tree sums versus dynamic programming, exact square comparisons for +rational specializations of the all-width bound, charged padding and complete +endpoint fixtures, factorial inequalities, and semantic/source/receipt mutants. +The universal claim rests on the written induction and inequalities, not the +finite sample. No full selected cold replay or hosted CI success is claimed. + +Observed with CPython 3.12: the scientific smoke and registered normal/optimized +replays pass. Each replay checks 6,156 recurrence cases, 539 complete wrapper +bills, 1,664 descriptor inequalities and 1,458 padded endpoints; all 17 controls +reject. The output includes `PASS_SELECTED_BOOTSTRAP_UNIFORM_TIME` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. This evidence does not measure C or sigma. + +## Open next questions + +- Bind each actual selected primitive implementation to the uniform constants + and preparation-site counts in the premises. First inspect logical-volume + normalization, fixed-tape parking and generated prefix work; the inherited + all-size/compiler and tape contracts still block unconditional adoption. +- Derive the actual selected stock envelope sigma with a same-domain producer + and depth argument. This is the separate H3 obligation and is not solved by + a large coefficient cap or by the explicit time constant above. +- Apply the lemma at later stages only after their preceding completed ordinary + contract is established; C may grow with the fixed stage, but must not hide + a width- or cutoff-dependent premise. The result here binds native stage one. + +[Task metadata](TASK.json) records the initial question, complete optimistic +bill, bounded overlap coverage and limits. Claims are confined to this package +and its PR; no discussion post is required. + +## Credit + +Josie Elliston supplied PR1956's carry audit and PR1965's time/space separation; +ToikY supplied PR1990's independent stock-fit audit and explicit H2/H3 limits. +Rohan Arun supplied the reviewed PR185 completed-leaf argument and selected +PR1094 assembly; Jeremy Kothe supplied PR1087's frozen selected producer. +The stopped recurrence and three-stage row/weighted-atom proofs retain their +original repository lineage; eumemic's PR589/PR555 BIT supplier is used through +its authenticated selected receipt. These predecessor constructions and the +weighted-induction method are not claimed as new. + +Prepared by Adam Gall with substantial OpenAI Codex assistance. Apache-2.0. +No independent human or formal-kernel review is claimed. diff --git a/research/selected-bootstrap-uniform-time/RESULT.json b/research/selected-bootstrap-uniform-time/RESULT.json new file mode 100644 index 0000000000..86ea58ea2e --- /dev/null +++ b/research/selected-bootstrap-uniform-time/RESULT.json @@ -0,0 +1,51 @@ +{ + "status": "PASS_SELECTED_BOOTSTRAP_UNIFORM_TIME", + "scope": "Conditional uniform lifting lemma; native selected stage1; no stock coefficient or supplier adoption", + "source_files_authenticated": 10, + "archive_members_authenticated": 1, + "selected_stage": { + "m": 64, + "W": 28416, + "maxchild": 42, + "a": "384599/10000000000", + "s": "67018507072324140916999892981492927675859083/40000000000000000000000000000000000000000000000", + "a_prime": "2676351903605968510955225199374139336419692211991205809803291212685832779316802617926399111/1600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "rank_one_surcharge": "4713/11291503906250", + "linear_gap": "16326904278023/2890625000000000", + "stopped_gap_lower": "25504319623965913202561177203577795565550087/1280000000000000000000000000000000000000000000000", + "linear_coefficient_strict_upper": 717, + "stopped_coefficient_strict_upper": 401501, + "K_if_each_primitive_coefficient_at_most_C": "C*max(401501,2*sigma)", + "descriptor_degree_for_d1_b0": 597, + "moment_certificate": "Inherited authenticated acceptance; no root recomputation" + }, + "recursion_tree_and_induction_cases": 6156, + "complete_wrapper_bill_cases": 539, + "descriptor_inequality_cases": 1664, + "padded_complete_endpoint_cases": 1458, + "controls_rejected": [ + "non_strict_moment", + "negative_cost", + "omitted_leaf_charge", + "omitted_node_charge", + "omitted_padding_multiplier", + "omitted_high_exchange", + "unrestored_row", + "incomplete_fiber", + "eventual_not_uniform_leaf", + "missing_selected_surcharge", + "non_strict_inherited_receipt", + "changed_selected_profile", + "detached_stage_exponent", + "source_byte_drift", + "archive_member_drift", + "negative_square_bound", + "changed_regenerated_receipt" + ], + "remaining_premises": [ + "uniform primitive/compiler and normalized logical-volume contracts", + "actual same-domain stock envelope sigma", + "inherited exact endpoint and tape contracts" + ] +} diff --git a/research/selected-bootstrap-uniform-time/SELECTION.json b/research/selected-bootstrap-uniform-time/SELECTION.json new file mode 100644 index 0000000000..7a5123e8eb --- /dev/null +++ b/research/selected-bootstrap-uniform-time/SELECTION.json @@ -0,0 +1,65 @@ +{ + "seed": "3c6ed534c7c882d069b0dc2c8cd99397", + "track": "adversarial-audit", + "suggestions": [ + { + "task_id": "selected-stock-envelope", + "scope_key": "f5c32b23bcd01d2e356d", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "method": "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope.", + "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": "dcdb0fa8e49b08a958d0", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "method": "Construct one semantically invalid but superficially well-formed fixture and test rejection.", + "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." + }, + { + "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." + } + ], + "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-bootstrap-uniform-time/SOURCES.json b/research/selected-bootstrap-uniform-time/SOURCES.json new file mode 100644 index 0000000000..cdd5faa669 --- /dev/null +++ b/research/selected-bootstrap-uniform-time/SOURCES.json @@ -0,0 +1,80 @@ +{ + "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": "notes/stopped-product-interface.tex", + "usage": "input", + "git_blob": "20c44ce4866fa972ce64365dcf365b1659a83050", + "sha256": "454a8f3924afc26e575b2a8cec6d0860397cb7f2dc431f3ba63fb8a7142cc96b" + }, + { + "path": "research/bootstrap-cutoff-time-space-split/README.md", + "usage": "input", + "git_blob": "59986cb4b0a912ab18883a4f41dedae0fda1a5ae", + "sha256": "e7f215a11a81c02b657bac9ebb904f346d1ae95446f32fda74a4084360c79a86" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "usage": "input", + "git_blob": "2970ef79b0441e937449bed30f68f2e0558186ba", + "sha256": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86" + }, + { + "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/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "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" + } + ], + "archive_members": [ + { + "path": "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "member": "code/assemble.py", + "sha256": "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a", + "usage": "Read-only coefficient, moment and first-stage formula binding; never executed" + } + ] +} diff --git a/research/selected-bootstrap-uniform-time/TASK.json b/research/selected-bootstrap-uniform-time/TASK.json new file mode 100644 index 0000000000..433def1a4d --- /dev/null +++ b/research/selected-bootstrap-uniform-time/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 4, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read 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_status": "refined", + "actual_scope": "Prove a cutoff-independent complete time bound for the native first selected ordinary-bootstrap stage, conditional on explicit uniform primitive and stock contracts. Derive PR1965 H2 from the floor/stopped recurrence, padding, two reversed body calls, three shifts, residual digits and high-part exchange; isolate descriptor preprocessing with an all-width bound instead of an unspecified sufficiently-large-width condition.", + "scope_change_reason": "The emitted uniform-transfer card is refined to the H2 obligation explicitly retained by PR1965 and PR1990. This is separate from computing the selected producer's H3 reserve coefficient and does not repeat the fourteen headroom calculations.", + "bottleneck_link": "A cutoff chosen solely for stock fit is justified only if the remaining time bill is uniform whenever the stock fits. An explicit conditional lifting lemma removes the asymptotic-to-uniform inference without adopting the selected all-size producer.", + "budget_minutes": 60, + "stop_rule": "Complete the quantified lifting lemma and source-bound exact corroboration. If a primitive's all-width contract is unavailable, name it as a remaining premise rather than assuming it or claiming full H2 adoption. No supplier synthesis or selected-frontier edit.", + "outcome": "completed", + "evidence": "Written uniform induction, complete wrapper bill and factorial descriptor absorption. Final scientific smoke passed: 6156 independent recursion-tree/dynamic-programming and induction cases, 539 complete wrapper bills, 1664 descriptor inequalities, 1458 literal padded endpoints, and 17 semantic/source/receipt controls. Selected native stage1 gives K=C*max(401501,2*sigma), with C and sigma explicitly conditional. No new moment-root replay or supplier admission.", + "author": "Adam Gall", + "ai_assistance": "Substantial OpenAI Codex assistance. No formal-kernel or independent human verification is claimed.", + "assignment_seed": "3c6ed534c7c882d069b0dc2c8cd99397", + "track": "adversarial-audit", + "selected_method": "Prove one missing implication with explicit quantified hypotheses.", + "question": "Which explicit uniform premises suffice to derive the selected native first-stage H2 bound independently of a stock-fit cutoff?", + "changed_premise": "Replace the unexpanded H2 assumption by a stated uniform node/leaf recurrence and complete wrapper toll contract. The selected stock envelope remains a separate hypothesis.", + "domain": "Integer radix-q widths e>=1, fixed q>=2, atom width ceil(e^s), integer borrowed stock 0<=k 0 for v in h.values()), "positive child counts") + m, width = 64, nine["bit"]["live"] + require(width == 28416 and max(h) == nine["bit"]["maxchild"] == 42, + "selected producer dimensions") + require(sum(r * count for r, count in h.items()) == nine["bit"]["rank_mass"], + "selected profile mass") + moment = [row for row in assembly["moments"] + if row["side"] == "bit" and row["accept"] is True] + require(len(moment) == 1, "one inherited accepting BIT moment") + moment = moment[0] + require(moment["surcharge"] is True and Q(moment["endpoint"]) == b, + "inherited moment model") + for engine in ("mercator", "base_two"): + low, high = map(Q, moment[engine]) + require(-1 < low <= high < 0, "inherited moment upper endpoint") + s = min(b, (1 - Q(1, 10**24)) * Q(assembly["complex_lower"])) - Q(1, 10**27) + a = Q(384599, 10**10) + require(0 <= a < s < b < 1, "stage exponent domain") + aprime = (1 - s) * s + s * a + require(aprime == Q(assembly["bootstrap"][0]["exponent"]), "first-stage exponent") + coefficients = {r: Q(count, width) for r, count in h.items()} + surcharge = Q(32 * m * m * sum(h.values()), 10**16 * width) + coefficients[1] += surcharge + mu1 = sum(value * Q(r, m) for r, value in coefficients.items()) + g1 = 1 - mu1 + rho = Q(max(coefficients), m) + gt = (1 - rho) * (b - s) + require(0 < g1 < 1 and 0 < gt < 1, "positive rational gaps") + require(4 / g1 + 8 < 717 and 8 / gt < 401501, "uniform time coefficient") + return { + "m": m, "W": width, "maxchild": max(coefficients), + "a": str(a), "s": str(s), "a_prime": str(aprime), + "bit_lower": str(b), "rank_one_surcharge": str(surcharge), + "linear_gap": str(g1), "stopped_gap_lower": str(gt), + "linear_coefficient_strict_upper": 717, + "stopped_coefficient_strict_upper": 401501, + "K_if_each_primitive_coefficient_at_most_C": "C*max(401501,2*sigma)", + "descriptor_degree_for_d1_b0": ceil(1 / s), + "moment_certificate": "Inherited authenticated acceptance; no root recomputation", + } + + +def constants(g1, gt, cadapt, cpeel, cleaf, cshift, cpad, crem, chi, sigma): + require(g1 > 0 and gt > 0, "strict moment gaps") + require(all(x >= 0 for x in (cadapt, cpeel, cleaf, cshift, cpad, crem, chi, sigma)), + "nonnegative costs and stock coefficient") + A, B = cadapt / g1, max(cleaf, cpeel / gt) + K = max(4 * A + 6 * cshift + cpad + chi, 8 * B, 2 * sigma * chi, crem) + return A, B, K + + +def sqrt_leq(coefficient, radicand, bound): + """Check coefficient*sqrt(radicand) <= bound, with exact sign handling.""" + require(coefficient >= 0 and radicand >= 0, "square comparison domain") + return bound >= 0 and coefficient * coefficient * radicand <= bound * bound + + +def table_cost(m, children, nmax, w, cadapt, cpeel, cleaf): + values = [Q(0)] + for n in range(1, nmax + 1): + if n < m: + values.append(cleaf * w) + else: + values.append(sum(c * values[r * (n // m)] for r, c in children.items()) + + cadapt * n + cpeel * w) + return values + + +def tree_cost(m, children, n, w, cadapt, cpeel, cleaf): + """Independent explicit tree sum: no dynamic-programming cache or bound.""" + pending = [(Q(1), n)] + total = Q(0) + while pending: + weight, width = pending.pop() + if width == 0: + continue + if width < m: + total += weight * cleaf * w + else: + total += weight * (cadapt * width + cpeel * w) + quotient, _ = divmod(width, m) + pending.extend((weight * c, r * quotient) for r, c in children.items()) + return total + + +def admit_node(actual, n, w, A, B): + remainder = actual - A * n + require(remainder <= 0 or remainder**2 <= B * B * w * w * n, + "uniform induction bound") + + +def admit_wrapper(n, w, k, A, B, cshift, cpad, crem, chi, rhs): + base = (4 * A + 6 * cshift) * n + cpad + crem * w + chi * k + require(sqrt_leq(4 * B * w, n, rhs - base), "complete H2 bill") + + +def recursion_cases(): + # s=1/2, a=0. Perfect-square ratios make both moments rational. + families = [(4, {1: Q(1, 2)}), (9, {1: Q(1, 2), 4: Q(1, 2)}), + (16, {1: Q(1, 2), 4: Q(1)})] + checked = 0 + for m, children in families: + mu1 = sum(c * Q(r, m) for r, c in children.items()) + mutau = sum(c * Q(isqrt(r), isqrt(m)) for r, c in children.items()) + require(isqrt(m)**2 == m and all(isqrt(r)**2 == r for r in children), + "rational square-root fixture") + A, B, _ = constants(1 - mu1, 1 - mutau, Q(2), Q(3), Q(5), + Q(0), Q(0), Q(0), Q(0), Q(0)) + for w in (1, 2, 7, 31): + values = table_cost(m, children, 512, w, Q(2), Q(3), Q(5)) + for n, actual in enumerate(values): + require(actual == tree_cost(m, children, n, w, Q(2), Q(3), Q(5)), + "tree and dynamic recurrence disagree") + admit_node(actual, n, w, A, B) + checked += 1 + return checked + + +def wrapper_cases(): + g1, gt = Q(23, 32), Q(3, 8) # m=16 family in recursion_cases. + cadapt, cpeel, cleaf = Q(2), Q(3), Q(5) + cshift, cpad, crem, chi = Q(7), Q(11), Q(13), Q(17) + checked = 0 + for sigma in (Q(1, 100), Q(1, 2), Q(1), Q(3), Q(10)): + A, B, K = constants(g1, gt, cadapt, cpeel, cleaf, cshift, cpad, crem, chi, sigma) + for j in range(5): + e, w, ep = 16**j, 4**j, 8**j # e^s, e^(1-a') for s=1/2,a=0. + top = min((e - 1) // 2, ceil(sigma * w * (1 + 4 * j))) + ks = range(top + 1) if e <= 256 else sorted({0, min(1, top), top // 2, top}) + for k in ks: + n = (e - k) // w + rhs = K * (w + ep + w * (1 + 4 * j) + w) + admit_wrapper(n, w, k, A, B, cshift, cpad, crem, chi, rhs) + require(n * w <= e - k < (n + 1) * w, "residual width") + checked += 1 + # Empty body can occur at small widths: s=3/4,e=9,w=6,k=4. + require(5**4 < 9**3 <= 6**4 and 2 * 4 < 9 and (9 - 4) // 6 == 0, + "empty atom-body boundary") + require(tree_cost(16, {1: Q(1)}, 0, 6, Q(2), Q(3), Q(5)) == 0, + "empty body costs no recursive call") + return checked + + +def descriptor_cases(): + checked = 0 + for degree in range(13): + cap = 2**degree * factorial(degree) + partial = Q(0) + for w in range(1, 129): + term = comb(w + degree - 1, degree) + require(w**degree <= factorial(degree) * term, "rising factorial inequality") + partial += Q(term, 2**w) + require(partial < 2**degree, "positive series partial sum") + require(Q(w**degree, 2**w) <= cap, "all-width descriptor cap") + checked += 1 + return checked + + +def ordinary_body(head, data, row, restore=True): + """Literal five-operation wrapper on two radix-3 atoms; arbitrary row.""" + h, d = divmod(head, 3), divmod(data, 3) + d = tuple((y - x) % 3 for x, y in zip(h, d)) + # A completed reversed call may temporarily leave the genuine row range. + row = (row + 1) % 4 + h, d = d[::-1], h[::-1] + row = (row - 1) % 4 + d = tuple((y + x) % 3 for x, y in zip(h, d)) + row = (row + 1) % 4 + h, d = d[::-1], h[::-1] + if restore: + row = (row - 1) % 4 + d = tuple((x - y) % 3 for x, y in zip(h, d)) + return 3 * h[0] + h[1], 3 * d[0] + d[1], row + + +def endpoint_cases(): + # q=3,k=1, body range 9, two spectator values, row divisor 2. + # Genuine preceding row range 3 pads to 4, a nondivisible case. + checked = 0 + for hhi in range(3): + for dh in range(3): + for hb in range(9): + for db in range(9): + for spectator in range(2): + left, right, row = ordinary_body(hb, db, hhi) + z, other = spectator, dh + require(row < 3, "genuine padded range invariant") + completed = (other, left, z, row, right) + require(completed == (dh, db, spectator, hhi, hb), + "completed high/body interchange") + checked += 1 + return checked + + +def rejection(action, expected): + try: + action() + except ValueError as exc: + require(expected in str(exc), "wrong rejection: " + str(exc)) + return + raise ValueError("control was accepted: " + expected) + + +def controls(record, assembly, bit, payloads, sources): + rejected = [] + + def check(name, action, expected): + rejection(action, expected) + rejected.append(name) + + zero = Q(0) + check("non_strict_moment", lambda: constants(zero, Q(1), *([Q(1)] * 8)), + "strict moment gaps") + check("negative_cost", lambda: constants(Q(1), Q(1), Q(-1), *([Q(1)] * 7)), + "nonnegative costs") + # Build the independent actual costs, then delete the charged coefficient. + leaf = tree_cost(16, {}, 1, 1, zero, zero, Q(10)) + check("omitted_leaf_charge", lambda: admit_node(leaf, 1, 1, zero, zero), + "uniform induction bound") + node = tree_cost(16, {}, 16, 1, Q(1), zero, zero) + check("omitted_node_charge", lambda: admit_node(node, 16, 1, zero, zero), + "uniform induction bound") + # q^k=3, divisor=2: compare two calls on the actual padded logical volume. + exact_padding = Q(ceil(Q(3, 2)) * 2, 3) + check("omitted_padding_multiplier", + lambda: require(2 * exact_padding <= 2, "padded body bill"), "padded body bill") + # Actual Chi=1; a proposed bound obtained by deleting Chi pays nothing. + _, _, missing_high_K = constants(Q(1), Q(1), *([zero] * 7), Q(1)) + check("omitted_high_exchange", + lambda: admit_wrapper(9, 16, 100, zero, zero, zero, zero, zero, Q(1), + missing_high_K * (16 + 64 + 144 + 16)), + "complete H2 bill") + # Mutate the literal wrapper's second row restoration, not the expected tuple. + check("unrestored_row", + lambda: require(ordinary_body(1, 5, 2, restore=False)[2] < 3, + "genuine row restriction"), "genuine row restriction") + cap = 2**3 * factorial(3) + check("incomplete_fiber", lambda: require(100**3 <= cap, "fiber normalization"), + "fiber normalization") + # Cost equals w except for w=7, so its eventual coefficient is one. + spike = lambda w: 1000 if w == 7 else w + require(all(spike(w) == w for w in range(8, 32)), "eventual spike fixture") + check("eventual_not_uniform_leaf", + lambda: admit_node(Q(spike(7)), 1, 7, zero, Q(1)), "uniform induction bound") + bad = deepcopy(assembly) + bad["surcharge_model"]["bit"] = False + check("missing_selected_surcharge", lambda: selected_stage(record, bad, bit), "BIT surcharge") + bad2 = deepcopy(assembly) + for row in bad2["moments"]: + if row["side"] == "bit" and row["accept"]: + row["base_two"][1] = "0" + check("non_strict_inherited_receipt", lambda: selected_stage(record, bad2, bit), + "inherited moment upper") + bad3 = deepcopy(bit) + bad3["nine"]["profile"]["1"] += 1 + check("changed_selected_profile", lambda: selected_stage(record, assembly, bad3), + "selected profile mass") + bad4 = deepcopy(assembly) + bad4["bootstrap"][0]["exponent"] = "0" + check("detached_stage_exponent", lambda: selected_stage(record, bad4, bit), + "first-stage exponent") + corrupt = dict(payloads) + corrupt[BIT] += b" " + check("source_byte_drift", lambda: authenticate(corrupt, sources), "source hash") + bad_sources = deepcopy(sources) + bad_sources["archive_members"][0]["sha256"] = "0" * 64 + check("archive_member_drift", lambda: authenticate(payloads, bad_sources), "archive member hash") + require(not sqrt_leq(Q(1), 1, Q(-1)), "square sign guard") + rejected.append("negative_square_bound") + return rejected + + +def compare_receipt(expected, actual): + require(expected == actual, "canonical receipt mismatch") + + +def evaluate(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + payloads = {row["path"]: (ROOT / row["path"]).read_bytes() + for row in sources["files"] if row["usage"] == "input"} + source_count = authenticate(payloads, sources) + record = json.loads(payloads["certificates/selected-result.json"]) + require(record["certificate_sha256"] == digest(payloads[ASSEMBLY]), "selected receipt hash") + assembly, bit = json.loads(payloads[ASSEMBLY]), json.loads(payloads[BIT]) + stage = selected_stage(record, assembly, bit) + result = { + "status": "PASS_SELECTED_BOOTSTRAP_UNIFORM_TIME", + "scope": "Conditional uniform lifting lemma; native selected stage1; no stock coefficient or supplier adoption", + "source_files_authenticated": source_count, + "archive_members_authenticated": len(sources["archive_members"]), + "selected_stage": stage, + "recursion_tree_and_induction_cases": recursion_cases(), + "complete_wrapper_bill_cases": wrapper_cases(), + "descriptor_inequality_cases": descriptor_cases(), + "padded_complete_endpoint_cases": endpoint_cases(), + "controls_rejected": controls(record, assembly, bit, payloads, sources), + "remaining_premises": ["uniform primitive/compiler and normalized logical-volume contracts", + "actual same-domain stock envelope sigma", "inherited exact endpoint and tape contracts"], + } + altered = deepcopy(result) + altered["selected_stage"]["stopped_coefficient_strict_upper"] -= 1 + rejection(lambda: compare_receipt(altered, result), "canonical receipt mismatch") + result["controls_rejected"].append("changed_regenerated_receipt") + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path, help="write once to a new output path") + args = parser.parse_args() + result = evaluate() + if args.write_receipt: + with args.write_receipt.open("x", encoding="utf-8") as stream: + json.dump(result, stream, indent=2) + stream.write("\n") + else: + compare_receipt(json.loads((PACKAGE / "RESULT.json").read_text()), result) + print(result["status"], "stage=1", "K=C*max(401501,2*sigma)", + "recurrence_cases=" + str(result["recursion_tree_and_induction_cases"]), + "wrapper_cases=" + str(result["complete_wrapper_bill_cases"]), + "controls_rejected=" + str(len(result["controls_rejected"]))) + + +if __name__ == "__main__": + main() From 950943420913dae9aec8cd07ef94ba2d0392a1ab Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 15:05:01 -0400 Subject: [PATCH 2/3] Keep semantic controls and record submission provenance --- research/selected-bootstrap-uniform-time/README.md | 6 ++++-- research/selected-bootstrap-uniform-time/RESULT.json | 3 +-- research/selected-bootstrap-uniform-time/TASK.json | 7 ++++++- research/selected-bootstrap-uniform-time/VERIFY.json | 2 +- research/selected-bootstrap-uniform-time/verify.py | 4 ---- 5 files changed, 12 insertions(+), 10 deletions(-) diff --git a/research/selected-bootstrap-uniform-time/README.md b/research/selected-bootstrap-uniform-time/README.md index fd173fe16e..1e8bea9b5c 100644 --- a/research/selected-bootstrap-uniform-time/README.md +++ b/research/selected-bootstrap-uniform-time/README.md @@ -220,13 +220,15 @@ never executed. The checker compares the canonical regenerated JSON object with [RESULT.json](RESULT.json). The finite evidence includes independent recursion-tree sums versus dynamic programming, exact square comparisons for rational specializations of the all-width bound, charged padding and complete -endpoint fixtures, factorial inequalities, and semantic/source/receipt mutants. +endpoint fixtures, factorial inequalities, and semantic/source controls. The +padding, incomplete-fiber and finite-spike fixtures are mathematical countermodels +to weakened hypotheses, not reports of bugs in the selected implementation. The universal claim rests on the written induction and inequalities, not the finite sample. No full selected cold replay or hosted CI success is claimed. Observed with CPython 3.12: the scientific smoke and registered normal/optimized replays pass. Each replay checks 6,156 recurrence cases, 539 complete wrapper -bills, 1,664 descriptor inequalities and 1,458 padded endpoints; all 17 controls +bills, 1,664 descriptor inequalities and 1,458 padded endpoints; all 16 controls reject. The output includes `PASS_SELECTED_BOOTSTRAP_UNIFORM_TIME` and `PASS_REGISTERED_RESEARCH_PACKAGE`. This evidence does not measure C or sigma. diff --git a/research/selected-bootstrap-uniform-time/RESULT.json b/research/selected-bootstrap-uniform-time/RESULT.json index 86ea58ea2e..2fa3e2a1a1 100644 --- a/research/selected-bootstrap-uniform-time/RESULT.json +++ b/research/selected-bootstrap-uniform-time/RESULT.json @@ -40,8 +40,7 @@ "detached_stage_exponent", "source_byte_drift", "archive_member_drift", - "negative_square_bound", - "changed_regenerated_receipt" + "negative_square_bound" ], "remaining_premises": [ "uniform primitive/compiler and normalized logical-volume contracts", diff --git a/research/selected-bootstrap-uniform-time/TASK.json b/research/selected-bootstrap-uniform-time/TASK.json index 433def1a4d..b7a2cf1cf7 100644 --- a/research/selected-bootstrap-uniform-time/TASK.json +++ b/research/selected-bootstrap-uniform-time/TASK.json @@ -46,7 +46,7 @@ "budget_minutes": 60, "stop_rule": "Complete the quantified lifting lemma and source-bound exact corroboration. If a primitive's all-width contract is unavailable, name it as a remaining premise rather than assuming it or claiming full H2 adoption. No supplier synthesis or selected-frontier edit.", "outcome": "completed", - "evidence": "Written uniform induction, complete wrapper bill and factorial descriptor absorption. Final scientific smoke passed: 6156 independent recursion-tree/dynamic-programming and induction cases, 539 complete wrapper bills, 1664 descriptor inequalities, 1458 literal padded endpoints, and 17 semantic/source/receipt controls. Selected native stage1 gives K=C*max(401501,2*sigma), with C and sigma explicitly conditional. No new moment-root replay or supplier admission.", + "evidence": "Written uniform induction, complete wrapper bill and factorial descriptor absorption. Final scientific smoke and registered normal/-O replays: 6156 independent recursion-tree/dynamic-programming and induction cases, 539 complete wrapper bills, 1664 descriptor inequalities, 1458 literal padded endpoints, and 16 mathematical countermodel/semantic/source controls. Selected native stage1 gives K=C*max(401501,2*sigma), with C and sigma explicitly conditional. No new moment-root replay, selected implementation bug, or supplier admission is claimed.", "author": "Adam Gall", "ai_assistance": "Substantial OpenAI Codex assistance. No formal-kernel or independent human verification is claimed.", "assignment_seed": "3c6ed534c7c882d069b0dc2c8cd99397", @@ -82,6 +82,11 @@ "priority_revision": 4, "guidance_read": "Updated autoresearch discussion/handoff guidance and priority-log workflow follow-up.", "compatibility": "Only AGENTS.md, autoresearch.md and the priority log changed; catalogue, selected record and scientific inputs unchanged. Scientific base and immutable source pins retained.", + "open_pr_snapshot_utc": "2026-10-14T19:00:33.696741+00:00", + "discussion_snapshot_utc": "2026-10-14T19:02:09.707625+00:00", + "targeted_search_utc": "2026-10-14T19:03:36.281396+00:00", + "coverage": "353 open PRs including drafts and 738 discussion/comment/reply records, complete cached pagination. Targeted search includes 1538 local records after adding this package. Live PR1965/1990 dispositions read: both merged. Six targeted matches include this package twice, PR1990, and three historical circuit/recurrence packages; their actual scopes were inspected and are not claims of this uniform H2 implication.", + "limits": "Non-atomic snapshots, cached text and bounded targeted reading do not establish absence of unpublished or unindexed overlap.", "publication_policy": "Self-contained PR only; no separate discussion or status post." }, "selection_note": "One independent draw. Corrected one transcription of a scope string against the original stdout; seed and all mathematical selection fields are unchanged.", diff --git a/research/selected-bootstrap-uniform-time/VERIFY.json b/research/selected-bootstrap-uniform-time/VERIFY.json index 26a934e8a5..cf1db4456e 100644 --- a/research/selected-bootstrap-uniform-time/VERIFY.json +++ b/research/selected-bootstrap-uniform-time/VERIFY.json @@ -24,7 +24,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Authenticated selected first-stage rational constants; independent recursion-tree and dynamic-programming comparisons; complete wrapper and descriptor inequalities; literal padded endpoint and semantic/source/receipt failure controls." + "checks": "Authenticated selected first-stage rational constants; independent recursion-tree and dynamic-programming comparisons; complete wrapper and descriptor inequalities; literal padded endpoint, countermodels to weakened mathematical premises, and semantic/source controls." }, { "argv": [ diff --git a/research/selected-bootstrap-uniform-time/verify.py b/research/selected-bootstrap-uniform-time/verify.py index 19a1cfaf3d..1ad43c3da5 100755 --- a/research/selected-bootstrap-uniform-time/verify.py +++ b/research/selected-bootstrap-uniform-time/verify.py @@ -362,10 +362,6 @@ def evaluate(): "remaining_premises": ["uniform primitive/compiler and normalized logical-volume contracts", "actual same-domain stock envelope sigma", "inherited exact endpoint and tape contracts"], } - altered = deepcopy(result) - altered["selected_stage"]["stopped_coefficient_strict_upper"] -= 1 - rejection(lambda: compare_receipt(altered, result), "canonical receipt mismatch") - result["controls_rejected"].append("changed_regenerated_receipt") return result From b5ffc48e3dd5c92f591bdb4fabafa2c8e8b33970 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 15:06:10 -0400 Subject: [PATCH 3/3] Credit PR589 supplier and PR555 base separately --- research/selected-bootstrap-uniform-time/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/research/selected-bootstrap-uniform-time/README.md b/research/selected-bootstrap-uniform-time/README.md index 1e8bea9b5c..0ab96ab833 100644 --- a/research/selected-bootstrap-uniform-time/README.md +++ b/research/selected-bootstrap-uniform-time/README.md @@ -256,8 +256,8 @@ ToikY supplied PR1990's independent stock-fit audit and explicit H2/H3 limits. Rohan Arun supplied the reviewed PR185 completed-leaf argument and selected PR1094 assembly; Jeremy Kothe supplied PR1087's frozen selected producer. The stopped recurrence and three-stage row/weighted-atom proofs retain their -original repository lineage; eumemic's PR589/PR555 BIT supplier is used through -its authenticated selected receipt. These predecessor constructions and the +original repository lineage; DreamingOfClouds's PR589 BIT supplier, on eumemic's +PR555 base, is used through its authenticated selected receipt. These constructions and the weighted-induction method are not claimed as new. Prepared by Adam Gall with substantial OpenAI Codex assistance. Apache-2.0.