diff --git a/research/r437-descendant-stock/README.md b/research/r437-descendant-stock/README.md new file mode 100644 index 0000000000..357e1bf9f9 --- /dev/null +++ b/research/r437-descendant-stock/README.md @@ -0,0 +1,180 @@ +# R437 descendant stock: retain the 9475 factor once + +**Scoped stock theorem and arithmetic path certificate; no new kappa.** For the +row quotient and stock guard used by the pinned R437 physical caller, sufficient +root stock is + +\[ + R=t\,9475\,A^{D(n)},\qquad + A=28416\,|\mathrm{GL}_{64}(\mathbb F_q)|\,q^{4096(w-1)},\quad t\geq1, +\] + +when `n >= 64`; any positive row count suffices for this internal-node condition +when `n < 64`. Here `D(n)=0` below 64 and +`D(n)=1+D(42 floor(n/64))` otherwise. The original root's `q,w` stay fixed. + +PR4176's `NUMERICAL.md` section 5 uses the stronger sufficient stock `t K^D`, +where `K=lcm(28416,28425)|GL64|q^(4096(w-1))=9475 A`. +Thus at positive depth `D` this component's least sufficient divisor is smaller +by exactly **9475^(D-1)**. This does not identify a defect in that conservative +bound. Its `check_stock_rows` intentionally rejects our smaller stock for `D>1`; +the frozen numerical wrapper is unchanged and does not admit it. + +The new divisor is necessary and sufficient for **all paths allowed by this +rank-ceiling row-guard model**. Necessity is not a claim that every maximal path +is produced by the actual compiler, or that this is the least stock for every +other construction obligation. The universal result is the written argument +below; finite checks support its source binding and implementation. + +## Actual source boundary + +All sources are exact bytes at canonical main +`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`; `SOURCES.json` binds their blobs and +SHA256 digests. No predecessor source is edited. + +1. `r437-pooled-native-interface/replica_catalogue.py`, `ReplicaTopology`, has + 28,416 families. `selected-bit-physical-caller/macro_binding.py`, + `SelectedBinding`, sets cutoff 64 and `stock_multiple=9475`. +2. `fresh_rows.quotient` divides positive rows successively by the family count, + `context.codes.size=|GL64(F_q)|`, then by `q` exactly `4096(w-1)` times. + Its `radix_power` source yields once per division of `q^w` by `q` until 1; + the first of those `w` iterations is skipped for each of 4096 matrix entries. + Every remainder must be zero, and the quotient must be positive. +3. `Machine.node` stores that quotient as `unused` and immediately requires + divisibility by 9475. Its `prepare_child` handoff passes `unused` as the + child's `rows` port through the fixed `CAPSULE` ordering. It does not divide + the child's inherited row count by 9475. +4. `r437-carrier-integration/numerical.py` supplies the declared maximum paid + rank 42 and the depth recurrence. The separate native/compiler claim that + every child width is at most `42 floor(n/64)` is retained as a premise. + +These facts identify the recurrence `R_child=R_parent/A` and the local +condition `9475 | R_child`. They do not price `Count` arithmetic, prove the +complete request inventory, or execute a recursive payload. The source's +`SelectedBinding.check_stock` placeholder is not presented as an installed +descendant validator. + +## Proof and exact scope + +Put `S=9475`. First fix any positive integers `A,S` and a path with exactly `d` +internal transitions. At transition `j`, starting with `j=1`, the unchanged +guards require a positive exact quotient `R/A^j` divisible by `S`. +The final condition implies `S A^d | R`. Conversely, if `R=t S A^d`, every +quotient is the positive integer `t S A^(d-j)`, so all guards pass. Consequently +the least positive stock on a path of length `d` is **S A^d**, without any +coprimality assumption about `A` and `S`. With zero transitions no guard is run. + +For the width model, let `g(n)=42 floor(n/64)`. On internal widths, `g` is +nondecreasing and strictly smaller than `n`. Iterating it shows that `D` is +nondecreasing. Every permitted child `1 <= c <= g(n)` therefore satisfies +`D(c) <= D(n)-1`. Along a path at depth `j`, `D(n_j) <= D(n_0)-j`. +Starting with `R_0=t S A^D`, exact row inheritance gives + +\[ + R_j=t S A^{D-j}. +\] + +If node `j` is internal, `D-j >= 1`, so its quotient remains divisible by `S`. +Moreover its inherited rows are divisible by the new sufficient divisor for +its entire remaining subtree: for `D(n_j)>0`, the multiplier is +`t A^(D-j-D(n_j))`. At a leaf the divisor is 1. This proves all bounded paths +are covered, including early leaf termination and paths stopping internally. + +The maximal path `n,g(n),g(g(n)),...` has exactly `D(n)` transitions in the +declared model. Applying the first paragraph to that path proves necessity +within the model. A compiler that forbids that path might permit less stock; +we make no such reachability claim. Additional stock predicates outside the +two identified guards are also outside this minimum claim. + +`stock.py` implements a separate arithmetic certificate. It anchors the first +node to a supplied root, preserves its field and precision, checks the rank +ceiling, and requires **exact** parent-to-child row equality. Local divisibility +alone is insufficient: at widths `128 -> 84`, twice the correct child stock +passes its local divisibility test but is not the parent's quotient. The +checker rejects that forged path. The supplied root still needs external +prime, precision, source and Program authentication. This component does not +replace PR4176's complete `checked_entry` or remove its root-only restriction. + +## Reproduction and evidence + +Python 3.12, standard library only: + +```sh +python -B scripts/research_package.py --package research/r437-descendant-stock +``` + +Direct replay, including in a Git-free export containing the declared inputs: + +```sh +python -B research/r437-descendant-stock/verify.py +python -O -B research/r437-descendant-stock/verify.py +``` + +Ordinary verification is read-only and compares the complete deterministic +`RESULT.json`. Explicit `--write` is reserved for receipt regeneration. +The receipt reports: + +- 1,024 width comparisons with the pinned depth function and **323,232** child + transitions checking the depth inequality. +- **25,620** exhaustive abstract `(A,S,d,R)` cases comparing the formula with + repeated local guards (`A=1..5`, `S=1..4`, `d=0..4`, `1 <= R <= 2 S A^d+1`, + with leaf divisor 1). These include non-coprime factors. +- **14** internal nodes through the unchanged AST of `fresh_rows.quotient` and + the four-statement quotient/stock block in `Machine.node`, using an explicitly + substituted **integer Count/Word adapter**, including the source's radix loop. + This checks control-flow arithmetic, + not binary tape operations, acquisition, cleanup or timing. +- Four full maximal paths with `(q,w,n)=(3,1,64),(3,2,128),(5,2,512),(3,2,2048)`. + At width 512, depth 4, the old/new stock factor is **850,624,046,875**. At + width 2048, depth 7, it is **723,561,269,122,002,197,265,625**. These are row + cardinality ratios, not time savings or practical materialized datasets. +- **17** rejecting controls, including locally divisible but unrelated rows, + lost high-lift/family/9475 factors, one missing recursive factor, precision + and field changes, wrong widths, missing roots, and continuation below cutoff. + Three controls confirm that the predecessor's stronger wrapper rejects the + new smaller stock; this is expected, not a failed predecessor test. + +The q=3/q=5 fixtures are semantic arithmetic checks, not the q>2^80 numerical +admission. No full selected cold replay, compiler catalogue, Lean, Docker, +native payload, source preparation or physical tape simulation was run. The +orientation command `research_selected_baseline.py` stopped on an omitted +`certificates/checkpoints/frontier4359.json` in this sparse checkout; no baseline +pass is claimed. The selected record remains conditional kappa 0.00302015. + +## Coordination and attribution + +Task `r437-carrier-integration`, revision 7, refined from the bit-mechanisms +draw `5b8bdff3d61d78a94ac212b844fcd944` to this exact stock implication. +[Discussion #4682](https://github.com/CrocSwap/integer-mult-bounds/discussions/4682) +is the canonical claim/result. Overlap checks covered R437, descendant/path +certificates, 9475 and stock-divisor terms. The initial remote snapshot had +448 open PRs and 3,606 Discussion records with complete pagination; local +coverage was sparse and closed PR bodies/code diffs were not fully searched. +The central ledger was consulted. PR4584 audits the separate pivot implication; +PR4612 concerns selected BIT row stock, with different atom and call boundaries. + +Chris R / Clear1nsight's PR4067 and PR4176 supply the changed carrier, complete +source interface, conservative K^D bound and explicit descendant-certificate +gap. unpaidmoon / PR4147 supplies the earlier coefficient audit, not recomputed +here. The literal caller and stock interfaces retain Jose Manuel / +jmbarrancoml, David Arias, Nick Petalas, ywz65 and the PR2753/2769 lineage. +The R437/hosting/source predecessors retain ai-nanachi, Ali Romman, Sagar Thakrar, +Rohan Arun, zxv, Ross Richardson and all notices in the pinned packages. +New proof, arithmetic certificate and checks: Mihir Srivastava (mihir-s-05), +with substantial OpenAI Codex assistance. Apache-2.0. This is author-checked +work with separately written arithmetic, not independent human review or +formal proof-kernel verification. + +## Open next questions + +1. **Bind an arithmetic path to actual produced Program events.** This is + necessary before extending the numerical entry to descendants. Start with + one authenticated `checked_entry` root, its `Machine.prepare_child` handoff + and decoded chronological STEP. The blocker is proving actual request, + width, source identity and inherited `rows` correspondence; a list of valid + integers does not establish that correspondence. +2. **Price or implement the guard on the physical Count tapes.** The theorem + removes a repeated stock factor but gives no physical cost reduction. Start + by running the unchanged quotient and stock check with real tape Count + objects and the same fixed root precision. Complete source-table, payload, + visited-backing and blank-return costs remain separate obligations. diff --git a/research/r437-descendant-stock/RESULT.json b/research/r437-descendant-stock/RESULT.json new file mode 100644 index 0000000000..57574b7cbf --- /dev/null +++ b/research/r437-descendant-stock/RESULT.json @@ -0,0 +1,120 @@ +{ + "abstract_guard_cases": 25620, + "bounded_child_transitions": 323232, + "depth_widths": 1024, + "fixtures": [ + { + "certificate": { + "depth": 1, + "root_multiplier": 1, + "scope": "arithmetic stock only; Program/source binding remains external", + "terminal_width": 42, + "transitions": 1 + }, + "old_to_new_factor": "1", + "q": 3, + "root_stock_bits": 6520, + "root_stock_sha256": "b4b2fab41fd0a7ab8f92729e4049ab786f2b7de7db4938ba58754e3ce4c38be3", + "w": 1, + "widths": [ + 64, + 42 + ] + }, + { + "certificate": { + "depth": 2, + "root_multiplier": 1, + "scope": "arithmetic stock only; Program/source binding remains external", + "terminal_width": 42, + "transitions": 2 + }, + "old_to_new_factor": "9475", + "q": 3, + "root_stock_bits": 26010, + "root_stock_sha256": "fb854591452036d2cbacbaad05d441a36f7f0f8434c7b8f185c9b877811d15b2", + "w": 2, + "widths": [ + 128, + 84, + 42 + ] + }, + { + "certificate": { + "depth": 4, + "root_multiplier": 1, + "scope": "arithmetic stock only; Program/source binding remains external", + "terminal_width": 42, + "transitions": 4 + }, + "old_to_new_factor": "850624046875", + "q": 5, + "root_stock_bits": 76156, + "root_stock_sha256": "8bd793adab2a26e4096b73ab69c93bf9c55f9d61f5d467d68265d40d1158815c", + "w": 2, + "widths": [ + 512, + 336, + 210, + 126, + 42 + ] + }, + { + "certificate": { + "depth": 7, + "root_multiplier": 1, + "scope": "arithmetic stock only; Program/source binding remains external", + "terminal_width": 42, + "transitions": 7 + }, + "old_to_new_factor": "723561269122002197265625", + "q": 3, + "root_stock_bits": 91000, + "root_stock_sha256": "46cf1c4882729cec1f8ffa18058b80433c0c8a4e0a56344a05be475a24c00cdc", + "w": 2, + "widths": [ + 2048, + 1344, + 882, + 546, + 336, + 210, + 126, + 42 + ] + } + ], + "literal_internal_nodes": 14, + "rejected_controls": [ + "old_guard_rejects_new_stock_n128", + "old_guard_rejects_new_stock_n512", + "old_guard_rejects_new_stock_n2048", + "locally_valid_but_unrelated_descendant", + "changed_precision", + "changed_field", + "missing_root", + "wrong_child_width", + "transition_below_cutoff", + "noninteger_rows", + "empty_path", + "lost_9475_factor", + "inexact_family_factor", + "empty_stock", + "lost_high_lift_factor", + "undivided_child_rows", + "one_missing_recursion_factor" + ], + "scope": "Sharp row-guard arithmetic; integer Count adapter, no tape/payload replay, supplier admission or new kappa", + "source_sha256": { + "research/r437-carrier-integration/NUMERICAL.md": "e2303eec688d963390f5df4440300bee75840c2c485d94d7342a7d2ef1430438", + "research/r437-carrier-integration/numerical.py": "83f2b60a90ab2d0354c5c84f48af246ab416605c3ae4bd62368bbe5f23bb53bb", + "research/r437-pooled-native-interface/replica_catalogue.py": "d093a5a5421596d82c6c6e9fbc7fbf3f313c803a7ba423d666b98344b1912ff3", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py": "e4ae08fbd658add630eb7754ebe0cbcb42c6f39cf4128f9cb92e27fcf5213a7d", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22", + "research/selected-bit-physical-caller/macro_binding.py": "9ef31765d03d2c54fad9296f2ff0707a190ce169e44de4f0f45214e3c410c01a", + "research/selected-bit-physical-caller/macro_machine.py": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a" + }, + "status": "PASS_R437_DESCENDANT_STOCK" +} diff --git a/research/r437-descendant-stock/SOURCES.json b/research/r437-descendant-stock/SOURCES.json new file mode 100644 index 0000000000..63b93e4303 --- /dev/null +++ b/research/r437-descendant-stock/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/r437-carrier-integration/NUMERICAL.md", + "usage": "input", + "git_blob": "1001480b0ba8da8bae4ae8f53c18d8c6aa9d7b57", + "sha256": "e2303eec688d963390f5df4440300bee75840c2c485d94d7342a7d2ef1430438" + }, + { + "path": "research/r437-carrier-integration/numerical.py", + "usage": "input", + "git_blob": "d3411758be96f22f8d64e02ba278dc46b21639c5", + "sha256": "83f2b60a90ab2d0354c5c84f48af246ab416605c3ae4bd62368bbe5f23bb53bb" + }, + { + "path": "research/r437-pooled-native-interface/replica_catalogue.py", + "usage": "input", + "git_blob": "1fa6ea58c5193952bc6175cbb9f1a778a6502eac", + "sha256": "d093a5a5421596d82c6c6e9fbc7fbf3f313c803a7ba423d666b98344b1912ff3" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py", + "usage": "input", + "git_blob": "aa3a327604308d3a5c7a27b65f5e631d430ab093", + "sha256": "e4ae08fbd658add630eb7754ebe0cbcb42c6f39cf4128f9cb92e27fcf5213a7d" + }, + { + "path": "research/selected-bit-physical-caller/macro_binding.py", + "usage": "input", + "git_blob": "c197eb6458be9374cb4684c654bfc99e619dcaf0", + "sha256": "9ef31765d03d2c54fad9296f2ff0707a190ce169e44de4f0f45214e3c410c01a" + }, + { + "path": "research/selected-bit-physical-caller/macro_machine.py", + "usage": "input", + "git_blob": "5a032e8923f7f8b22bb98f3e39b804beb9906c16", + "sha256": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py", + "usage": "input", + "git_blob": "b8ba857e32c5903408e1e61ff916300848b4a208", + "sha256": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22" + } + ] +} diff --git a/research/r437-descendant-stock/TASK.json b/research/r437-descendant-stock/TASK.json new file mode 100644 index 0000000000..91ed9d7eec --- /dev/null +++ b/research/r437-descendant-stock/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "r437-carrier-integration", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "r437-carrier-integration", + "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/r437-two-window-carrier/README.md", + "research/r437-reverse-row-coefficient/README.md" + ], + "methods": [ + "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.", + "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample." + ], + "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4067 paid profile and open integration obligations; #4147 covers the reverse row coefficient. Three additional ADDs per call and all helpers remain charged. This is not a selected supplier.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.", + "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.", + "allowed_variations": [ + "One compiler rebind, one actual caller boundary, or one precision/stock implication." + ], + "scope_change_triggers": [ + "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram." + ], + "overlap_terms": [ + "R437", + "two-window carrier", + "4067", + "4147", + "pooled compiler", + "request alignment", + "reverse row coefficient" + ], + "existing_checks": [ + { + "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4147: reverse row coefficient follow-up.", + "evidence": "research/r437-reverse-row-coefficient/README.md", + "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.", + "status": "author-checked", + "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Sharp sufficient divisor 9475*A^D for the pinned R437 fresh-row quotient and stock guard, plus a separately implemented arithmetic descendant path certificate.", + "scope_change_reason": "The revision-7 integration card and PR4176 explicitly leave descendant path admission open. This isolates its row-cardinality component at the actual quotient and stock guard; no numerical-wrapper or payload admission is claimed.", + "bottleneck_link": "Removes repeated conservative stock factors without changing the paid profile; gives a concrete arithmetic component for original-root descendant validation. Actual Program/source binding and physical cost remain required.", + "budget_minutes": 60, + "stop_rule": "Finish the written induction, one bounded exact verifier and rejecting controls. Stop before full compiler, payload, tape or selected cold replay; do not infer kappa or activate a new admission contract.", + "outcome": "completed", + "evidence": "README proof; RESULT.json: 323232 width transitions, 25620 abstract guard cases, 14 source-guard nodes and 17 rejecting controls. Normal and optimized Python 3.12 replays. The literal AST uses an explicitly disclosed integer Count adapter, not physical tapes.", + "author": "Mihir Srivastava (mihir-s-05), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in investigation, proof, implementation, verification and writing; no independent human or proof-kernel review claimed.", + "open_questions": [ + { + "question": "Bind the arithmetic path to actual produced Program events.", + "why_it_matters": "Required before extending original-root numerical admission to descendants.", + "first_step": "Follow one authenticated root through Machine.prepare_child, its CAPSULE rows port and decoded chronological STEP.", + "blocked_by": "Actual request/source identity and width/stock correspondence are not certified by an integer node list." + }, + { + "question": "Price or implement the guard on physical Count tapes.", + "why_it_matters": "The stock-cardinality reduction alone is not a physical cost or runtime improvement.", + "first_step": "Run the pinned quotient and stock guard on real tape Count objects at fixed original-root precision.", + "blocked_by": "Source construction, payload, visited backing, cleanup and encoded guard tariffs remain unpriced." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4682", + "selector_seed": "5b8bdff3d61d78a94ac212b844fcd944", + "predecessor_heads": { + "4176": "71914dfbc9ed757f6746c02e9206bb7a984edfbb", + "4584": "cc304c09c48103c20e7c0e2634b22d0aa19aa38a", + "4612": "7e362114fa41570bffe74dbb32896f13354a54cd" + }, + "scope_exclusions": [ + "Complete Program/source-path authentication", + "Physical Count and payload execution", + "Complete logical/physical reserve admission", + "Prime and original-root precision authentication", + "New selected kappa" + ], + "overlap": { + "checked_at": "2026-10-22T15:44:45Z", + "main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "priority_revision": 7, + "open_prs": 448, + "discussion_records": 3606, + "remote_complete_pagination": true, + "local_coverage": "partial sparse notes plus central ledger; code diffs and closed PR bodies not fully searched" + } +} diff --git a/research/r437-descendant-stock/VERIFY.json b/research/r437-descendant-stock/VERIFY.json new file mode 100644 index 0000000000..93242ef517 --- /dev/null +++ b/research/r437-descendant-stock/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/r437-carrier-integration/NUMERICAL.md", + "research/r437-carrier-integration/numerical.py", + "research/r437-pooled-native-interface/replica_catalogue.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py", + "research/selected-bit-physical-caller/macro_binding.py", + "research/selected-bit-physical-caller/macro_machine.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source bindings, stock induction fixtures, literal quotient/stock guard under integer Count adapter, rejected forged paths and missing factors" + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same deterministic evidence and rejecting controls under optimized Python" + } + ] +} diff --git a/research/r437-descendant-stock/stock.py b/research/r437-descendant-stock/stock.py new file mode 100644 index 0000000000..c1803dd689 --- /dev/null +++ b/research/r437-descendant-stock/stock.py @@ -0,0 +1,89 @@ +"""R437 arithmetic stock certificates; no physical or Program admission. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from dataclasses import dataclass +from functools import lru_cache + +FAMILIES, STOCK_MULTIPLE, DIMENSION, MAX_RANK = 28416, 9475, 64, 42 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def positive_integer(value, name): + require(type(value) is int and value > 0, "positive integer " + name) + + +def depth(n): + positive_integer(n, "width") + result = 0 + while n >= DIMENSION: + n = MAX_RANK * (n // DIMENSION) + result += 1 + return result + + +@lru_cache(None, typed=True) +def row_factor(q, w): + """A = W |GL_64(F_q)| q^(4096(w-1)); prime q is an external premise.""" + positive_integer(q, "field order") + positive_integer(w, "root precision") + require(q >= 3 and q % 2 == 1, "odd field parameter") + order = 1 + for i in range(DIMENSION): + order *= q**DIMENSION - q**i + return FAMILIES * order * q ** (DIMENSION**2 * (w - 1)) + + +def stock_divisor(n, q, w): + """Sharp for the complete rank-ceiling path model; see README proof.""" + d = depth(n) + return 1 if d == 0 else STOCK_MULTIPLE * row_factor(q, w)**d + + +@dataclass(frozen=True) +class Node: + width: int + rows: int + q: int + w: int + + +def certify_path(root, nodes): + """Check root anchoring, exact row inheritance and future stock sufficiency. + + A path may stop internally. The caller must separately authenticate the + original root parameters and bind each node to actual Program events. + """ + require(isinstance(root, Node), "typed root") + require(isinstance(nodes, (list, tuple)) and len(nodes) > 0, "nonempty path") + positive_integer(root.width, "root width") + positive_integer(root.rows, "root rows") + factor = row_factor(root.q, root.w) + require(nodes[0] == root, "path begins at the supplied root") + divisor = stock_divisor(root.width, root.q, root.w) + require(root.rows % divisor == 0, "root stock covers every bounded path") + for i, node in enumerate(nodes): + require(isinstance(node, Node), "typed descendant") + positive_integer(node.width, "descendant width") + positive_integer(node.rows, "descendant rows") + positive_integer(node.q, "descendant field") + positive_integer(node.w, "descendant precision") + require((node.q, node.w) == (root.q, root.w), "unchanged original-root field and precision") + require(node.rows % stock_divisor(node.width, root.q, root.w) == 0, + "descendant stock covers its remaining subtree") + if node.width >= DIMENSION: + require(node.rows % factor == 0, "complete family/low/high factors") + require((node.rows // factor) % STOCK_MULTIPLE == 0, + "caller unused-row stock factor") + if i: + parent = nodes[i - 1] + require(parent.width >= DIMENSION, "no transition below cutoff") + require(node.width <= MAX_RANK * (parent.width // DIMENSION), "actual rank ceiling") + require(parent.rows == factor * node.rows, "exact parent-to-child row quotient") + return {"depth": depth(root.width), "transitions": len(nodes) - 1, + "terminal_width": nodes[-1].width, "root_multiplier": root.rows // divisor, + "scope": "arithmetic stock only; Program/source binding remains external"} diff --git a/research/r437-descendant-stock/verify.py b/research/r437-descendant-stock/verify.py new file mode 100644 index 0000000000..a5f2fe16f7 --- /dev/null +++ b/research/r437-descendant-stock/verify.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +"""Source-bound stock proof checks using an explicit integer Count adapter. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import ast +from dataclasses import replace +from hashlib import sha256 +import json +from pathlib import Path +from types import SimpleNamespace +from stock import (DIMENSION, FAMILIES, MAX_RANK, STOCK_MULTIPLE, Node, + certify_path, depth, require, row_factor, stock_divisor) + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FRESH = "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py" +MACHINE = "research/selected-bit-physical-caller/macro_machine.py" +NUMERICAL = "research/r437-carrier-integration/numerical.py" +CARDINALITY = "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py" + + +def authenticate(): + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + checked = {} + for row in pins["files"]: + if row["usage"] == "input": + data = (ROOT / row["path"]).read_bytes() + require(sha256(data).hexdigest() == row["sha256"], "source hash: " + row["path"]) + checked[row["path"]] = row["sha256"] + return checked + + +class IntegerCount: + """Mathematical interface used by the unchanged quotient and next guard.""" + def __init__(self, value): + self.value = value.value if isinstance(value, IntegerCount) else value + + def divide_small(self, divisor): + self.value, remainder = divmod(self.value, divisor) + return remainder + + def zero(self): + return self.value == 0 + + def close(self): + pass + + +def positive(value): + require(isinstance(value, IntegerCount) and value.value > 0, "positive Count") + + +def integer_ring(q, w): + """Integer adapter for the retained radix_power Word interface.""" + arena = SimpleNamespace(literal=IntegerCount, copy=IntegerCount, + free_many=lambda *words: None) + raw = SimpleNamespace(compare=lambda a, b: (a.value > b.value) - (a.value < b.value), + divmod=lambda a, b: tuple(IntegerCount(v) for v in divmod(a.value, b.value))) + return SimpleNamespace(arena=arena, raw=raw, modulus=IntegerCount(q**w), one=IntegerCount(1)) + + +def source_guard(): + tree = ast.parse((ROOT / FRESH).read_text(encoding="utf-8")) + quotient = next(n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == "quotient") + scope = {"Count": IntegerCount, "positive": positive, "need": require} + cardinality = ast.parse((ROOT / CARDINALITY).read_text(encoding="utf-8")) + radix = next(n for n in cardinality.body if isinstance(n, ast.FunctionDef) and n.name == "radix_power") + exec(compile(ast.Module(body=[radix], type_ignores=[]), CARDINALITY, "exec"), scope) + for q, w in [(3, 1), (3, 2), (5, 3)]: + require(sum(1 for _ in scope["radix_power"](integer_ring(q, w), q)) == w, + "literal radix_power iteration count") + exec(compile(ast.Module(body=[quotient], type_ignores=[]), FRESH, "exec"), scope) + machine = ast.parse((ROOT / MACHINE).read_text(encoding="utf-8")) + cls = next(n for n in machine.body if isinstance(n, ast.ClassDef) and n.name == "Machine") + method = next(n for n in cls.body if isinstance(n, ast.FunctionDef) and n.name == "node") + start = next(i for i, n in enumerate(method.body) if isinstance(n, ast.Assign) + and isinstance(n.targets[0], ast.Name) and n.targets[0].id == "unused") + block = method.body[start:start + 4] + require([type(n).__name__ for n in block] == ["Assign", "Expr", "Assign", "Try"], + "literal quotient/save/stock/guard block") + scope["fresh_rows"] = SimpleNamespace(quotient=scope["quotient"]) + code = compile(ast.Module(body=block, type_ignores=[]), MACHINE, "exec") + + def check(rows, q, w): + order = 1 + for i in range(64): + order *= q**64 - q**i + counts = {"rows": IntegerCount(rows)} + runtime = SimpleNamespace(context=SimpleNamespace(codes=SimpleNamespace(size=order), + dimension=64, ring=integer_ring(q, w), q=q), + topology=SimpleNamespace(families=FAMILIES), + binding=SimpleNamespace(stock_multiple=STOCK_MULTIPLE), + count=lambda name: counts[name], + save_count=lambda value, name: counts.__setitem__(name, value)) + exec(code, dict(scope, self=runtime)) + return counts["unused"].value + return check + + +def run(): + pins, guard = authenticate(), source_guard() + predecessor = {"__name__": "pinned_numerical", "__file__": str(ROOT / NUMERICAL)} + exec(compile((ROOT / NUMERICAL).read_bytes(), NUMERICAL, "exec"), predecessor) + require((predecessor["W"], predecessor["M"]) == (FAMILIES, DIMENSION), "source constants") + require(predecessor["STOCK_MULTIPLIER"] == FAMILIES * STOCK_MULTIPLE, "K = 9475 A") + require(max(predecessor["PROFILE_D"]) == MAX_RANK, "declared maximum rank") + require("cutoff, stock_multiple, child_mode = 64, 9475, 0" in + (ROOT / "research/selected-bit-physical-caller/macro_binding.py").read_text(), + "literal binding stock factor") + require("replicas, pairs, ports, families, stride = 32, 4, 111, 28416, 888" in + (ROOT / "research/r437-pooled-native-interface/replica_catalogue.py").read_text(), + "literal pooled family count") + transitions = 0 + for n in range(1, 1025): + require(depth(n) == predecessor["depth"](n), "independent depth recurrence") + if n >= 64: + for c in range(1, 42 * (n // 64) + 1): + require(depth(c) <= depth(n) - 1, "rank-ceiling depth monotonicity") + transitions += 1 + abstract_cases = 0 + for a in range(1, 6): + for s in range(1, 5): + for d in range(5): + minimum = s * a**d if d else 1 + for rows in range(1, 2 * minimum + 2): + value, valid = rows, True + for _ in range(d): + value, remainder = divmod(value, a) + if remainder or value <= 0 or value % s: + valid = False + break + require(valid == (rows % minimum == 0), "sharp abstract stock characterization") + abstract_cases += 1 + rejected = [] + def reject(name, callback): + try: + callback() + except ValueError: + rejected.append(name) + else: + raise ValueError("failed rejection control: " + name) + fixtures, literal_nodes = [], 0 + for q, w, n in [(3, 1, 64), (3, 2, 128), (5, 2, 512), (3, 2, 2048)]: + a, d = row_factor(q, w), depth(n) + root = Node(n, stock_divisor(n, q, w), q, w) + nodes = [root] + while nodes[-1].width >= 64: + p = nodes[-1] + actual = guard(p.rows, q, w) + require(actual == p.rows // a, "source quotient matches independent A") + nodes.append(Node(42 * (p.width // 64), actual, q, w)) + literal_nodes += 1 + result = certify_path(root, nodes) + require(len(nodes) - 1 == d and nodes[-1].rows == STOCK_MULTIPLE, "maximal path terminal stock") + old_rows = predecessor["stock_unit"](q, w)**d + require(old_rows == root.rows * STOCK_MULTIPLE**(d - 1), "old/new ratio") + old_nodes = [replace(v, rows=v.rows * STOCK_MULTIPLE**(d - 1)) for v in nodes] + certify_path(old_nodes[0], old_nodes) + if d > 1: + reject(f"old_guard_rejects_new_stock_n{n}", + lambda r=root: predecessor["check_stock_rows"](r.rows, r.width, r.q, r.w)) + fixtures.append({"q": q, "w": w, "widths": [v.width for v in nodes], + "root_stock_bits": root.rows.bit_length(), + "root_stock_sha256": sha256(root.rows.to_bytes((root.rows.bit_length()+7)//8, "big")).hexdigest(), + "old_to_new_factor": str(STOCK_MULTIPLE**(d - 1)), "certificate": result}) + a = row_factor(3, 2) + root = Node(128, stock_divisor(128, 3, 2), 3, 2) + child = Node(84, root.rows // a, 3, 2) + leaf = Node(42, child.rows // a, 3, 2) + certify_path(root, [root, child, leaf]) + forged = replace(child, rows=2 * child.rows) + require(forged.rows % stock_divisor(84, 3, 2) == 0, "forgery passes local test") + reject("locally_valid_but_unrelated_descendant", lambda: certify_path(root, [root, forged])) + reject("changed_precision", lambda: certify_path(root, [root, replace(child, w=1)])) + reject("changed_field", lambda: certify_path(root, [root, replace(child, q=5)])) + reject("missing_root", lambda: certify_path(root, [child])) + reject("wrong_child_width", lambda: certify_path(root, [root, replace(child, width=85)])) + reject("transition_below_cutoff", lambda: certify_path(root, [root, child, leaf, leaf])) + reject("noninteger_rows", lambda: certify_path(replace(root, rows=1.0), [root])) + reject("empty_path", lambda: certify_path(root, [])) + reject("lost_9475_factor", lambda: guard(a, 3, 2)) + reject("inexact_family_factor", lambda: guard(root.rows + 1, 3, 2)) + reject("empty_stock", lambda: guard(0, 3, 2)) + reject("lost_high_lift_factor", lambda: guard(row_factor(3, 1)*STOCK_MULTIPLE, 3, 2)) + reject("undivided_child_rows", lambda: certify_path(root, [root, replace(child, rows=root.rows)])) + short = STOCK_MULTIPLE * a + require(guard(short, 3, 2) == STOCK_MULTIPLE, "depth-one positive control") + reject("one_missing_recursion_factor", lambda: guard(guard(short, 3, 2), 3, 2)) + require(stock_divisor(63, 3, 2) == 1, "leaf has no internal guard") + return {"status": "PASS_R437_DESCENDANT_STOCK", "source_sha256": pins, + "depth_widths": 1024, "bounded_child_transitions": transitions, + "abstract_guard_cases": abstract_cases, "literal_internal_nodes": literal_nodes, + "fixtures": fixtures, "rejected_controls": rejected, + "scope": "Sharp row-guard arithmetic; integer Count adapter, no tape/payload replay, supplier admission or new kappa"} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true", help="explicit receipt regeneration") + args = parser.parse_args() + result, receipt = run(), HERE / "RESULT.json" + if args.write: + receipt.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8", newline="\n") + else: + require(json.loads(receipt.read_text(encoding="utf-8")) == result, "complete deterministic receipt") + print(result["status"], "transitions=" + str(result["bounded_child_transitions"]), + "abstract=" + str(result["abstract_guard_cases"]), + "literal_nodes=" + str(result["literal_internal_nodes"]), + "controls=" + str(len(result["rejected_controls"])))