From 1a4b266db28db3e2e4e5cd95af28695bddaf0a21 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 15:12:21 -0400 Subject: [PATCH 1/2] Prove fresh-row conditioning for the selected stopped cover --- .../selected-cover-fresh-fibers/README.md | 239 +++++++++++ .../selected-cover-fresh-fibers/RESULT.json | 143 +++++++ .../SELECTION.json | 80 ++++ .../selected-cover-fresh-fibers/SOURCES.json | 72 ++++ .../selected-cover-fresh-fibers/TASK.json | 93 +++++ .../selected-cover-fresh-fibers/VERIFY.json | 31 ++ .../selected-cover-fresh-fibers/verify.py | 370 ++++++++++++++++++ 7 files changed, 1028 insertions(+) create mode 100644 research/selected-cover-fresh-fibers/README.md create mode 100644 research/selected-cover-fresh-fibers/RESULT.json create mode 100644 research/selected-cover-fresh-fibers/SELECTION.json create mode 100644 research/selected-cover-fresh-fibers/SOURCES.json create mode 100644 research/selected-cover-fresh-fibers/TASK.json create mode 100644 research/selected-cover-fresh-fibers/VERIFY.json create mode 100755 research/selected-cover-fresh-fibers/verify.py diff --git a/research/selected-cover-fresh-fibers/README.md b/research/selected-cover-fresh-fibers/README.md new file mode 100644 index 0000000000..e9a7eaaff1 --- /dev/null +++ b/research/selected-cover-fresh-fibers/README.md @@ -0,0 +1,239 @@ +# Fresh row fibers in the selected stopped cover + +**A conditional all-depth address theorem and adversarial audit; no new κ.** +A large enough row reserve and a restored row endpoint are not, by themselves, +enough to justify per-edge bad-class averaging. This package proves the missing +counting implication under the inherited **fresh-field** contract, maps that +contract to the selected bit producer's source, and gives exact counterexamples +when either invocation predictability or complete padded execution is removed. +It does not assert that the selected compiler violates either condition. + +## Selected object and source boundary + +The scientific base is `564148b82ae9df72163f22106f15e73efca8aff2`, selected #1094, +κ = `836330098538459/500000000000000000`. The ordinary stopped producer is the +selected **PR589 bit supplier**, not the complex supplier of dimension 73. +The frozen PR1087 assembler binds PR589's record by Git blob +`e293ddc557742637f9f679f083a1a282d87b1b13` and SHA256. It gives nine stages, +32 replicas, moment dimension `m=1+7*9=64`, live roles `28416`, physical roles +`28425`, maximum child rank `42`, and the full paid histogram in `RESULT.json`. +The seven native and seven conservative bootstrap stages use the same bit word; +only their scalar bootstrap parameter differs. No cutoff arithmetic is repeated. + +The actual selected finite record is linked through the selected assembly, not +identified by a similarly named historical package. The checker authenticates +all source bytes before parsing, including the archived assembler member. No +predecessor Python is imported or executed. `SOURCES.json` pins the proof texts +and the source chain. These texts retain an all-size compiler hypothesis: the +finite PR589 record is **not** an execution trace over every input width. + +### Exact source-to-hypothesis map + +The line numbers below refer to the pinned files, not moving web text. + +| Source | What it supplies | Use here / what remains conditional | +|---|---|---| +| `five-stage-source527-banks/proof/three-stage-cover-bit.tex` 9–15 | weights may read exposed ancestor rows, never fresh invocation roles or data; complete spectators and row restoration | invocation parameters are fixed on each ancestor cylinder; inherited compiler must implement this restriction | +| same, 32–44 | current routing changes fresh fields; right multiplication changes chart, not the endpoint | current-role routing is a bijection independent of unused descendant stock | +| same, 122–145 | child weight `A_child[kf+j]=A[i_k f+j] D_P[k]`; parent's current fields become child ancestors; child's roles use disjoint stock | a parent's low-residue/pivot choice may select a child, but may not select using that child's future role coordinate | +| same, 161–195 | fallback pivot choices use the parent's low class; resulting children have their own descriptor | adaptive fallback is permitted at the **next** depth: its choice is already an ancestor value there | +| same, 197–218 | `GL_m(Z/q^w Z)` chart `g=g0+qG1`, batched high matrices, role divisor | every low matrix has the same number of high lifts; physical-role factor cancels in the density, not in stock | +| same, 220–228 | per-edge polynomial bad fraction `2m^3/q`, no simultaneous union bound | justified by complete fibers and a fixed list of edge occurrences at each invocation, not by endpoint restoration alone | +| `three-stage-cover-rows.tex` 1–15, 29–60 | stock `W(w)^D`, fresh descendant fields, one outer row padding, completed row restoration | supplies the row-layout and return contract to which the theorem below applies | +| retained PR185 proof, 36–44 | completed inner ordinary leaves borrow internally and return outer spectators | their internal digits are not additional external role factors; their compiler contract is retained | +| frozen PR1087 `code/assemble.py`, `BIT_L/BIT_T`, `load_bit`, `outer_witness` | the selected PR589 record, dimension 64 and finite bootstrap use | binds this audit to the selected supplier; does not prove its all-size read/write discipline | + +The old note's example has dimension 67. We use its **stated structural +contract**, not its old histogram, depth constant, or row coefficient. The +selected finite dimension/profile come from PR589. Portability of the contract +to that selected implementation remains explicitly conditional, as in the +selected review. The new result discharges an implication of that contract; +it does not discharge all-size compiler admission. + +## One-padding conditional-fiber theorem + +Fix integers `W>=2`, `D>=1`, and a genuine row range `Q>=S=W^D`. Let + +``` +T = ceil(Q/S), P = T*S. +``` + +Pad **once**, from `[Q]` to `[P]`, and execute over the entire padded range. +Euclidean division is a bijection + +``` +[P] <-> [T] × [W]^D, +x = (((t*W + r_0)*W + r_1)*W + ...)*W + r_(D-1). +``` + +At depth `j`, the slab `t` and fields `r_0,...,r_(j-1)` are ancestors, +`r_j` is current, and the remaining fields are unused stock. The exact +hypotheses at every invocation boundary are: + +1. The decision that this invocation exists, its width, its fixed edge list and + its weights depend only on its ancestors (and fixed program indices), not on + current/future row fields or data. An ancestor-dependent union of cylinders + is allowed. A child selected by a parent's current residue satisfies this + rule because that field has become a child ancestor. +2. Each current-role route fixes ancestors and unused stock and acts as a + permutation of `[W]` depending only on ancestors. In particular, no unused + stock value selects that permutation. +3. Calls have depth at most `D`; a completed child restores its supplied row + field and preserves ancestor spectators before a sequential sibling uses + it. The ordinary leaf may borrow internally under its own completed contract. +4. The padded rows are not pruned by the genuine/dummy flag during execution. + Only a completed row-restoring endpoint restricts back to `[Q]`. + +**Conclusion.** Every live invocation domain is a disjoint union of complete +suffix cylinders. On fixing one ancestor prefix, each value of its current +role occurs exactly `W^(D-j-1)` times. Every low type in an equal-fiber +partition of that current role has its stated uniform frequency. There is +no per-recursion padding factor: `Q <= P < Q+S <= 2Q`, with `P<2Q` also when +`Q=S`. The original genuine range is invariant at the completed endpoint. + +**Proof.** The root is a full product by Euclidean division. Suppose the claim +holds at a node. Hypothesis 1 selects entire ancestor cylinders, never a +proper subset of the fresh suffix. Hypothesis 2 permutes the current factor +and fixes all later factors, so preserves the full suffix product and its +counting measure. At a child boundary, fixing the parent's current field +merely fixes one more prefix coordinate; every later factor remains complete. +This proves the assertion by induction to depth `D`, including prefix-dependent +stopping and fallback. Hypothesis 3 restores the child row before reuse, so +sequential siblings start with the same product rather than consuming or +multiplying the reserve. The two ordinary-body calls likewise reuse it. +For padding, `ceil(Q/S)=1**, not just the small test rings. + +Fix any invocation's ancestor prefix and any one of its edge occurrences. +The source's bad-minor set has fraction at most `b=2*64^3/q < 10^-16`. +By the theorem, this remains its frequency at the invocation. Sum costs over +edge occurrences and then ancestor prefixes. Linearity of a finite sum, not +independence of bad events, gives the surcharge. There is no need to bound the +probability that *some* edge fails, and no simultaneous union bound. Arbitrary +correlation between the bad sets of two fixed edges is harmless. + +With selected histogram `H`, `E=sum_r H_r`, `L=28416` and exponent `a`, retain +exactly the selected conservative charge + +``` +(1/L) * sum_r H_r*(r/64)^(1-a) + + (1/10^16) * (32*64^2) * E/L * (1/64)^(1-a). +``` + +Every good term stays charged; no displaced-good subtraction is taken. One +outer factor `P/Q<2` is a volume constant, **not** a factor inserted into the +characteristic moment at each level. This audit derives neither a new endpoint +nor a new reserve coefficient. The first-stage fit envelope, H2 time bound, +selected compiler, precision/tape and analytic-transfer obligations remain. + +## Two failures that row restoration cannot detect + +**Current-field adaptive edge choice.** Over `GL_2(F_q)`, index edge predicates +by the `q+1` projective lines `[v]` and let `B_v={g : first_row(g)·v=0}`. +Every fixed `B_v` has fraction `1/(q+1)`: each nonzero first row has exactly one +kernel line, and invertible change of basis permutes the line fibers. Choose +`v` to be the kernel of the **current** first row. The selected edge is then +bad on every matrix. Identity routing and the identity final row map remain +legal bijections; the sole missing hypothesis is that the edge choice be fixed +before reading that invocation's current role. This is a linear-minor example, +not an arbitrary rare-set oracle. It does not allege such a choice in PR589. + +**Skipping dummy rows.** Take `W=3`, `D=2`, `S=9`, `Q=10`, `P=18`. The complete +padded slab `t=1` has three values of `r_0`, each with three values of `r_1`. +In the genuine prefix `[10]`, the cylinder `(t,r_0)=(1,0)` contains only +`r_1=0`. The event `r_1=0` has conditional frequency one rather than one third. +All routes can be identity and the final row map can restore every row. Thus +endpoint restoration justifies **unpadding**, not pruning intermediate +invocations. The package checks these two failures separately. + +## Reproduction and evidence limits + +``` +uv run --python 3.12 --no-project python -I -B research/selected-cover-fresh-fibers/verify.py +uv run --python 3.12 --no-project python -I -O -B research/selected-cover-fresh-fibers/verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/selected-cover-fresh-fibers +``` + +Observed local Python 3.12 smoke and registered optimized replay: + +``` +PASS_SELECTED_COVER_FRESH_FIBERS cases=60 cuts=150 GL_rings=4 controls=9 +PASS_REGISTERED_RESEARCH_PACKAGE research/selected-cover-fresh-fibers outcome=completed +``` + +The 60 mixed-radix cases cover 14,120 padded rows and 2,370 conditional +fibers. The four full small-ring enumerations are `GL_2` over moduli +`3,9,5,25`; the adaptive-minor witnesses use primes `3,5,7`. These finite +domains are explicitly separate from the universal written theorem. + +`RESULT.json` is required and compared with a fresh canonical JSON object. +Explicit `--write-result PATH` creates a new external receipt without +silently replacing an existing file. Exact finite checks exercise mixed-radix +round trips, prefix-dependent bijections and stopping, all low-matrix fibers +of the stated small prime-power rings, both counterexamples, and semantic +mutations. Acceptance uses explicit exceptions, not Python assertions. +Finite runs support the implementation; the all-depth and all-width statements +come from the written proofs above. No whole supplier cold replay, formal +kernel run, or hosted CI result is claimed. + +## Open next questions + +1. **Emit the selected all-size field-dependency certificate.** The concrete + remaining obligation is that every call guard/edge-list/weight read set is + contained in its ancestor fields and every route fixes unused descendant + fields. Start from the child-weight formula and the current chart route, + then annotate the selected emitter's all-size lowering. This is blocked by + that lowering remaining an inherited contract rather than an emitted + address-level artifact; stock magnitude and scalar endpoint checks cannot + substitute for it. +2. **Admit a deliberately adaptive selector only with its new charge.** If a + changed controller chooses an edge after reading current low residues, + compute the fiberwise sum of its chosen bad indicators instead of reusing + the fixed-edge average. Start with a finite partition of low classes. The + obstacle is a favorable fully paid bound, not the mere existence of a + row-restoring permutation. This result supplies no such improved selector. + +## Attribution and provenance + +The source's GL chart, weighted child rule, fresh-role restrictions and per-edge +polynomial bound belong to the retained three-stage-cover framework; its +source527 packaging and finite accounting are credited to eumemic. Rohan Arun +supplied the PR185/PR387 bootstrap lineage and selected PR1094 assembly; +Jeremy Kothe supplied the pinned PR1087 assembler. PR589's tuned bit supplier +retains its credited punctured-E8, nine-stage and hosting lineage. Josie +Elliston's PR1956/1965 and ToikY's PR1990 isolate the stock-fit question; this +package does not claim their cutoff results. `r480-sharp-charge535` and its +PR461/464/465 predecessors already sharpen the numerical bad-class charge; +no such numerical refinement is claimed here. + +Prepared for Adam Gall with substantial OpenAI Codex assistance in mathematics, +code and writing. Apache-2.0. No independent human review is claimed. Selection +nonce `cc5bf62436a3476502c7769e29c2990c`, adversarial-audit, priority revision 4; +`SELECTION.json` preserves the one original draw. The checked upstream +checkpoint `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` changes guidance only; +scientific inputs are retained at the original base. Live/cached overlap +coverage and its limitations are recorded in `TASK.json`. diff --git a/research/selected-cover-fresh-fibers/RESULT.json b/research/selected-cover-fresh-fibers/RESULT.json new file mode 100644 index 0000000000..b13dcfd1b0 --- /dev/null +++ b/research/selected-cover-fresh-fibers/RESULT.json @@ -0,0 +1,143 @@ +{ + "adaptive_minor_counterexamples": [ + { + "adaptive_bad_fraction": "1", + "edges": 4, + "fixed_bad_fraction": "1/4", + "matrices": 48, + "prime": 3, + "row_map": "identity" + }, + { + "adaptive_bad_fraction": "1", + "edges": 6, + "fixed_bad_fraction": "1/6", + "matrices": 480, + "prime": 5, + "row_map": "identity" + }, + { + "adaptive_bad_fraction": "1", + "edges": 8, + "fixed_bad_fraction": "1/8", + "matrices": 2016, + "prime": 7, + "row_map": "identity" + } + ], + "address_audit": { + "cases": 60, + "conditional_fibers": 2370, + "cuts": 150, + "depths": [ + 1, + 4 + ], + "padded_rows": 14120, + "widths": [ + 2, + 6 + ] + }, + "genuine_prefix_counterexample": { + "D": 2, + "W": 3, + "ancestor": [ + 1, + 0 + ], + "genuine": 10, + "genuine_bad_fraction": "1", + "genuine_fresh_values": [ + 0 + ], + "padded": 18, + "padded_bad_fraction": "1/3", + "stock": 9 + }, + "gl2_low_fibers": [ + { + "lifts_per_low_class": 1, + "low_classes": 48, + "matrices": 48, + "power": 1, + "prime": 3 + }, + { + "lifts_per_low_class": 81, + "low_classes": 48, + "matrices": 3888, + "power": 2, + "prime": 3 + }, + { + "lifts_per_low_class": 1, + "low_classes": 480, + "matrices": 480, + "power": 1, + "prime": 5 + }, + { + "lifts_per_low_class": 625, + "low_classes": 480, + "matrices": 300000, + "power": 2, + "prime": 5 + } + ], + "limits": [ + "All-depth theorem uses the written prefix/complete-domain hypotheses.", + "Selected all-size field dependency graph remains an inherited compiler obligation.", + "No stock coefficient, improved root, new supplier or multiplication theorem.", + "Finite matrices are GL2 controls, not enumeration of selected GL64." + ], + "negative_controls_rejected": [ + "current_route_reads_future", + "nonbijective_current_route", + "ancestor_future_alias", + "pruned_padded_domain", + "adaptive_edge_at_fixed_edge_charge", + "omitted_selected_edge", + "live_stock_substituted_for_physical", + "source_byte_corruption", + "unrestored_row_at_unpadding" + ], + "selected": { + "bad_fraction_retained": "1/10000000000000000", + "complete_moment_at_a_zero": "2874298095721977/2890625000000000", + "deficit": 10272, + "edges": 904896, + "fallback_coefficient_before_rank_power": "4713/11291503906250", + "fallback_per_bad_edge": 131072, + "live_roles": 28416, + "m": 64, + "max_child": 42, + "physical_roles": 28425, + "profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "42": 288, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "rank_mass": 1808352, + "scope": "Existing selected bill only; no new moment root or stock coefficient." + }, + "source_sha256": { + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "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/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz:code/assemble.py": "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a", + "research/e8-bit-p111-tuned/tune/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "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/r480-sharp-charge535/README.md": "28355cfc614358eb482d018ba7b21addb0725520fbcd148a0f0f0faaabd03209", + "research/selected-bootstrap-stock-audit/README.md": "0f3cda98c8382d41dc4f5d905460a4b4ed2854d6f94f20035b150e14825827c6" + }, + "status": "PASS_SELECTED_COVER_FRESH_FIBERS" +} diff --git a/research/selected-cover-fresh-fibers/SELECTION.json b/research/selected-cover-fresh-fibers/SELECTION.json new file mode 100644 index 0000000000..889eee05d8 --- /dev/null +++ b/research/selected-cover-fresh-fibers/SELECTION.json @@ -0,0 +1,80 @@ +{ + "seed": "cc5bf62436a3476502c7769e29c2990c", + "track": "adversarial-audit", + "suggestions": [ + { + "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": "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": "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-cover-fresh-fibers/SOURCES.json b/research/selected-cover-fresh-fibers/SOURCES.json new file mode 100644 index 0000000000..5cae3f6bfd --- /dev/null +++ b/research/selected-cover-fresh-fibers/SOURCES.json @@ -0,0 +1,72 @@ +{ + "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-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/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/r480-sharp-charge535/README.md", + "usage": "input", + "git_blob": "1a71dc2b5627ccfc3a242a39e191ba330fe2c58e", + "sha256": "28355cfc614358eb482d018ba7b21addb0725520fbcd148a0f0f0faaabd03209" + }, + { + "path": "research/selected-bootstrap-stock-audit/README.md", + "usage": "input", + "git_blob": "bba25c7feca4f7b6872f550ed4c874b6fe979f62", + "sha256": "0f3cda98c8382d41dc4f5d905460a4b4ed2854d6f94f20035b150e14825827c6" + } + ] +} diff --git a/research/selected-cover-fresh-fibers/TASK.json b/research/selected-cover-fresh-fibers/TASK.json new file mode 100644 index 0000000000..c0bc9688fc --- /dev/null +++ b/research/selected-cover-fresh-fibers/TASK.json @@ -0,0 +1,93 @@ +{ + "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": "changed", + "actual_scope": "Prove the conditional-fiber/address implication needed to turn one padded W(w)^D row reserve into the selected stopped bit producer's per-edge bad-class averaging. Bind selected PR589 m=64, its actual profile and physical roles; give exact single-hypothesis counterexamples to current-fresh-field adaptive edge selection and to executing only the genuine prefix of a padded row range.", + "scope_change_reason": "The concrete missing interface is not another numerical stock coefficient or headroom. The selected ordinary producer is the m=64 bit supplier, while m=73 is the complex supplier. This audit isolates the fresh-field measurability and complete padded execution obligations used by the inherited no-union-bound argument, without duplicating the reserve/depth estimate.", + "bottleneck_link": "A sufficiently large reserve is useful only if its address partition leaves fresh GL low residues uniform conditional on every ancestor choice. Otherwise the selected bit bad-branch surcharge is not justified by its per-edge density bound. This is a scoped inherited-interface proof, not a new exponent.", + "budget_minutes": 60, + "stop_rule": "Accept only a written all-depth counting proof with an explicit source-to-hypothesis map and exact semantic negative controls. Stop any numerical frontier or stock-coefficient claim. If the finite selected artifacts do not prove a prefix contract, identify that remaining compiler obligation rather than infer it from endpoint restoration.", + "outcome": "completed", + "result_scope": "Conditional all-depth address/counting implication proved, with source binding and two exact single-hypothesis counterexamples. No selected all-size compiler admission or new kappa.", + "evidence": "README gives the proof and source-to-hypothesis map. Final exact smoke passed: 60 address cases, 150 cuts, 2370 conditional fibers, 14120 padded rows, four GL2 prime-power rings, three adaptive-minor witnesses and nine rejected controls. RESULT.json stores the canonical receipt.", + "author": "Adam Gall", + "ai_assistance": "Substantial OpenAI Codex assistance in source investigation, proof, implementation and writing; not independent human review.", + "open_questions": [ + { + "question": "Can the selected all-size compiler expose a machine-checkable ancestor/current/future field dependency certificate for each invocation?", + "why_it_matters": "The finite scalar/controller records and stock counts do not by themselves certify prefix measurability at every width.", + "first_step": "Annotate the inherited child-weight rule and right-multiplication route with field read/write sets, then reject a read of an unused descendant field.", + "blocked_by": "The current selected package retains the all-size compiler as an explicit hypothesis rather than emitting this address-level certificate." + }, + { + "question": "What paid bad-class charge remains for a controller that deliberately selects an edge from its current low residue?", + "why_it_matters": "The fixed-edge fraction cannot be reused after adaptive selection, even with restored rows.", + "first_step": "Specify a finite low-class partition and sum the chosen bad indicators fiberwise with every selector and fallback cost.", + "blocked_by": "No favorable fully paid adaptive selector is constructed here." + } + ], + "seed": "cc5bf62436a3476502c7769e29c2990c", + "track": "adversarial-audit", + "domain": "All integer cover sizes W>=2, finite recursion depth D>=1, row range Q>=W^D, and arbitrary complete spectators; selected instantiation W(w)=28425*|GL_64(Z/q^w Z)| for eligible q>2^80.", + "changed_premise": "Audit execution-domain and selector independence rather than derive another reserve coefficient.", + "method": "Exact integer mixed-radix bijections, induction on invocation depth, GL low-residue equal-fiber counting, rational surcharge identities, finite exhaustive semantic controls.", + "optimistic_complete_bill": "No supplier saving is proposed. Preserve the complete selected good profile plus (1/10^16)*(32*64^2)*sum(H)/28416*(1/64)^(1-a); pay one outer padded-volume factor P/Q<2. No per-level padding factor or free removal of bad children.", + "source_binding": "SOURCES.json pins selected record, assembly, PR589 expected record, frozen PR1087 assembler and inherited row/weighted-child proof texts; code is inspected/authenticated, not imported.", + "upstream_checkpoint": { + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "checked_at": "2026-10-14T19:09:18.457404+00:00", + "decision": "Retain scientific base 564148b82ae9df72163f22106f15e73efca8aff2: refreshed guidance only; selected record, catalogue and mathematical inputs unchanged." + }, + "overlap": { + "open_prs_fetched_at": "2026-10-14T19:00:33.696741+00:00", + "discussion_records_fetched_at": "2026-10-14T19:02:09.707625+00:00", + "coverage": "353 open PRs including drafts, 738 discussion/comment/reply records, complete pagination; 1538 local records including this package. Targeted cached search refreshed 2026-10-14T19:09:29.969298+00:00; offline warnings retained, code diffs and arbitrary nested files not searched. Live PR1990 disposition read: merged at reviewed head c3bd90d9a8d9202c063700ae443e83825780e056. Absence is not novelty evidence.", + "predecessor_boundary": "PR1956/1965/1990 address cutoff constants and stock-fit envelopes; r480-sharp-charge535 sharpens a previously proved per-edge numerical charge. Neither is treated as a proof of the selected all-size field dependency graph." + } +} diff --git a/research/selected-cover-fresh-fibers/VERIFY.json b/research/selected-cover-fresh-fibers/VERIFY.json new file mode 100644 index 0000000000..517a58095b --- /dev/null +++ b/research/selected-cover-fresh-fibers/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "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/tune/EXPECTED.json", + "research/five-stage-source527-banks/proof/three-stage-cover-bit.tex", + "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex", + "research/r480-sharp-charge535/README.md", + "research/selected-bootstrap-stock-audit/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated selected source binding; exact mixed-radix and conditional-fiber audit; GL prime-power equal fibers and right routing; adaptive-minor and genuine-prefix counterexamples; nine semantic/source controls; canonical result comparison with assertions disabled." + } + ] +} diff --git a/research/selected-cover-fresh-fibers/verify.py b/research/selected-cover-fresh-fibers/verify.py new file mode 100755 index 0000000000..dc13d62614 --- /dev/null +++ b/research/selected-cover-fresh-fibers/verify.py @@ -0,0 +1,370 @@ +#!/usr/bin/env python3 +"""Source-bound fresh-fiber audit. Standard library; no predecessor execution. + +Prepared for Adam Gall with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import ast +from collections import Counter, defaultdict +from copy import deepcopy +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path +import tarfile + +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_PINS = "research/complex-t16-rare-pattern-exchanges/SOURCE.json" +SELECTED = "certificates/selected-result.json" + + +class Reject(ValueError): + pass + + +def require(condition, message): + if not condition: + raise Reject(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def git_blob(data): + return hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def reject_control(name, function): + try: + function() + except Reject: + return name + raise Reject("negative control accepted: " + name) + + +def check_digest(data, expected): + require(digest(data) == expected, "source digest mismatch") + + +def authenticate(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = {} + pins = {} + for entry in manifest["files"]: + if entry["usage"] == "input": + data = (ROOT / entry["path"]).read_bytes() + check_digest(data, entry["sha256"]) + require(git_blob(data) == entry["git_blob"], "source Git blob mismatch") + inputs[entry["path"]] = data + pins[entry["path"]] = entry["sha256"] + require({BIT, ASSEMBLY, ARCHIVE, ARCHIVE_PINS, SELECTED} <= inputs.keys(), + "missing selected source") + # Authenticate the container before opening, and the member before parsing. + with tarfile.open(ROOT / ARCHIVE, "r:gz") as archive: + member = archive.extractfile("code/assemble.py") + require(member is not None, "missing archived assembler") + assembler = member.read() + archive_pins = json.loads(inputs[ARCHIVE_PINS]) + check_digest(assembler, archive_pins["files"]["code/assemble.py"]) + constants = {} + for node in ast.parse(assembler).body: + if isinstance(node, ast.Assign) and len(node.targets) == 1: + target = node.targets[0] + if isinstance(target, ast.Name) and target.id == "BIT_BLOB": + constants["blob"] = ast.literal_eval(node.value) + if isinstance(target, ast.Tuple): + names = [item.id for item in target.elts if isinstance(item, ast.Name)] + if names == ["BIT_L", "BIT_T"]: + constants["stages"], constants["replicas"] = ast.literal_eval(node.value) + require(constants == {"blob": git_blob(inputs[BIT]), "stages": 9, "replicas": 32}, + "selected assembler bit binding") + selected = json.loads(inputs[SELECTED]) + require(selected["certificate"] == ASSEMBLY, "selected assembly path") + check_digest(inputs[ASSEMBLY], selected["certificate_sha256"]) + assembly = json.loads(inputs[ASSEMBLY]) + require(assembly["bit_supplier"]["git_blob_sha1"] == constants["blob"], + "assembly bit blob") + check_digest(inputs[BIT], assembly["input_sha256"]["package:inputs/PR589-EXPECTED.json"]) + pins[ARCHIVE + ":code/assemble.py"] = digest(assembler) + return json.loads(inputs[BIT]), assembly, pins + + +def selected_facts(bit, assembly): + word, nine = bit["word"], bit["nine"] + profile = {int(rank): count for rank, count in nine["profile"].items()} + require(all(type(count) is int and count > 0 for count in profile.values()), "profile count") + require(set(profile) == {1, 2, 3, 4, 5, 6, 7, 42}, "selected profile ranks") + m, stages, replicas = 64, 9, 32 + pairs = (stages - 1) // 2 + live = 2 * pairs * word["v"] * replicas + mass = sum(rank * count for rank, count in profile.items()) + deficit = replicas * (2 * pairs * word["v"] - stages * word["decoder_constant"]) + require(live == nine["bit"]["live"] == 28416, "selected live stock") + require(nine["bit"]["physical"] == live + 9 == 28425, "selected physical stock") + require(mass == nine["bit"]["rank_mass"] == m * live - deficit, "selected rank mass") + require(deficit == assembly["bit_supplier"]["derived_deficit"], "selected deficit") + require(max(profile) == nine["bit"]["maxchild"] == 42, "selected maximum child") + require(m * m > 2 * max(profile) ** 2, "selected halving guard") + require(len(assembly["bootstrap"]) == len(assembly["conservative_bootstrap"]) == 7, + "selected bootstrap stages") + edges = sum(profile.values()) + fallback = 32 * m * m + # This is the existing complete charge, not a new endpoint calculation. + coefficient = Fraction(fallback * edges, 10**16 * live) + zero_moment = Fraction(mass, m * live) + coefficient / m + require(zero_moment < 1, "orientation: unchanged bill at exponent zero") + return { + "m": m, "live_roles": live, "physical_roles": nine["bit"]["physical"], + "profile": {str(rank): count for rank, count in sorted(profile.items())}, + "edges": edges, "rank_mass": mass, "deficit": deficit, + "max_child": max(profile), "fallback_per_bad_edge": fallback, + "bad_fraction_retained": "1/10000000000000000", + "fallback_coefficient_before_rank_power": str(coefficient), + "complete_moment_at_a_zero": str(zero_moment), + "scope": "Existing selected bill only; no new moment root or stock coefficient.", + } + + +def split_row(index, width, depth): + digits = [] + for _ in range(depth): + index, digit = divmod(index, width) + digits.append(digit) + return (index, *reversed(digits)) + + +def join_row(row, width): + value = row[0] + for digit in row[1:]: + value = value * width + digit + return value + + +def route(row, width, level, direction=1): + # Current permutation depends on ancestors only; future stock is untouched. + ancestor = row[: level + 1] + shift = 1 + sum((i + 1) * value for i, value in enumerate(ancestor)) + changed = (row[level + 1] + direction * shift) % width + return row[: level + 1] + (changed,) + row[level + 2 :] + + +def check_route(rows, width, level, transform): + laws = {} + images = defaultdict(set) + for row in rows: + new = transform(row) + require(len(new) == len(row), "route arity") + require(new[: level + 1] == row[: level + 1], "route changed ancestor") + require(new[level + 2 :] == row[level + 2 :], "route changed future stock") + require(0 <= new[level + 1] < width, "route outside current field") + key = row[: level + 2] + if key in laws: + require(laws[key] == new[level + 1], "route reads future stock") + laws[key] = new[level + 1] + images[row[: level + 1]].add(new[level + 1]) + require(all(len(image) == width for image in images.values()), "nonbijective current route") + + +def check_complete_fibers(rows, width, depth, level): + require(len(rows) == len(set(rows)), "duplicate address") + fibers = defaultdict(Counter) + for row in rows: + require(len(row) == depth + 1, "row arity") + require(all(0 <= x < width for x in row[1:]), "row digit") + fibers[row[: level + 1]][row[level + 1]] += 1 + wanted = Counter({digit: width ** (depth - level - 1) for digit in range(width)}) + require(all(fiber == wanted for fiber in fibers.values()), "incomplete current/future fiber") + return len(fibers) + + +def address_cases(): + cases = cuts = fibers = rows_checked = 0 + for width in range(2, 7): + for depth in range(1, 5): + stock = width**depth + for genuine in (stock, stock + 1, 2 * stock - 1): + padded = ((genuine + stock - 1) // stock) * stock + require(genuine <= padded < 2 * genuine, "one-padding volume") + rows = [split_row(index, width, depth) for index in range(padded)] + require(all(join_row(row, width) == i for i, row in enumerate(rows)), "radix round trip") + # Separate Cartesian oracle, not another repeated-divmod implementation. + cartesian = list(product(range(padded // stock), *([range(width)] * depth))) + require(rows == cartesian, "Euclidean/Cartesian disagreement") + for level in range(depth): + check_route(rows, width, level, lambda row: route(row, width, level)) + moved = [route(row, width, level) for row in rows] + # Prefix-dependent stopping and child selection are allowed. + active = [row for row in moved if level == 0 or sum(row[: level + 1]) % 3 != 0] + fibers += check_complete_fibers(active, width, depth, level) + cuts += 1 + for row in rows: + moved = row + for level in range(depth): + moved = route(moved, width, level) + for level in reversed(range(depth)): + moved = route(moved, width, level, -1) + require(moved == row, "completed route restoration") + rows_checked += len(rows) + cases += 1 + return {"cases": cases, "cuts": cuts, "conditional_fibers": fibers, + "padded_rows": rows_checked, "widths": [2, 6], "depths": [1, 4]} + + +def det2(matrix): + a, b, c, d = matrix + return a * d - b * c + + +def gl2_low_fibers(): + records = [] + for prime, power in ((3, 1), (3, 2), (5, 1), (5, 2)): + modulus = prime**power + fibers = Counter() + route_images = set() + count = 0 + for matrix in product(range(modulus), repeat=4): + if det2(matrix) % prime == 0: + continue + a, b, c, d = matrix + fibers[tuple(x % prime for x in matrix)] += 1 + # Right multiply by [[1,1],[0,1]], a genuine GL route. + routed = (a, (a + b) % modulus, c, (c + d) % modulus) + require(det2(routed) % prime != 0, "right route left GL") + route_images.add(routed) + count += 1 + low_count = (prime**2 - 1) * (prime**2 - prime) + lifts = prime ** (4 * (power - 1)) + require(len(fibers) == low_count, "GL low class count") + require(set(fibers.values()) == {lifts}, "GL low fibers unequal") + require(count == low_count * lifts == len(route_images), "GL right route not bijective") + records.append({"prime": prime, "power": power, "low_classes": low_count, + "lifts_per_low_class": lifts, "matrices": count}) + return records + + +def projective_predicate_cases(): + records = [] + for prime in (3, 5, 7): + lines = [(1, slope) for slope in range(prime)] + [(0, 1)] + fixed_bad = Counter({line: 0 for line in lines}) + selected_bad = total = 0 + for matrix in product(range(prime), repeat=4): + if det2(matrix) % prime == 0: + continue + a, b = matrix[:2] + kernels = [v for v in lines if (a * v[0] + b * v[1]) % prime == 0] + require(len(kernels) == 1, "projective kernel is not unique") + chosen = kernels[0] + selected_bad += int((a * chosen[0] + b * chosen[1]) % prime == 0) + for v in lines: + fixed_bad[v] += int((a * v[0] + b * v[1]) % prime == 0) + total += 1 + require(set(fixed_bad.values()) == {total // (prime + 1)}, "fixed-edge density") + require(selected_bad == total, "adaptive witness not always bad") + # All edge indicators summed at fixed cost still obey linearity exactly. + require(sum(fixed_bad.values()) == total, "fixed-edge sum") + records.append({"prime": prime, "matrices": total, "edges": prime + 1, + "fixed_bad_fraction": str(Fraction(1, prime + 1)), + "adaptive_bad_fraction": "1", "row_map": "identity"}) + return records + + +def semantic_controls(bit, assembly, predicates): + controls = [] + rows = list(product(range(2), range(3), range(3))) + controls.append(reject_control("current_route_reads_future", lambda: check_route( + rows, 3, 0, lambda row: (row[0], (row[1] + row[2]) % 3, row[2])))) + controls.append(reject_control("nonbijective_current_route", lambda: check_route( + rows, 3, 0, lambda row: (row[0], 0, row[2])))) + equal_rows = list(product(range(3), repeat=3)) + controls.append(reject_control("ancestor_future_alias", lambda: check_route( + equal_rows, 3, 0, lambda row: (row[2], row[1], row[0])))) + genuine = [split_row(index, 3, 2) for index in range(10)] + controls.append(reject_control("pruned_padded_domain", lambda: check_complete_fibers( + genuine, 3, 2, 1))) + cell = [row for row in genuine if row[:2] == (1, 0)] + require(cell == [(1, 0, 0)], "genuine-prefix witness") + all_padded = [split_row(index, 3, 2) for index in range(18)] + check_complete_fibers(all_padded, 3, 2, 1) + selected_bad = Fraction(predicates[0]["adaptive_bad_fraction"]) + fixed_bound = Fraction(predicates[0]["fixed_bad_fraction"]) + controls.append(reject_control("adaptive_edge_at_fixed_edge_charge", lambda: require( + selected_bad <= fixed_bound, "adaptive edge violates its claimed density"))) + # Restoration alone does not reject this selector: both maps really are identity. + require(all(tuple(row) == row for row in rows), "identity row-map control") + tampered = deepcopy(bit) + tampered["nine"]["profile"]["42"] -= 1 + controls.append(reject_control("omitted_selected_edge", lambda: selected_facts(tampered, assembly))) + tampered = deepcopy(bit) + tampered["nine"]["bit"]["physical"] -= 1 + controls.append(reject_control("live_stock_substituted_for_physical", lambda: selected_facts(tampered, assembly))) + source_bytes = (ROOT / BIT).read_bytes() + controls.append(reject_control("source_byte_corruption", lambda: check_digest( + source_bytes + b" ", digest(source_bytes)))) + # The complete padded domain is sufficient; restoration is a distinct condition. + controls.append(reject_control("unrestored_row_at_unpadding", lambda: require( + {join_row(route(row, 3, 0), 3) for row in genuine} == set(range(10)), + "genuine prefix not invariant at unfinished route"))) + return controls + + +def build_result(): + bit, assembly, source_pins = authenticate() + facts = selected_facts(bit, assembly) + predicates = projective_predicate_cases() + return { + "status": "PASS_SELECTED_COVER_FRESH_FIBERS", + "selected": facts, + "address_audit": address_cases(), + "gl2_low_fibers": gl2_low_fibers(), + "adaptive_minor_counterexamples": predicates, + "genuine_prefix_counterexample": { + "W": 3, "D": 2, "stock": 9, "genuine": 10, "padded": 18, + "ancestor": [1, 0], "genuine_fresh_values": [0], + "padded_bad_fraction": "1/3", "genuine_bad_fraction": "1", + }, + "negative_controls_rejected": semantic_controls(bit, assembly, predicates), + "source_sha256": source_pins, + "limits": [ + "All-depth theorem uses the written prefix/complete-domain hypotheses.", + "Selected all-size field dependency graph remains an inherited compiler obligation.", + "No stock coefficient, improved root, new supplier or multiplication theorem.", + "Finite matrices are GL2 controls, not enumeration of selected GL64.", + ], + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path, help="create a new external receipt") + args = parser.parse_args() + result = build_result() + if args.write_result is not None: + destination = args.write_result.resolve() + require(not destination.is_relative_to(PACKAGE), "regenerate to an external path") + with destination.open("x", encoding="utf-8") as output: + output.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(canonical(expected) == canonical(result), "saved result differs from reconstruction") + print(result["status"], "cases=" + str(result["address_audit"]["cases"]), + "cuts=" + str(result["address_audit"]["cuts"]), + "GL_rings=" + str(len(result["gl2_low_fibers"])), + "controls=" + str(len(result["negative_controls_rejected"]))) + + +if __name__ == "__main__": + try: + main() + except (Reject, OSError, KeyError, ValueError, tarfile.TarError) as error: + raise SystemExit("REJECT_SELECTED_COVER_FRESH_FIBERS: " + str(error)) from error From 1d3ee0926656d5260c6cb1c0b81964ffe9fe1377 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 15:13:25 -0400 Subject: [PATCH 2/2] Clarify prime eligibility and remove redundant identity check --- research/selected-cover-fresh-fibers/README.md | 8 ++++++-- research/selected-cover-fresh-fibers/verify.py | 2 -- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/research/selected-cover-fresh-fibers/README.md b/research/selected-cover-fresh-fibers/README.md index e9a7eaaff1..8d9e84dc7c 100644 --- a/research/selected-cover-fresh-fibers/README.md +++ b/research/selected-cover-fresh-fibers/README.md @@ -128,8 +128,12 @@ whole group and on low classes, so it preserves this equal-fiber statement. The role factor `28425` is independent and cancels. These statements hold for **every eligible prime q and every w>=1**, not just the small test rings. -Fix any invocation's ancestor prefix and any one of its edge occurrences. -The source's bad-minor set has fraction at most `b=2*64^3/q < 10^-16`. +Fix an odd prime `q>2^80` before choosing input widths, avoiding the fixed +rational denominators and rank witnesses of the selected geometry, as required +by the inherited cover contract. This is what **eligible** means here; the +finite profile alone does not certify that prime-selection contract. Fix any +invocation's ancestor prefix and any one of its edge occurrences. The source's +bad-minor set then has fraction at most `b=2*64^3/q < 10^-16`. By the theorem, this remains its frequency at the invocation. Sum costs over edge occurrences and then ancestor prefixes. Linearity of a finite sum, not independence of bad events, gives the surcharge. There is no need to bound the diff --git a/research/selected-cover-fresh-fibers/verify.py b/research/selected-cover-fresh-fibers/verify.py index dc13d62614..33a249823b 100755 --- a/research/selected-cover-fresh-fibers/verify.py +++ b/research/selected-cover-fresh-fibers/verify.py @@ -300,8 +300,6 @@ def semantic_controls(bit, assembly, predicates): fixed_bound = Fraction(predicates[0]["fixed_bad_fraction"]) controls.append(reject_control("adaptive_edge_at_fixed_edge_charge", lambda: require( selected_bad <= fixed_bound, "adaptive edge violates its claimed density"))) - # Restoration alone does not reject this selector: both maps really are identity. - require(all(tuple(row) == row for row in rows), "identity row-map control") tampered = deepcopy(bit) tampered["nine"]["profile"]["42"] -= 1 controls.append(reject_control("omitted_selected_edge", lambda: selected_facts(tampered, assembly)))