diff --git a/research/selected-bit-ceiling-free-stock/README.md b/research/selected-bit-ceiling-free-stock/README.md new file mode 100644 index 0000000000..fce1792420 --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/README.md @@ -0,0 +1,146 @@ +# A ceiling-free parent-stock bound for the selected BIT producer + +Under the same packet and completed-leaf hypotheses as [PR2084](https://github.com/CrocSwap/integer-mult-bounds/pull/2084), the selected ordinary BIT producer admits + +``` +log_q S(n,w) <= 6748*w*log2(max(1,n)) + <= 6748*w*(1+log2 e), 0 <= n <= e, e,w integers >= 1. +``` + +This reduces PR2084's sufficient parent-stock coefficient from 8194 to 6748, a ratio of exactly 14/17. It also reduces `ceil(log2(8*sigma))` from 17 to 16. The existing native first-stage cutoff passes the sufficient fit guard with this coefficient. + +This is a conditional stock-bound refinement and independent audit, not a new supplier, changed cutoff, physical reserve implementation or new kappa. The production row coefficient remains 18,355. No selected record or predecessor evidence changes. + +## Scope and overlap + +Scientific base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. The one-time selection is retained in [SELECTION.json](SELECTION.json). The assigned card is `selected-stock-envelope`, refined to the native first-stage ordinary BIT producer and a tighter depth implication. + +The nearest predecessor is Adam Gall's PR2084, read at head `8001a23b003bec5dff5e61edec907b652c475932`. Its packet/restoration proof and coefficient 8194 are credited, not claimed as new. Sricharan Vagvala's concurrent [PR2105](https://github.com/CrocSwap/integer-mult-bounds/pull/2105), head `0aca64e29d43533743bb912ac8b77b434e04b84a`, audits floor-depth thresholds for the **different complex m=73/rank-48 producer**. Its exact-depth method informed the independent inverse-threshold cross-check here. No predecessor verifier is imported or executed, and no pending package is copied into this one. + +The new implication uses the BIT terminal threshold to remove a rounded-depth additive term before bounding stock. It does not reproduce the fourteen known headrooms or solve the retained implementation hypotheses. The ordinary producer is BIT `m=64`, not the complex `m=73` supplier that constrains the shared exponent. + +Coordination: [Discussion 2114](https://github.com/CrocSwap/integer-mult-bounds/discussions/2114). The entry refresh covered 376 open PRs and 769 discussion records with complete pagination and no warnings. Metadata searches do not cover every diff or unpublished result. + +## Source binding + +The selected record binds `research/community-frontier1094-audit/ASSEMBLY.json`. Its BIT citation binds the exact tuned PR589 receipt by Git blob. The retained PR1087 assembler is authenticated as an immutable archive, then its `code/assemble.py` member is authenticated separately and read without execution. Its `BIT_L,BIT_T=9,32` and `BIT_M=1+7*BIT_L` identify dimension 64. + +The cited receipt has maximum child rank 42, 28,416 live roles and 28,425 physical roles. All nine work roles remain in the packet. Its row bill is `2*(64^2+1)+9909+252=18355`; this package changes none of those charged production terms. + +The source `three-stage-cover-bit.tex` supplies the local-ring full-cover formula and floor-child contract in sections "Finite covers, batching, and the strict moment" and "One weighted child on a generic residue class". Its displayed dimension 67 is historical. Instantiating that contract on the selected BIT recipe remains an explicit realization assumption. The reviewed PR185 proof retained by PR387 supplies the internally completed ordinary-leaf interface in "Nested row restoration and fixed tapes". Source hashes, Git blobs and the archive-member hash are in [SOURCES.json](SOURCES.json). + +## Conditional all-width lemma + +Retain these hypotheses. + +- Fix an eligible odd prime `q>2^80`, avoiding the recipe's fixed denominator and rank exclusions, before choosing widths. +- The selected full-cover implementation exposes one complete packet per active coarse level, with divisor + `W_q(w)=28425*|GL_64(F_q)|*q^(4096*(w-1))`. +- Atom width `w` stays fixed along a coarse call. Every child has atom count at most `r*floor(n/64)`, with `r<=42`. Bad-class fallback children have the stronger bound `floor(n/64)`. Below 64 atoms, and for peeled remainders and other ordinary operations, use completed ordinary calls. +- A child uses only its unused row quotient, fixes exposed ancestor fields as complete spectators and restores its supplied row before sequential reuse. The complete node restores its exposed role field. Completed ordinary leaves borrow internally and need no additional external row factor. + +These are inherited interfaces, not conclusions of the finite checks below. + +### Depth without a ceiling + +Let `D(n)` be the maximum-rank depth envelope: zero for `n<64`, and otherwise + +``` +D(n) = 1 + D(42*floor(n/64)). +``` + +Monotonicity makes this an upper bound for every permitted child path, including fallback. It is not a claim that every such path is realized by the physical compiler. + +Set `rho=42/64`. The exact integer certificate + +``` +2^17 * 42^28 < 64^28 +``` + +proves `rho < 2^(-17/28)`. If a path has `d>=1` active nodes, its last active atom count is at least 64 and at most `rho^(d-1)*n`. Thus + +``` +log2 n >= 6 + (d-1)*log2(64/42) + >= 6 + (d-1)*17/28 + >= d*17/28. +``` + +The last step uses the terminal slack `6>=17/28`. Consequently, for every integer `n>=0`, + +``` +D(n) <= (28/17)*log2(max(1,n)). +``` + +This has no ceiling or unnamed additive constant. Removing the terminal threshold invalidates this proof step. Replacing the floor by a ceiling can even prevent termination, since `42*ceil(84/64)=84`. Neither countermodel describes a defect in the selected floor contract. The allowance 28/17 is not claimed optimal. + +### Divisible stock and its complete packet charge + +Reduction modulo q gives exactly `q^(4096*(w-1))` lifts of each invertible low matrix. Therefore + +``` +|GL_64(Z/q^w Z)| < q^(4096*w), +log_q W_q(w) < 4096*w+1 <= 4097*w, +``` + +since `28425= 3, +L*delta^2 >= 36, +L*delta >= 2*(4+16). +``` + +The sufficient fit lemma of Josie Elliston's PR1965 then gives `ceil(log_q S(e,w))=2^L`, with `w=ceil(e^s)`, subject to the retained interfaces. This comparison does not assert that an actual selected implementation meets them, nor that this cutoff is necessary. The known headroom arithmetic is not claimed as new. + +## Replay and controls + +Standard-library Python 3.12, from the repository root: + +``` +python3.12 -I -B research/selected-bit-ceiling-free-stock/verify.py +python3.12 -I -O -B research/selected-bit-ceiling-free-stock/test_verify.py +python3.12 scripts/research_package.py --package research/selected-bit-ceiling-free-stock +``` + +Expected output includes `PASS_SELECTED_BIT_CEILING_FREE_STOCK sigma=6748 predecessor=8194 ratio=14/17 widths=100001 ell=16 no_new_kappa`, ten passing test groups and `PASS_REGISTERED_RESEARCH_PACKAGE`. + +The verifier checks every external byte pin before semantic use, authenticates the archive member, and requires the committed [RESULT.json](RESULT.json). It neither regenerates a missing result nor changes a mismatched one. The exact checks cover every width 0..100,000 using separate forward and all-child dynamic programs, 196 inverse-threshold boundary probes, and 15 power-boundary probes up to 4097-bit atom counts. Literal depth fixtures constrain their shared conventions. + +Tests reject a false contraction, rank-43 substitution, missing terminal slack, capacity excess, wrong producer, omitted largest child, corrupted/nonregular archive member, insufficient cutoff and wrong coefficient. Optimized public-CLI controls mutate every declared live input in isolated copies and test corrupted and missing required results. No frozen file is modified. Python assertions are not acceptance gates. The universal implication rests on the written argument, not the finite fixtures. + +## Verification limits and implementation bounds + +No full selected cold replay, native compiler execution, Lean proof, hosted CI pass or independent human review is claimed. Only the native first-stage comparison is checked. Other stages need their preceding completed ordinary contract. The selected exponent and production row charge are unchanged. + +The new checker has no recursion. The width sweep is bounded at 100,001, rank inventories at 64, source lists at 16, archive scanning at 1024 members, consumed member size at 65,536 bytes and forward paths at 8194 edges. Source files are capped at 8 MiB and authenticated before archive decoding. The selected two-level halving guard bounds paths for the admitted 4097-bit atom counts. + +Power-of-Ten deviations are confined to Python's managed allocation and standard testing machinery. Rules 3 and 9 cannot provide allocation-free arithmetic or static unittest dispatch in this runtime. The fixed input/sweep/bit capacities bound live collections and integer sizes; test subprocesses have 120-second timeouts and temporary copies have scoped cleanup. The single `runpy` target is this package's own fixed verifier path. Follow-up is to reassess these capacities if the sweep or width domain expands, not to generalize this checker into an unbounded search. Syntax compilation, warnings-as-errors and normal/optimized replays are the available diagnostics; no repository-wide analyzer configuration changes are made. + +## Open next questions + +1. Can the selected GL64 packet and completed-row interfaces be realized with a source-bound all-size field-dependency certificate? Begin with one emitted parent/child split and verify that routes fix ancestor spectators and unused descendant stock. Finite scalar and depth checks do not discharge this implementation obligation. PR2097's fresh-fiber theorem is complementary. +2. Can an actual selected ordinary leaf be bound to the internally completed, zero-extra-external-stock interface at every admitted width? Trace its borrowing and restored endpoints while retaining complete outer spectators. The reviewed contract is inherited here; its physical realization, uniform time coefficients and tape obligations still block unconditional adoption. + +## Credit + +Adam Gall supplied PR2084's conditional BIT packet/stock implication. Sricharan Vagvala supplied the concurrent PR2105 complex depth audit. Josie Elliston supplied PR1956/PR1965's cutoff audit and time/space separation; ToikY supplied PR1990's independent stock-fit audit. DreamingOfClouds supplied the selected PR589 BIT word on eumemic's base and its credited compiler/hosting lineage. Rohan Arun supplied the reviewed PR185/PR387 contracts and selected PR1094 assembly on Jeremy Kothe's PR1087 predecessor. Their constructions, interface arguments and existing numerical receipts are not claimed as new. + +Nick Petalas retains authorship and responsibility for this conditional refinement and checker. Apache-2.0, following the repository license. No predecessor files are vendored or modified. diff --git a/research/selected-bit-ceiling-free-stock/RESULT.json b/research/selected-bit-ceiling-free-stock/RESULT.json new file mode 100644 index 0000000000..39624ef43b --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/RESULT.json @@ -0,0 +1,99 @@ +{ + "status": "PASS_SELECTED_BIT_CEILING_FREE_STOCK", + "m": 64, + "maxchild": 42, + "physical_roles": 28425, + "depth_allowance": "28/17", + "sigma": 6748, + "predecessor_sigma": 8194, + "coefficient_ratio": "14/17", + "finite_checks": { + "all_child_widths": 100001, + "threshold_probes": 196, + "large_widths": [ + [ + 7, + -1, + 1 + ], + [ + 7, + 0, + 2 + ], + [ + 7, + 1, + 2 + ], + [ + 64, + -1, + 94 + ], + [ + 64, + 0, + 94 + ], + [ + 64, + 1, + 94 + ], + [ + 256, + -1, + 410 + ], + [ + 256, + 0, + 410 + ], + [ + 256, + 1, + 410 + ], + [ + 1024, + -1, + 1674 + ], + [ + 1024, + 0, + 1674 + ], + [ + 1024, + 1, + 1674 + ], + [ + 4096, + -1, + 6729 + ], + [ + 4096, + 0, + 6729 + ], + [ + 4096, + 1, + 6729 + ] + ] + }, + "first_cutoff": { + "branch": "native", + "stage": 1, + "cutoff_log2": 4785575287428, + "ell": 16, + "gap": "4388379286997125724770519885577770614671108008794190196708787314167220683197382073600889/1600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + }, + "scope": "Conditional packet/completed-leaf envelope only; no new kappa or supplier admission." +} diff --git a/research/selected-bit-ceiling-free-stock/SELECTION.json b/research/selected-bit-ceiling-free-stock/SELECTION.json new file mode 100644 index 0000000000..70ea613b5a --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/SELECTION.json @@ -0,0 +1,132 @@ +{ + "seed": "54d4d17f6d56842e50afacbc598bd1d2", + "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": "ce7411fb7cf6f3460bfc", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "method": "Find an exact counterexample at the claimed interface boundary.", + "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": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/selected-bit-ceiling-free-stock/SOURCES.json b/research/selected-bit-ceiling-free-stock/SOURCES.json new file mode 100644 index 0000000000..e5f12c4087 --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/SOURCES.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "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/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/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "usage": "input", + "git_blob": "2970ef79b0441e937449bed30f68f2e0558186ba", + "sha256": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86" + }, + { + "path": "research/bootstrap-cutoff-time-space-split/README.md", + "usage": "input", + "git_blob": "59986cb4b0a912ab18883a4f41dedae0fda1a5ae", + "sha256": "e7f215a11a81c02b657bac9ebb904f346d1ae95446f32fda74a4084360c79a86" + }, + { + "path": "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex", + "usage": "input", + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8" + } + ], + "archive_members": [ + { + "path": "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "member": "code/assemble.py", + "sha256": "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a" + } + ] +} diff --git a/research/selected-bit-ceiling-free-stock/TASK.json b/research/selected-bit-ceiling-free-stock/TASK.json new file mode 100644 index 0000000000..6976e16d34 --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently refine PR2084's conditional native first-stage BIT parent-stock bound by proving a ceiling-free rank-42/m64 depth allowance and a sufficient coefficient 6748 rather than 8194.", + "scope_change_reason": "Fresh overlap already contains conditional divisor and depth work. This uses the actual ordinary BIT producer, not the distinct complex m73 supplier, and audits one all-width depth/stock implication instead of repeating the fourteen headrooms or claiming physical realization.", + "bottleneck_link": "A smaller source-bound conditional parent reserve strengthens one inherited implementation obligation; it changes neither the paid supplier profile nor the selected exponent. The packet and completed-leaf implementation assumptions remain open.", + "budget_minutes": 60, + "stop_rule": "One proof and exact checker. Stop if the uniform depth implication or selected binding fails; do not change the hypotheses or selected frontier to force acceptance.", + "outcome": "completed", + "evidence": "README.md supplies the all-width proof; RESULT.json records 100001 all-child/forward cases, 196 threshold probes, 15 large-width probes and the first native stock-fit comparison. test_verify.py supplies ten behavioral and rejection groups.", + "author": "Nick Petalas", + "ai_assistance": "Substantial assistance in proof checking and test implementation. Authorship and responsibility remain with Nick Petalas.", + "upstream_checkpoint": { + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "checked_at_utc": "2026-10-14T19:46:18Z", + "priority_revision": 4 + }, + "predecessors": [ + { + "pr": 2084, + "head": "8001a23b003bec5dff5e61edec907b652c475932", + "credit": "Adam Gall's conditional selected BIT packet, depth/restoration and coefficient-8194 argument. Read, not imported or executed." + }, + { + "pr": 2105, + "head": "0aca64e29d43533743bb912ac8b77b434e04b84a", + "credit": "Sricharan Vagvala's separate complex m73/rank48 depth audit informed the inverse-threshold cross-check. No code imported or executed." + } + ], + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2114", + "scope_key": "f5c32b23bcd01d2e356d:BIT64-r42-ceiling-free-native-stage1", + "method": "Exact integer contraction and terminal-slack proof, with source-bound packet charging and code-disjoint forward/all-child/inverse-threshold cross-checks.", + "domain": "All integers e,w>=1 and 0<=n<=e under the retained eligible-prime, selected packet, floor-child and completed-leaf interfaces. Finite controls cover n=0..100000, 196 threshold probes and 15 power probes up to 4097 bits.", + "optimistic_cost_budget": "No paid supplier/profile or row-invoice change. The whole unchanged packet and completed-leaf contracts stay charged. Only the conditional parent-stock upper bound is refined.", + "verification": { + "environment": "CPython 3.12.15, standard library only, Linux x86_64 WSL2 6.6.87.2-microsoft-standard-WSL2", + "registered_command": "/home/nick/.local/bin/python3.12 -B scripts/research_package.py --package research/selected-bit-ceiling-free-stock", + "registered_result": "PASS_REGISTERED_RESEARCH_PACKAGE; normal/optimized warnings-as-errors verifier and ten test groups pass", + "workflow_command": "/home/nick/.local/bin/python3.12 -Werror -B -m unittest discover -s tests -p 'test_research_*.py'", + "workflow_result": "65 tests pass", + "selected_integrity_command": "make selected-record-check", + "selected_integrity_result": "PASS selected record, exact kappa, original source inventory and proof supplement", + "diagnostics": "Syntax compilation and AST function-length check pass; longest function is 33 lines. No ruff or mypy executable is installed.", + "linux_peak_resident_kib": 32480, + "unrun": "No full selected cold replay, native compiler, formal kernel, hosted CI or independent human review." + }, + "final_overlap": { + "open_prs": 380, + "discussion_records": 779, + "complete_pagination": true, + "checked_at_utc": "2026-10-14T19:48:50Z", + "warnings": [], + "related_heads": "PR2084 and PR2105 heads unchanged at submission checkpoint", + "limitations": "Metadata search is not a novelty certificate. Direct matches for the refined bound were this package and its claim." + }, + "entry_overlap": { + "open_prs": 376, + "discussion_records": 769, + "complete_pagination": true, + "checked_at_utc": "2026-10-14T19:36:24Z", + "limitations": "Text metadata only, not every diff or unpublished result; no absence-based novelty claim." + }, + "open_questions": [ + { + "question": "Can the selected GL64 packet/compiler map be given an all-size field-dependency certificate?", + "why_it_matters": "The conditional reserve bound does not implement packet realization, routing or fresh-field preservation.", + "first_step": "Check one emitted parent/child split, including preservation of exposed ancestors and unused quotient fields; compare PR2097's fresh-fiber contract.", + "blocked_by": "The selected all-size lowering and common-label/mutable-source realization remain inherited assumptions." + }, + { + "question": "Can an actual selected ordinary leaf be source-bound to the zero-extra-external-stock completed interface at all widths?", + "why_it_matters": "The reserve induction uses internal borrowing and restored complete outer spectators, not a scalar endpoint identity alone.", + "first_step": "Trace one selected ordinary borrowing wrapper and its restored row/spectator endpoints at the actual atom widths.", + "blocked_by": "Physical realization, uniform time coefficients and tape contracts are not discharged by this depth checker." + } + ] +} diff --git a/research/selected-bit-ceiling-free-stock/VERIFY.json b/research/selected-bit-ceiling-free-stock/VERIFY.json new file mode 100644 index 0000000000..09b9214e63 --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/bootstrap-cutoff-time-space-split/README.md", + "research/bootstrap-depth-audit/sources/pr387/bootstrap-sources/research/community-round8-audit/pr185-proof-reviewed.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/complex-t16-rare-pattern-exchanges/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" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-Werror", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Exact source binding, contraction and stock coefficient, independent finite depth oracles, required canonical receipt and native first-stage fit guard." + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Optimized read-only verifier acceptance must retain the same exact result." + }, + { + "argv": ["{python}", "-I", "-Werror", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Ten positive and semantic/source/receipt/capacity rejection groups, including isolated optimized public-CLI mutations." + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "All behavioral and failure controls must pass with assertions disabled." + } + ] +} diff --git a/research/selected-bit-ceiling-free-stock/test_verify.py b/research/selected-bit-ceiling-free-stock/test_verify.py new file mode 100644 index 0000000000..642033d32c --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/test_verify.py @@ -0,0 +1,154 @@ +#!/usr/bin/env python3 +"""Behavioral and rejection controls for the conditional stock checker. + +Nick Petalas. Apache-2.0. +""" +import copy +import io +import json +from pathlib import Path +import runpy +import shutil +import subprocess +import sys +import tarfile +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +V = runpy.run_path(str(PACKAGE / "verify.py")) + + +class StockTests(unittest.TestCase): + def test_literal_depths(self): + fixtures = {0: 0, 1: 0, 63: 0, 64: 1, 95: 1, 96: 1, 127: 1, + 128: 2, 191: 2, 192: 2, 256: 3, 384: 3} + self.assertEqual({n: V["forward_depth"](n) for n in fixtures}, fixtures) + + def test_contraction_and_terminal_controls(self): + V["depth_certificate"](64, 42, 28, 17, 64) + self.assertEqual(V["forward_depth"](128), 2) + for args, message in (((64, 42, 28, 18, 64), "strict contraction"), + ((64, 43, 28, 17, 64), "strict contraction"), + ((64, 42, 28, 17, 1), "terminal slack"), + ((64, 42, 65, 17, 64), "bounded contraction")): + with self.subTest(args=args), self.assertRaisesRegex(V["Rejected"], message): + V["depth_certificate"](*args) + + def test_capacity_and_wrong_producer(self): + self.assertEqual(V["forward_depth"](64), 1) + for n, m, r in ((-1, 64, 42), (1 << 4097, 64, 42), + (73, 73, 48), (True, 64, 42)): + with self.subTest(n=n), self.assertRaises(V["Rejected"]): + V["forward_depth"](n, m, r) + + def test_all_child_oracle_must_include_largest_rank(self): + with self.assertRaisesRegex(V["Rejected"], "selected child domain"): + V["finite_checks"]((1, 2, 3, 4)) + self.assertEqual(V["forward_depth"](256), 3) + + def test_floor_is_required(self): + # The weakened ceil recurrence can loop forever at 84. This is a + # countermodel to changing the premise, not a selected compiler bug. + self.assertEqual(V["forward_depth"](84), 1) + self.assertEqual(42 * ((84 + 63) // 64), 84) + self.assertEqual(42 * (84 // 64), 42) + + def test_archive_member_corruption_and_type(self): + data = (ROOT / V["ARCHIVE"]).read_bytes() + tree = V["assembler"](data) + self.assertEqual(V["ast"].literal_eval(V["assignment"](tree, "BIT_BLOB")), + "e293ddc557742637f9f679f083a1a282d87b1b13") + for symlink in (False, True): + stream = io.BytesIO() + with tarfile.open(fileobj=stream, mode="w:gz") as archive: + member = tarfile.TarInfo("code/assemble.py") + if symlink: + member.type = tarfile.SYMTYPE + member.linkname = "elsewhere" + archive.addfile(member) + else: + member.size = 1 + archive.addfile(member, io.BytesIO(b"x")) + with self.subTest(symlink=symlink), self.assertRaises(V["Rejected"]): + V["assembler"](stream.getvalue()) + + def test_cutoff_control(self): + inputs = V["read_inputs"]() + assembly = json.loads(inputs[V["ASSEMBLY"]]) + self.assertEqual(V["first_cutoff"](assembly, 6748)["ell"], 16) + with self.assertRaisesRegex(V["Rejected"], "stock coefficient"): + V["first_cutoff"](assembly, 6747) + bad = copy.deepcopy(assembly) + bad["bootstrap"][0]["cutoff_log2"] = "3" + with self.assertRaisesRegex(V["Rejected"], "stock-fit guard"): + V["first_cutoff"](bad, 6748) + + +class CliTests(unittest.TestCase): + def setUp(self): + self.directory = tempfile.TemporaryDirectory() + self.addCleanup(self.directory.cleanup) + self.root = Path(self.directory.name) + self.package = self.root / "research" / PACKAGE.name + self.package.mkdir(parents=True) + for name in ("verify.py", "SOURCES.json", "RESULT.json"): + shutil.copyfile(PACKAGE / name, self.package / name) + pins = json.loads((PACKAGE / "SOURCES.json").read_bytes())["files"] + self.inputs = [pin["path"] for pin in pins if pin["usage"] == "input"] + for name in self.inputs: + target = self.root / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, target) + + def cli(self): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(self.package / "verify.py")], + cwd=self.root, capture_output=True, text=True, encoding="utf-8", + timeout=120, check=False) + + def test_optimized_public_cli(self): + result = self.cli() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(result.stdout, + "PASS_SELECTED_BIT_CEILING_FREE_STOCK sigma=6748 predecessor=8194 " + "ratio=14/17 widths=100001 ell=16 no_new_kappa\n") + self.assertEqual(result.stderr, "") + + def test_every_live_source_mutation_rejects(self): + for name in self.inputs: + path = self.root / name + original = path.read_bytes() + path.write_bytes(original + b"\n") + try: + result = self.cli() + with self.subTest(source=name): + self.assertNotEqual(result.returncode, 0) + self.assertIn("source SHA256: " + name, result.stderr) + self.assertEqual(result.stdout, "") + finally: + path.write_bytes(original) + + def test_required_receipt_is_read_only(self): + path = self.package / "RESULT.json" + original = path.read_bytes() + altered = json.loads(original) + altered["sigma"] = 6747 + path.write_text(json.dumps(altered), encoding="utf-8") + result = self.cli() + self.assertNotEqual(result.returncode, 0) + self.assertIn("canonical RESULT.json mismatch", result.stderr) + self.assertEqual(json.loads(path.read_bytes())["sigma"], 6747) + path.unlink() + result = self.cli() + self.assertNotEqual(result.returncode, 0) + self.assertIn("FileNotFoundError", result.stderr) + self.assertFalse(path.exists()) + path.write_bytes(original) + result = self.cli() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("sigma=6748", result.stdout) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/selected-bit-ceiling-free-stock/verify.py b/research/selected-bit-ceiling-free-stock/verify.py new file mode 100644 index 0000000000..96b450e3bd --- /dev/null +++ b/research/selected-bit-ceiling-free-stock/verify.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Exact conditional depth/stock refinement for the selected BIT producer. + +Nick Petalas. Apache-2.0. No predecessor verifier is imported or executed. +""" +from __future__ import annotations + +import ast +from bisect import bisect_right +from fractions import Fraction +import hashlib +import io +import json +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SELECTED = "certificates/selected-result.json" +ASSEMBLY = "research/community-frontier1094-audit/ASSEMBLY.json" +BIT = "research/e8-bit-p111-tuned/tune/EXPECTED.json" +ARCHIVE = "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz" +MAX_SOURCE_BYTES = 8 * 1024 * 1024 +MAX_ATOM_BITS = 4097 +MAX_DEPTH = 2 * MAX_ATOM_BITS +FINITE_WIDTH = 100000 + + +class Rejected(ValueError): + """A source, model premise or required receipt did not match.""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise Rejected(message) + + +def authenticate(data: bytes, pin: dict) -> bytes: + require(len(data) <= MAX_SOURCE_BYTES, "source capacity") + digest = hashlib.sha256(data).hexdigest() + header = b"blob " + str(len(data)).encode("ascii") + b"\0" + require(digest == pin["sha256"], "source SHA256: " + pin["path"]) + require(hashlib.sha1(header + data).hexdigest() == pin["git_blob"], + "source Git blob: " + pin["path"]) + return data + + +def read_inputs() -> dict[str, bytes]: + manifest = json.loads((PACKAGE / "SOURCES.json").read_bytes()) + require(len(manifest["files"]) <= 16, "source count capacity") + result = {} + for pin in manifest["files"]: + if pin["usage"] == "input": + path = ROOT / pin["path"] + require(path.stat().st_size <= MAX_SOURCE_BYTES, "source file capacity") + result[pin["path"]] = authenticate(path.read_bytes(), pin) + return result + + +def assembler(data: bytes) -> ast.Module: + with tarfile.open(fileobj=io.BytesIO(data), mode="r:gz") as archive: + for _ in range(1024): + member = archive.next() + if member is None: + break + if member.name == "code/assemble.py": + require(member.isfile() and member.size <= 65536, "assembler member capacity") + stream = archive.extractfile(member) + require(stream is not None, "assembler member missing") + with stream: + payload = stream.read(65537) + require(hashlib.sha256(payload).hexdigest() == + "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a", + "assembler member SHA256") + return ast.parse(payload) + raise Rejected("assembler not found within archive scan capacity") + + +def assignment(tree: ast.Module, name: str) -> ast.expr: + found = [node.value for node in tree.body if isinstance(node, ast.Assign) + and any(isinstance(target, ast.Name) and target.id == name + for target in node.targets)] + require(len(found) == 1, "unique selected assembler assignment: " + name) + return found[0] + + +def selected_parameters(inputs: dict[str, bytes]) -> tuple[dict, tuple[int, ...]]: + selected = json.loads(inputs[SELECTED]) + assembly = json.loads(inputs[ASSEMBLY]) + bit = json.loads(inputs[BIT]) + require(selected["certificate"] == ASSEMBLY, "selected certificate path") + require(selected["certificate_sha256"] == hashlib.sha256(inputs[ASSEMBLY]).hexdigest(), + "selected certificate hash") + require(selected["kappa"] == assembly["kappa"], "selected exponent binding") + citation = assembly["bit_supplier"] + require(citation["pr"] == 589 and citation["path"] == BIT, "selected ordinary BIT producer") + header = b"blob " + str(len(inputs[BIT])).encode("ascii") + b"\0" + require(citation["git_blob_sha1"] == hashlib.sha1(header + inputs[BIT]).hexdigest(), + "selected BIT blob") + tree = assembler(inputs[ARCHIVE]) + require(ast.literal_eval(assignment(tree, "BIT_BLOB")) == citation["git_blob_sha1"], + "assembler BIT source binding") + expression = ast.parse("1 + 7 * BIT_L", mode="eval").body + require(ast.dump(assignment(tree, "BIT_M")) == ast.dump(expression), "BIT dimension formula") + stages = [node.value for node in tree.body if isinstance(node, ast.Assign) + and any(isinstance(t, ast.Tuple) and ast.dump(t) == + ast.dump(ast.parse("BIT_L, BIT_T = 0").body[0].targets[0]) + for t in node.targets)] + require(len(stages) == 1 and ast.literal_eval(stages[0]) == (9, 32), "nine-stage binding") + profile = bit["nine"]["profile"] + require(len(profile) <= 64, "rank inventory capacity") + ranks = tuple(sorted(int(key) for key in profile)) + require(all(type(value) is int and value > 0 for value in profile.values()), "rank counts") + record = bit["nine"]["bit"] + require(ranks[-1] == record["maxchild"] == 42 and ranks[0] == 1, "selected rank boundary") + require(record["physical"] == record["live"] + 9 == 28425, "all physical work roles") + require(record["row_coefficient"] == 2 * (64 ** 2 + 1) + 9909 + 252, "source row bill") + require(assembly["bit_lower"] == bit["nine"]["bit_lower"], "selected saving") + return assembly, ranks + + +def depth_certificate(m: int, r: int, steps: int, bits: int, terminal: int) -> None: + require(all(type(x) is int for x in (m, r, steps, bits, terminal)), "integer certificate") + require(2 <= m <= 128 and 1 <= r < m and 1 <= steps <= 64 and 1 <= bits <= 64, + "bounded contraction domain") + require(1 <= terminal <= m, "terminal domain") + require((1 << bits) * r ** steps < m ** steps, "strict contraction certificate") + require((1 << bits) <= terminal ** steps, "terminal slack, not an additive constant") + + +def forward_depth(n: int, m: int = 64, r: int = 42) -> int: + require(type(n) is int and n >= 0 and n.bit_length() <= MAX_ATOM_BITS, "atom count capacity") + require(m == 64 and r == 42, "selected forward recurrence") + for depth in range(MAX_DEPTH + 1): + if n < m: + return depth + n = r * (n // m) + raise Rejected("depth capacity exhausted") + + +def finite_checks(ranks: tuple[int, ...]) -> dict: + require(len(ranks) <= 64 and all(1 <= r <= 42 for r in ranks) and 42 in ranks, + "selected child domain") + # A separate all-child dynamic program, not the forward maximum-rank loop. + depths = [0] * (FINITE_WIDTH + 1) + for n in range(64, FINITE_WIDTH + 1): + depths[n] = 1 + max(depths[r * (n // 64)] for r in ranks) + require((1 << (17 * depths[n])) <= n ** 28, "finite ceiling-free inequality") + for n in range(FINITE_WIDTH + 1): + require(depths[n] == forward_depth(n), "all-child versus forward depth") + # Independent inverse thresholds, including both sides of each floor cut. + thresholds = [64] + for _ in range(63): + thresholds.append(64 * ((thresholds[-1] + 41) // 42)) + probes = {0, 1, 63, 64, 95, 96, 127, 128} + for threshold in thresholds: + probes.update((threshold - 1, threshold, threshold + 1)) + for n in sorted(probes): + require(forward_depth(n) == bisect_right(thresholds, n), "inverse threshold boundary") + large = [] + for bits in (7, 64, 256, 1024, 4096): + for offset in (-1, 0, 1): + n = (1 << bits) + offset + d = forward_depth(n) + require((1 << (17 * d)) <= n ** 28, "large-width ceiling-free inequality") + large.append([bits, offset, d]) + return {"all_child_widths": FINITE_WIDTH + 1, "threshold_probes": len(probes), + "large_widths": large} + + +def first_cutoff(assembly: dict, sigma: int) -> dict: + require(type(sigma) is int and sigma == 6748, "derived stock coefficient") + s = min(Fraction(assembly["bit_lower"]), + (1 - Fraction(1, 10 ** 24)) * Fraction(assembly["complex_lower"])) - Fraction(1, 10 ** 27) + old = Fraction(384599, 10 ** 10) + new = (1 - s) * s + s * old + delta = min(s - new, 1 - new - s, 1 - new - s * (1 - old), 1 - s) + first = assembly["bootstrap"][0] + require(Fraction(first["exponent"]) == new and Fraction(first["gap"]) == delta, + "selected native first-stage formula") + cutoff = int(first["cutoff_log2"]) + ell = (8 * sigma - 1).bit_length() + require(0 < delta <= 1 - s and cutoff >= 3, "stock-fit domain") + require(cutoff * delta ** 2 >= 36 and cutoff * delta >= 2 * (4 + ell), "stock-fit guard") + return {"branch": "native", "stage": 1, "cutoff_log2": cutoff, "ell": ell, + "gap": str(delta)} + + +def reconstruct(inputs: dict[str, bytes]) -> dict: + assembly, ranks = selected_parameters(inputs) + depth_certificate(64, 42, 28, 17, 64) + sigma = (64 ** 2 + 1) * Fraction(28, 17) + require(sigma.denominator == 1 and sigma == 6748, "exact stock coefficient") + require(6748 * 17 == 8194 * 14, "coefficient comparison") + return {"status": "PASS_SELECTED_BIT_CEILING_FREE_STOCK", "m": 64, "maxchild": 42, + "physical_roles": 28425, "depth_allowance": "28/17", "sigma": int(sigma), + "predecessor_sigma": 8194, "coefficient_ratio": "14/17", + "finite_checks": finite_checks(ranks), "first_cutoff": first_cutoff(assembly, int(sigma)), + "scope": "Conditional packet/completed-leaf envelope only; no new kappa or supplier admission."} + + +def check_receipt(actual: dict, receipt: dict) -> None: + require(actual == receipt, "required canonical RESULT.json mismatch") + + +def main() -> None: + actual = reconstruct(read_inputs()) + receipt = json.loads((PACKAGE / "RESULT.json").read_bytes()) + check_receipt(actual, receipt) + print(f"{actual['status']} sigma=6748 predecessor=8194 ratio=14/17 " + f"widths={actual['finite_checks']['all_child_widths']} ell=16 no_new_kappa") + + +if __name__ == "__main__": + main()