From 671757dfe548948e5a69e63058b98233b6a8f283 Mon Sep 17 00:00:00 2001 From: Mainzu <107363567+Mainzu@users.noreply.github.com> Date: Sun, 18 Oct 2026 19:55:58 +0700 Subject: [PATCH 1/5] Research: selected m=73 row-ledger terms do not bind rho Source-bind the selected m=73 ledger's non-complex terms: 9909 = 367*27 (historical coarse-bit family), 252 = 9*28 (old ordinary leaf), 1024 = 2*512 (prefix). They are external polynomial-reserve degrees, so #3113's 16469/15555 readings do not bind rho. rho = 0 under the completed-leaf contract (sigma <= 4362.14) or rho >= sigma_BIT = 8194 under PR2084 if the parent reserves the BIT factor; both pass the stage-1 guard. Partial; no new kappa. 42 checks, 10 mutation controls. Co-Authored-By: Claude Opus 5.5 --- research/selected-stock-rho-ledger/README.md | 157 +++++++++++ .../selected-stock-rho-ledger/SOURCES.json | 90 +++++++ research/selected-stock-rho-ledger/TASK.json | 94 +++++++ .../selected-stock-rho-ledger/VERIFY.json | 32 +++ research/selected-stock-rho-ledger/verify.py | 252 ++++++++++++++++++ 5 files changed, 625 insertions(+) create mode 100644 research/selected-stock-rho-ledger/README.md create mode 100644 research/selected-stock-rho-ledger/SOURCES.json create mode 100644 research/selected-stock-rho-ledger/TASK.json create mode 100644 research/selected-stock-rho-ledger/VERIFY.json create mode 100644 research/selected-stock-rho-ledger/verify.py diff --git a/research/selected-stock-rho-ledger/README.md b/research/selected-stock-rho-ledger/README.md new file mode 100644 index 0000000000..d63a461b67 --- /dev/null +++ b/research/selected-stock-rho-ledger/README.md @@ -0,0 +1,157 @@ +# Selected m=73 row ledger: the non-complex terms do not bind `rho` + +**Card `selected-stock-envelope`, scope refined. Partial. No new κ.** +[#3113](https://github.com/CrocSwap/integer-mult-bounds/pull/3113) and +[#3421](https://github.com/CrocSwap/integer-mult-bounds/pull/3421) bound `B` +and `A` for the selected m=73 complex producer: + +```text +sigma <= (43/26)*(1-s)*(A+B) + rho, A = 0, B = 2642 +``` + +That leaves `rho`, the leaf reserve, as the only unbound term. This package +traces every non-complex term of the selected row ledger to its source. It +shows that those terms cannot serve as `rho`, and reduces `rho` to a named +two-way missing lemma. Both branches pass the native stage-1 fit guard. + +```sh +python3 -I -B research/selected-stock-rho-ledger/verify.py +``` + +Expected: + +```text +PASS_SELECTED_STOCK_RHO_LEDGER B=2642 ledger=16469 9909=367*27 252=9*28 1024=2*512 bit_row=18355=8194+9909+252 implicit_rho_3113=11185 rho_a=0 sigma_a<=4362.14 rho_b=8194 sigma_b<=12556.14 guard=16,17<=6562783 controls=10 checks=42 +``` + +Python 3.12 standard library, under one second. The verifier authenticates +every live input listed in [SOURCES.json](SOURCES.json). It reads three +members of the pinned PR1087 tarball in memory; its `code/assemble.py` hash is +the one `selected-bootstrap-stock-audit` pins. Every constant is parsed from +source text, not typed in. Nothing from the repository is imported or executed. + +## Source facts + +1. **The selected ledger.** Frozen PR1087 `code/assemble.py` asserts the + ledger `2*stock.bit_length()+9909+252+1024`, which gives 16469. It also + asserts the retained cap `20161` and the external degree gap + `10^6 - (51/25)*20161`. That gap is the selected `ASSEMBLY.json` + `outer.row_product_gap = 23971789/25`. +2. **9909 and 252 are historical family charges.** + `notes/partial-gauge-assembly.tex` gives the "coarse bit, ordinary leaf and + complex families" the (halving degree, wire bits) pairs `(367,27)`, + `(9,28)` and `(200,28)`. Hence `9909 = 367·27` and `252 = 9·28`. Later + assembly notes carry them forward unchanged as "conservative previous bit + and ordinary-leaf reserves" (`58344+9909+252`, `10284+9909+252`). The + 367-level coarse-bit family is not the selected PR589 BIT producer, whose + halving depth is 2. +3. **1024 is the prefix term.** `invoice_allcold.py` sets + `row_prefix_extra = 2*payload`, and `charged_prefix_bits = 512`. +4. **The selected BIT ledger stacks the same constants.** PR510's + `assemble9.py` computes `row = DEPTH*(m*m+1)+9909+252 = 18355`. With + PR589's `nine.bit` record (m=64, maximum child 42, 28,425 physical roles, + halving depth 2), the BIT family's own term is `2·(64²+1) = 8194`. That is + the coefficient + [PR2084](https://github.com/CrocSwap/integer-mult-bounds/pull/2084) + (`research/selected-bit-parent-reserve`) proves conditionally. PR2084 + already reads this formula and argues that the other outer allowances do + not enter the BIT sigma. That BIT-side observation is not new here. +5. **The two stocks have different units.** The assembly notes define a row + coefficient as the degree of a **fixed external polynomial reserve**: + `log2 Q <= (51/25)·K·log2 p`, and `p^(10^6)` for the selected assembly. + They state that the width-dependent q-adic selector stock is "supplied by + the separate internal borrowing proof, rather than multiplied into this + external polynomial stock". H3, + `log_q S(e,w) <= sigma·w·(1+log2 e)` with `k < e/2`, constrains that + internal borrowed stock. + +## What follows for `rho` + +- #3113's conditional readings sigma ≈ 16469 or 15555 put the external-ledger + constants `9909 + 252 + 1024 = 11185` into the borrowed-stock envelope. The + verifier reproduces `15555 − ⌈43·2642/26⌉ = 11185`. Those constants are + w-free degrees of an external reserve, and 9909 belongs to a historical + family. So the ledger does not supply a source-bound `rho`. The control + `ledger_constant_as_rho` rejects 9909 as a w-free bound on the w-shaped BIT + term, because `9909 < 8194·w` for every `w >= 2`. +- **Reading (a): completed leaves.** If every BIT/ordinary callee inside an + m=73 node is a completed call that borrows internally and restores (PR2084 + hypothesis 4, the reviewed PR185 contract), then the external `S_leaf = 1`. + `selected-coarse-depth-stock/PROOF.md` already allows this conditionally. + Then `rho = 0` and, at native stage 1, + `sigma <= (43/26)(1-s)·2642 ≈ 4362.14`, with `ceil(log2(8·sigma)) = 16`. +- **Reading (b): the parent reserves the BIT factor.** This is the mode + `structured-bulk-assembly.tex` describes: "Both factors are reserved + simultaneously". Then `rho` must dominate the BIT stock's w-shaped + coefficient. Conditionally on PR2084 that gives `rho = 8194` and + `sigma <= 12556.14`, with guard 17. Sequential callees reuse restored rows, + and PR2084's envelope is monotone in `e` and `w`, so the maximum over + callees suffices. This composition is stated, not independently proved. +- Both branches sit far below the stage-1 sufficient guard `H_1 = 6,562,783`. + So the open obligation is which reading the selected construction actually + realizes, not headroom. + +## Controls + +Each of these must be rejected: + +1. A flipped byte in a pinned input. +2. A ledger constant changed to 9908. +3. The family wire bits changed to 28. +4. `Sp(70,2)` in place of `Sp(72,2)`. +5. A prefix extra of 2048. +6. The eleven-stage BIT record. +7. A tampered `row_product_gap`. +8. 9909 used as a w-free `rho`. +9. The `S_leaf=1` premise removed. +10. A guard set below sigma. + +## Not claimed + +No supplier, κ, cutoff, frontier or selected-record change. Only native +stage 1 is checked. Neither reading is shown to be the one the selected +lowering realizes. The PR2084 coefficient is used as that package's +conditional result, not re-derived. The composition in reading (b) is a +stated argument, not a proved lemma. This is a finite source-bound audit, +not a supplier replay or a multiplication theorem. Overlap was checked +against open and closed PRs, package READMEs and Discussion titles; I didn't +search Discussion bodies. + +## Open next questions + +The structured versions are in [TASK.json](TASK.json). + +1. **Which reading holds?** Inside selected m=73 nodes, is each BIT callee a + completed call, or does the parent reserve its factor? This decides + between `rho = 0` and `rho >= sigma_BIT`. First step: classify the + adapter and peeled-atom call sites in the PR1094 source manifest. Blocked + by: no pinned sentence names the reservation mode for selected m=73 + adapters. +2. **All fourteen stages.** Repeat the guard comparison for native stages + 2–7 and the conservative branch, using each stage's own `s` and headroom. + This is bounded arithmetic once question 1 is settled. +3. **Is the external ledger still source-bound?** The term 9909 was derived + for a fixed-wire historical family. If the selected BIT digit tower had to + sit in the external reserve, that term would not be bound to the selected + producer. First step: trace where the selected assembler routes PR589's + q-adic selector stock. + +## Credit + +- Aaron Wang (#3113, `selected-stock-envelope-m73`) bound `B = 2642` and + stated the missing `A, B, rho` lemma. +- Wentao Li (#3421, `selected-stock-shape-a-zero`) proved `A = 0`. +- Sricharan Vagvala (#2105, `selected-coarse-depth-stock`) supplied the + `43/26` depth rate, the composition formula and the conditional + `S_leaf = 1` sentence. +- Adam Gall (PR2084, `selected-bit-parent-reserve`) supplied the conditional + BIT coefficient 8194, its completed-leaf hypothesis and the BIT-side reading + of the 18355 formula. +- Josie Elliston (PR1965) and ToikY (`selected-bootstrap-stock-audit`) + supplied the stage receipt and guard. +- Jeremy Kothe (PR1087) and Rohan Arun (PR1094) supplied the selected + assembler and invoice. The partial-gauge, three-stage, paired-cube and + structured-bulk assembly notes keep their original attribution. + +Prepared by Mainzu, with substantial Claude Code (Anthropic) assistance. No +independent human review is claimed. Apache-2.0. diff --git a/research/selected-stock-rho-ledger/SOURCES.json b/research/selected-stock-rho-ledger/SOURCES.json new file mode 100644 index 0000000000..ca73ef8fc9 --- /dev/null +++ b/research/selected-stock-rho-ledger/SOURCES.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "notes/paired-cube-assembly.tex", + "usage": "input", + "git_blob": "d44227eb55ab68b9d04ea661bbe486fea66182d4", + "sha256": "45f28775ebf36338df9312957fd09af3c635690acc02ae3d60431ccd16fb46c3" + }, + { + "path": "notes/partial-gauge-assembly.tex", + "usage": "input", + "git_blob": "4a09f324a3fe8a3c2397f34244b5cedebeb95a7c", + "sha256": "ef27afc3a70656d3139bf3661ac0b2088622f37221141cc386d41324b7c563d0" + }, + { + "path": "notes/structured-bulk-assembly.tex", + "usage": "input", + "git_blob": "9bd11d88d201d6aa7b110bc169648d928c3a9c14", + "sha256": "048c67f6473ee4712d37033266a2e507dee9dcd2bb3b0fd177708100e2404d94" + }, + { + "path": "notes/three-stage-cover-assembly.tex", + "usage": "input", + "git_blob": "983ffb6ac8fb9117360cd0797c00c05dfa071c9d", + "sha256": "ccf34a6d37c4af14bebeab15be50ab204eb1caebe546385520050ec30089441d" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "usage": "input", + "git_blob": "2970ef79b0441e937449bed30f68f2e0558186ba", + "sha256": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "usage": "input", + "git_blob": "238226c568742dd5723b03eabae564a2eaa2bda9", + "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" + }, + { + "path": "research/selected-bit-parent-reserve/README.md", + "usage": "input", + "git_blob": "86dacf2f68b8e2127c8f6fe87fb98fd71ef1f422", + "sha256": "16b84730b7a604e805034008e11bae4f90fe6c91db6098d5bd5d011dded5f4ee" + }, + { + "path": "research/selected-bootstrap-stock-audit/RESULT.json", + "usage": "input", + "git_blob": "2826e072d4644b61b55ffbf322447513ed66f45d", + "sha256": "f0bd4f2270826de7b935323e9b4d2e034f69b46205be9535488c4429e95f7917" + }, + { + "path": "research/selected-coarse-depth-stock/PROOF.md", + "usage": "input", + "git_blob": "e0854d3afd012f7413147bd927812467843aca77", + "sha256": "fe1a29b3757a3fda7124027e7e14228a6f3aa49521e23822909036172807f800" + }, + { + "path": "research/selected-stock-envelope-m73/README.md", + "usage": "input", + "git_blob": "9c950560a82eb5747601768beab2474b6dd5e954", + "sha256": "efede1e472e45f78baf304da6bff7b6685b6bb4ae06cf6a1ea9d1ceaf6fd3b88" + }, + { + "path": "research/selected-stock-shape-a-zero/PROOF.md", + "usage": "input", + "git_blob": "c70ec691b5f3370bd95ae5e18a025659aebda3e3", + "sha256": "e2ce357464afc8f40fde33416f567c110750cced23b09856dbb9a8252b7f7bf9" + } + ] +} diff --git a/research/selected-stock-rho-ledger/TASK.json b/research/selected-stock-rho-ledger/TASK.json new file mode 100644 index 0000000000..ff4d1e7d25 --- /dev/null +++ b/research/selected-stock-rho-ledger/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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", + "research/stock-margin-chain/README.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 #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "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 actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.", + "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.", + "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990", + "2972", + "stock-margin-chain", + "actual_stock_coefficient" + ], + "existing_checks": [ + { + "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.", + "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation", + "remaining": "Derive one actual reserve/depth coefficient from the selected producer.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Source-bind the non-complex terms of the selected m=73 row ledger (9909, 252, 1024) and decide whether they bind the leaf reserve rho in sigma <= (43/26)(1-s)(A+B) + rho at native stage 1.", + "scope_change_reason": "The card asks for an explicit envelope. #3113 and #3421 bound B and A for the m=73 producer and left rho as the only unbound term; this package addresses only rho, at native stage 1, and ends at a named two-way missing lemma rather than one admitted envelope.", + "bottleneck_link": "Inherited implementation obligation (H3 stock fit) for the selected result; it changes no supplier, kappa or cutoff. It prevents an external-ledger constant from being counted as a proved borrowed-stock coefficient.", + "budget_minutes": 90, + "stop_rule": "Stop once each ledger term is bound to source and rho is reduced to a named dichotomy with both branches checked against the stage-1 guard; do not attempt the completed-leaf implementation proof or other stages.", + "outcome": "partial", + "evidence": "verify.py: 42 exact checks over 13 pinned inputs plus three PR1087 tarball members, and 10 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... controls=10 checks=42.", + "author": "Mainzu", + "ai_assistance": "Substantial assistance from Claude Code (Anthropic, Claude Opus 5.5) for source search, the verifier and drafting; no independent human review is claimed.", + "open_questions": [ + { + "question": "Inside selected m=73 nodes, is every BIT callee a completed ordinary call with internal borrowing, or does the parent reserve the BIT factor (structured-bulk: 'Both factors are reserved simultaneously')?", + "why_it_matters": "It decides rho = 0 (sigma <= 4362.14) versus rho >= sigma_BIT (w-shaped; 8194 under PR2084), i.e. which conditional envelope the outer proof may cite.", + "first_step": "Locate the selected complex construction's adapter/peeled-atom call sites in the PR1094 source manifest and classify each as completed-call or parent-reserved.", + "blocked_by": "The selected complex lowering is inherited; no pinned sentence names the reservation mode for selected m=73 adapters." + }, + { + "question": "Do reading (a) and reading (b) also pass at native stages 2-7 and the seven conservative stages?", + "why_it_matters": "This package checks only native stage 1; the outer proof needs all fourteen recorded stages.", + "first_step": "Repeat section 9 of verify.py for every stage record in selected-bootstrap-stock-audit/RESULT.json using its own s and stock_headroom_log2.", + "blocked_by": "Nothing technical; it is bounded arithmetic once question 1's reading is fixed." + }, + { + "question": "Is the external polynomial reserve itself (degree 16469 < 20161, p^(10^6)) still sufficient for the selected BIT family, whose divisor has a w-dependent digit tower?", + "why_it_matters": "9909 was derived for a historical coarse-bit family with fixed 27-bit wires; if the selected BIT tower must sit in the external reserve, that ledger term is not source-bound to the selected producer.", + "first_step": "Trace where the selected assembler routes PR589's q-adic selector stock: external ledger or internal borrowing (three-stage-cover-assembly.tex states the latter for the historical families).", + "blocked_by": "Same inherited lowering as question 1." + } + ] +} diff --git a/research/selected-stock-rho-ledger/VERIFY.json b/research/selected-stock-rho-ledger/VERIFY.json new file mode 100644 index 0000000000..fa70cb9301 --- /dev/null +++ b/research/selected-stock-rho-ledger/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/paired-cube-assembly.tex", + "notes/partial-gauge-assembly.tex", + "notes/structured-bulk-assembly.tex", + "notes/three-stage-cover-assembly.tex", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "research/selected-bit-parent-reserve/README.md", + "research/selected-bootstrap-stock-audit/RESULT.json", + "research/selected-coarse-depth-stock/PROOF.md", + "research/selected-stock-envelope-m73/README.md", + "research/selected-stock-shape-a-zero/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticates all live inputs and three tarball members by SHA-256; parses the selected ledger, family pairs, prefix payload, PR589 record and stage-1 receipt; 42 exact checks; 10 mutation controls (tampered byte, ledger constant, family wire bits, Sp(70,2), prefix extra, eleven-stage BIT record, row gap, w-free constant as rho, missing S_leaf premise, guard below sigma) must each be rejected." + } + ] +} diff --git a/research/selected-stock-rho-ledger/verify.py b/research/selected-stock-rho-ledger/verify.py new file mode 100644 index 0000000000..32b4d4cb4a --- /dev/null +++ b/research/selected-stock-rho-ledger/verify.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +"""Source-bound audit of the selected m=73 row-ledger terms behind `rho`. + +Standard library only. Reads the pinned live inputs named in SOURCES.json +(and three members of the pinned PR1087 tarball, in memory); nothing from the +repository is imported or executed. Every proof-relevant constant is parsed +from source text, then checked by exact integer/rational arithmetic. Ten +mutation controls must each be rejected. + +Mainzu, with substantial Claude Code assistance. Apache-2.0. +""" +import copy +import hashlib +import io +import json +import re +import sys +import tarfile +from fractions import Fraction as F +from pathlib import Path + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +TARBALL = "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz" +MEMBERS = { # member -> sha256 (the assemble.py pin matches selected-bootstrap-stock-audit) + "code/assemble.py": "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a", + "code/invoice_allcold.py": "71eb57514e28ced97251e0507105f654f59885ec4d40486a780bf166098858a8", + "inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", +} +MARKER = "PASS_SELECTED_STOCK_RHO_LEDGER" +DEFAULTS = dict(sp_half=36, bit_record="nine", rho_b=None, h1_override=None) + + +class Reject(Exception): + pass + + +def need(cond, what): + if not cond: + raise Reject(what) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def flat(text): + return " ".join(text.split()) + + +def load_raw(): + sources = json.loads((PKG / "SOURCES.json").read_text(encoding="utf-8")) + pins = {r["path"]: r["sha256"] for r in sources["files"] if r["usage"] == "input"} + return pins, {p: (ROOT / p).read_bytes() for p in pins} + + +def authenticate(pins, raw): + for path, digest in pins.items(): + need(sha(raw[path]) == digest, "pin mismatch: " + path) + with tarfile.open(fileobj=io.BytesIO(raw[TARBALL])) as tar: + names = {m.name.lstrip("./"): m for m in tar.getmembers() if m.isfile()} + members = {k: tar.extractfile(names[k]).read() for k in MEMBERS} + for k, digest in MEMBERS.items(): + need(sha(members[k]) == digest, "member mismatch: " + k) + texts = {p: b.decode("utf-8") for p, b in raw.items() if p != TARBALL} + texts.update({"tar:" + k: b.decode("utf-8") for k, b in members.items()}) + return texts + + +def ceil_log2(x): + """Least integer g with 2**g >= x, for rational x > 0.""" + g = max(x.numerator.bit_length() - x.denominator.bit_length() - 1, 0) + while F(2) ** g < x: + g += 1 + return g + + +def analyse(t, p): + n = [0] + + def ok(cond, what): + need(cond, what) + n[0] += 1 + + asm, inv = t["tar:code/assemble.py"], t["tar:code/invoice_allcold.py"] + + # 1. The selected complex ledger as the frozen assembler states it. + m = re.search(r"finite\['physical_row_coefficient'\]==2\*stock\.bit_length\(\)\+(\d+)\+(\d+)\+(\d+)", asm) + ok(m is not None, "selected ledger formula") + c_bit, c_leaf, c_prefix = map(int, m.groups()) + ok("finite['retained_row_coefficient']==20161" in asm, "retained row cap 20161") + ok("'degree_gap':Q(10**6)-Q(51*20161,25)" in asm, "external p^(10^6) degree gap") + gap = json.loads(t["research/community-frontier1094-audit/ASSEMBLY.json"])["outer"]["row_product_gap"] + ok(F(gap) == F(10 ** 6) - F(51 * 20161, 25), "selected ASSEMBLY row_product_gap") + + # 2. Prefix term = twice the charged prefix payload. + pay = re.search(r"invoice\['charged_prefix_bits'\]==(\d+)", asm) + extra = re.search(r"invoice\['row_prefix_extra'\]==(\d+)", asm) + ok(pay is not None and extra is not None, "prefix fields") + ok("row=2*stock.bit_length()+9909+252+2*payload" in inv, "invoice ledger uses 2*payload") + ok("charged_prefix_bits=payload" in inv and "row_prefix_extra=2*payload" in inv, "invoice prefix binding") + ok(c_prefix == int(extra.group(1)) == 2 * int(pay.group(1)), "prefix term = 2*payload") + + # 3. B = bit length of |Sp(2h,2)| times the 14,826 physical families. + h = p["sp_half"] + order = 2 ** (h * h) + for j in range(1, h + 1): + order *= 2 ** (2 * j) - 1 + fam = re.search(r"data_and_owner_families=(\d+),local_helpers=R,private_centres=(\d+),coefficient_work=(\d+)", asm) + ok(fam is not None, "physical stock identity") + families = int(fam.group(1)) + 480 + int(fam.group(2)) + int(fam.group(3)) + ok("families=14826" in t["research/selected-stock-envelope-m73/README.md"] and families == 14826, "14826 families") + b_bits = (order * families).bit_length() + ok(b_bits == 2642, "B = 2642 bits") + ledger = 2 * b_bits + c_bit + c_leaf + c_prefix + ok(ledger == 16469 < 20161, "physical ledger 16469 < 20161") + + # 4. Origin of 9909 and 252: historical (halving degree, wire bits) families. + pg = flat(t["notes/partial-gauge-assembly.tex"]) + ok("The coarse bit, ordinary leaf and complex families" in pg, "family sentence") + pairs = re.search(r"\$\((\d+),(\d+)\),\((\d+),(\d+)\),\((\d+),(\d+)\)\$", pg) + ok(pairs is not None, "family pairs") + (hb, wb, hl, wl, hc, wc) = map(int, pairs.groups()) + ok(f"{hb}\\cdot{wb}+{hl}\\cdot{wl}+{hc}\\cdot{wc}={hb*wb+hl*wl+hc*wc}" in pg, "family sum as printed") + ok(c_bit == hb * wb, "9909 = coarse-bit family degree x wire bits") + ok(c_leaf == hl * wl, "252 = ordinary-leaf family degree x wire bits") + tsc = flat(t["notes/three-stage-cover-assembly.tex"]) + ok("conservative previous bit and ordinary-leaf reserves" in tsc, "carried as conservative reserves") + ok(f"58344+{c_bit}+{c_leaf}=68505" in tsc, "carried forward (three-stage)") + ok(f"10284+{c_bit}+{c_leaf}=20445" in flat(t["notes/paired-cube-assembly.tex"]), "carried forward (paired-cube)") + + # 5. Units: external polynomial reserve degree vs internal q-adic borrowing. + ok("width-dependent q-adic selectors are supplied by the separate internal borrowing proof, " + "rather than multiplied into this external polynomial stock" in tsc, "selectors internal (three-stage)") + ok("selector stock is borrowed and restored internally, not multiplied into this external " + "polynomial reserve" in flat(t["notes/paired-cube-assembly.tex"]), "selectors internal (paired-cube)") + sb = flat(t["notes/structured-bulk-assembly.tex"]) + ok("\\log_2Q\\le\\frac{51}{25}K\\log_2p" in sb, "row coefficient is a log2 Q / log2 p degree") + ok("Both factors are reserved simultaneously" in sb, "bit-adapter factor reserved with complex factor") + + # 6. Selected BIT (PR589) ledger stacks the same constants (PR2084's reading). + ok("bit=bit_record['nine']" in asm, "assembler consumes the nine-stage BIT record") + rec = json.loads(t["tar:inputs/PR589-EXPECTED.json"])[p["bit_record"]]["bit"] + ok(rec["maxchild"] == 42 and rec["physical"] == 28425, "PR589 m=64 producer identity") + a9 = t["research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py"] + f9 = re.search(r"row = DEPTH \* \(m \* m \+ 1\) \+ (\d+) \+ (\d+); assert row == (\d+)", a9) + ok(f9 is not None, "PR510 assemble9 row formula") + ok((int(f9.group(1)), int(f9.group(2))) == (c_bit, c_leaf), "BIT ledger reuses 9909 and 252") + hd = rec["halving_depth"] + ok(64 ** hd > 2 * rec["maxchild"] ** hd and 64 ** (hd - 1) <= 2 * rec["maxchild"] ** (hd - 1), "least halving depth") + sigma_bit = hd * (64 * 64 + 1) + ok(rec["row_coefficient"] == int(f9.group(3)) == sigma_bit + c_bit + c_leaf, "BIT row = HD(m^2+1)+9909+252") + pr2084 = flat(t["research/selected-bit-parent-reserve/README.md"]) + ok(f"2*(64^2+1)={sigma_bit}" in pr2084, "PR2084 sigma_BIT") + ok("needs **no additional externally supplied row factor**" in pr2084, "PR2084 hypothesis 4") + + # 7. Predecessor statements this package composes. + cd = flat(t["research/selected-coarse-depth-stock/PROOF.md"]) + ok("one may take S_leaf=1" in cd, "coarse-depth: S_leaf=1 admissible under completed leaves") + ok("sigma <= (43/26)*(1-s)*(A+B) + rho." in cd, "coarse-depth composition formula") + ok("**A = 0** and **B = 2642**" in t["research/selected-stock-shape-a-zero/PROOF.md"], "PR3421 A=0, B=2642") + m73 = t["research/selected-stock-envelope-m73/README.md"] + ok("ledger=16469->15555" in m73 and "Under either conditional ledger reading" in m73, "#3113 ledger readings") + implicit = 15555 - -(-43 * b_bits // 26) + ok(implicit == c_bit + c_leaf + c_prefix == 11185, "#3113's 15555 reading carries 11185 as rho") + + # 8. Native stage 1 from the audited receipt. + br = json.loads(t["research/selected-bootstrap-stock-audit/RESULT.json"])["branches"]["bootstrap"] + s = F(br["common_saving"]) + st1 = br["stages"][0] + ok(st1["stage"] in (1, "1") and st1["actual_stock_coefficient"] is None, "stage-1 record, coefficient null") + h1 = int(st1["stock_headroom_log2"]) if p["h1_override"] is None else p["h1_override"] + ok(0 < s < 1, "0 < s < 1") + + # 9. The two readings of rho, and why the ledger constant is not one. + base = F(43, 26) * (1 - s) * b_bits # complex part with A = 0 + # A candidate is (coefficient, shape): "w" multiplies w*(1+log2 e) as in H3; + # "free" multiplies only ceil(log2 e), as every external-ledger degree does. + rho_b, shape = (sigma_bit, "w") if p["rho_b"] is None else p["rho_b"] + if shape == "w": + ok(rho_b >= sigma_bit, "reading (b) rho must dominate the w-shaped BIT coefficient") + else: + ok(all(rho_b >= sigma_bit * w for w in range(1, 4097)), "w-free rho must dominate 8194*w at every w") + ok(all(c_bit < sigma_bit * w for w in range(2, 4097)), "9909 < 8194*w for every w >= 2 probed") + sigma_a, sigma_b = base, base + rho_b + g_a, g_b = ceil_log2(8 * sigma_a), ceil_log2(8 * sigma_b) + ok(g_a <= h1 and g_b <= h1, "sufficient guard ceil(log2(8 sigma)) <= H_1") + return dict(checks=n[0], b=b_bits, ledger=ledger, c=(c_bit, c_leaf, c_prefix), fam=(hb, wb, hl, wl), + bit_row=rec["row_coefficient"], sigma_bit=sigma_bit, implicit=implicit, + sigma_a=sigma_a, sigma_b=sigma_b, g=(g_a, g_b), h1=h1) + + +def controls(pins, raw, texts): + def text_edit(key, old, new): + def run(): + t = dict(texts) + need(old in t[key], "control precondition: " + old) + t[key] = t[key].replace(old, new) + analyse(t, DEFAULTS) + return run + + def param(**kw): + return lambda: analyse(texts, {**DEFAULTS, **kw}) + + def tamper(): + r = copy.copy(raw) + k = "notes/partial-gauge-assembly.tex" + r[k] = r[k][:-1] + bytes([r[k][-1] ^ 1]) + authenticate(pins, r) + + asm, pg = "tar:code/assemble.py", "notes/partial-gauge-assembly.tex" + cases = { + "tampered_input_byte": tamper, + "ledger_constant_9908": text_edit(asm, "+9909+252+1024", "+9908+252+1024"), + "family_wire_bits_28": text_edit(pg, "(367,27)", "(367,28)"), + "sp70_instead_of_sp72": param(sp_half=35), + "prefix_extra_2048": text_edit(asm, "invoice['row_prefix_extra']==1024", "invoice['row_prefix_extra']==2048"), + "eleven_stage_bit_record": param(bit_record="eleven"), + "row_gap_tampered": text_edit("research/community-frontier1094-audit/ASSEMBLY.json", + '"row_product_gap": "23971789/25"', '"row_product_gap": "23971790/25"'), + "ledger_constant_as_rho": param(rho_b=(9909, "free")), + "missing_s_leaf_premise": text_edit("research/selected-coarse-depth-stock/PROOF.md", + "one may take S_leaf=1", "one may take S_leaf=2"), + "guard_below_sigma": param(h1_override=15), + } + for name, run in cases.items(): + try: + run() + except Reject: + continue + raise SystemExit("CONTROL ACCEPTED (must reject): " + name) + return len(cases) + + +def main(): + pins, raw = load_raw() + texts = authenticate(pins, raw) + r = analyse(texts, DEFAULTS) + k = controls(pins, raw, texts) + print(f"{MARKER} B={r['b']} ledger={r['ledger']} " + f"{r['c'][0]}={r['fam'][0]}*{r['fam'][1]} {r['c'][1]}={r['fam'][2]}*{r['fam'][3]} " + f"{r['c'][2]}=2*{r['c'][2] // 2} bit_row={r['bit_row']}={r['sigma_bit']}+{r['c'][0]}+{r['c'][1]} " + f"implicit_rho_3113={r['implicit']} rho_a=0 sigma_a<={float(r['sigma_a']):.2f} " + f"rho_b={r['sigma_bit']} sigma_b<={float(r['sigma_b']):.2f} " + f"guard={r['g'][0]},{r['g'][1]}<={r['h1']} controls={k} checks={r['checks']}") + + +if __name__ == "__main__": + try: + main() + except Reject as exc: + sys.exit("FAIL: " + str(exc)) From b20c4c1dcc5e35c6b49229856d43ea602ca446cf Mon Sep 17 00:00:00 2001 From: Mainzu <107363567+Mainzu@users.noreply.github.com> Date: Sun, 18 Oct 2026 21:43:35 +0700 Subject: [PATCH 2/5] Settle rho for the selected m=73 layer; check all fourteen stages Read the selected complex chain (PR2287/PR3385, PR2250, PR2234, PR2899): the layer's only row stock is its own divisor L^D0(d), its compact fields are not row stock, its peeled axes and leaves are elementary, and its only BIT callee borrows internally. So S_leaf = 1 and rho = 0, conditionally on that chain. The structured-bulk "reserved simultaneously" sentence concerns fixed-wire external factors. Also check both values against all fourteen stage guards, show the 9909/252 row slots are slack in the selected layer, and show the q-adic BIT's stock cannot sit in the 20161 row cap. Partial; no new kappa. 62 checks, 16 mutation controls. Co-Authored-By: Claude Opus 5.5 --- research/selected-stock-rho-ledger/README.md | 184 ++++++++++++++---- .../selected-stock-rho-ledger/SOURCES.json | 36 ++++ research/selected-stock-rho-ledger/TASK.json | 32 +-- .../selected-stock-rho-ledger/VERIFY.json | 5 +- research/selected-stock-rho-ledger/verify.py | 93 ++++++++- 5 files changed, 287 insertions(+), 63 deletions(-) diff --git a/research/selected-stock-rho-ledger/README.md b/research/selected-stock-rho-ledger/README.md index d63a461b67..aad1e64d72 100644 --- a/research/selected-stock-rho-ledger/README.md +++ b/research/selected-stock-rho-ledger/README.md @@ -11,8 +11,11 @@ sigma <= (43/26)*(1-s)*(A+B) + rho, A = 0, B = 2642 That leaves `rho`, the leaf reserve, as the only unbound term. This package traces every non-complex term of the selected row ledger to its source. It -shows that those terms cannot serve as `rho`, and reduces `rho` to a named -two-way missing lemma. Both branches pass the native stage-1 fit guard. +shows that those terms cannot serve as `rho`. It then reads the merged +selected complex layer to settle how its callees get their stock: the layer's +only row stock is its own divisor, so `S_leaf = 1` and `rho = 0`. This holds +conditionally on that chain. All fourteen recorded stage guards pass either +way. ```sh python3 -I -B research/selected-stock-rho-ledger/verify.py @@ -21,7 +24,7 @@ python3 -I -B research/selected-stock-rho-ledger/verify.py Expected: ```text -PASS_SELECTED_STOCK_RHO_LEDGER B=2642 ledger=16469 9909=367*27 252=9*28 1024=2*512 bit_row=18355=8194+9909+252 implicit_rho_3113=11185 rho_a=0 sigma_a<=4362.14 rho_b=8194 sigma_b<=12556.14 guard=16,17<=6562783 controls=10 checks=42 +PASS_SELECTED_STOCK_RHO_LEDGER B=2642 ledger=16469 9909=367*27 252=9*28 1024=2*512 bit_row=18355=8194+9909+252 implicit_rho_3113=11185 rho_a=0 sigma_a<=4362.14 rho_b=8194 sigma_b<=12556.14 L_bits=2642 S_leaf=1 guard=16,17<=6562783 stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62 ``` Python 3.12 standard library, under one second. The verifier authenticates @@ -64,6 +67,33 @@ source text, not typed in. Nothing from the repository is imported or executed. external polynomial stock". H3, `log_q S(e,w) <= sigma·w·(1+log2 e)` with `k < e/2`, constrains that internal borrowed stock. +6. **The selected complex layer's only row stock is its own divisor.** Jose + Manuel's PR2287 (`selected-complex-layer-closure/PROOF.md`) is the written + all-size m=73 layer. PR3385 implements it physically; that archive has had + intake checks only, with no scientific verifier run. PR2287 sets + `W = 14336` and `L = W·|O(73,2)|`. Its only row stock is `L^D0(d)`, taken + from a prefix of `q0 = ceil(log2 L)·D0(d)` chunks. A child receives `U` + with `L^D0(e') | U`, and "a completed child restores its own row labels". + - **Peeled axes and stopped leaves.** The layer processes the + `e mod 73` leftmost axes individually, and "the leaves require only the + elementary C kernel". These calls have no callee and need no stock. + - **Compact fields.** The root also reserves `qF + qB` chunks for three + H-bit compact fields (`H = dG`, `G = 4⌈log2 p⌉ + 6`). They may start + dirty, and the adapters restore them. "No compact-field bit enters this + selector", so they are not row stock and lie outside A, B and `rho`. + - **Ordinary/BIT calls.** The only ones sit inside PR2250's compact + adapters, which run them on `(f-1)G`-bit pieces of the compact fields. + PR2287 says its bound uses "an ordinary binary chunk interchange … + PR2234 proposes that contract". PR2250 grants that callee "no external + row stock or ancestor access". PR3385 binds it to B1/C0 (L17–19). + - **The callee's own stock.** PR2234 §8 (realized physically as B1 in + PR2899) chooses its own stock `S=K(w)^D(e)` with `log_q K <= 4097w`. It + borrows `k=ceil(log_q S)` leading digits of its own chunk, so inside the + compact-field piece it was given. Below the fitted range it falls back to + elementary interchanges. With halving + depth 2 that stock is exactly PR2084's `8194` coefficient. + - **The divisor matches B.** `ceil(log2(14336·Γ)) = 2642`, the same as + #3113's B. The divisor is w-free, consistent with #3421's `A = 0`. ## What follows for `rho` @@ -74,22 +104,59 @@ source text, not typed in. Nothing from the repository is imported or executed. family. So the ledger does not supply a source-bound `rho`. The control `ledger_constant_as_rho` rejects 9909 as a w-free bound on the w-shaped BIT term, because `9909 < 8194·w` for every `w >= 2`. -- **Reading (a): completed leaves.** If every BIT/ordinary callee inside an - m=73 node is a completed call that borrows internally and restores (PR2084 - hypothesis 4, the reviewed PR185 contract), then the external `S_leaf = 1`. - `selected-coarse-depth-stock/PROOF.md` already allows this conditionally. - Then `rho = 0` and, at native stage 1, +- **Reading (a), completed callees, is what the selected layer does.** Every + callee inside an m=73 node is either elementary or a completed ordinary call + that borrows internally and restores (fact 6). So `S_leaf = 1`, as + `selected-coarse-depth-stock/PROOF.md` already allowed conditionally. Then + `rho = 0` and, at native stage 1, `sigma <= (43/26)(1-s)·2642 ≈ 4362.14`, with `ceil(log2(8·sigma)) = 16`. -- **Reading (b): the parent reserves the BIT factor.** This is the mode - `structured-bulk-assembly.tex` describes: "Both factors are reserved - simultaneously". Then `rho` must dominate the BIT stock's w-shaped - coefficient. Conditionally on PR2084 that gives `rho = 8194` and - `sigma <= 12556.14`, with guard 17. Sequential callees reuse restored rows, - and PR2084's envelope is monotone in `e` and `w`, so the maximum over - callees suffices. This composition is stated, not independently proved. -- Both branches sit far below the stage-1 sufficient guard `H_1 = 6,562,783`. - So the open obligation is which reading the selected construction actually - realizes, not headroom. +- **Reading (b), the parent reserving the BIT factor, is kept only as a + counterfactual.** An earlier version cited `structured-bulk-assembly.tex`'s + "Both factors are reserved simultaneously" for it. That sentence concerns + fixed-wire *external* factors (`W_b,W_c<2^{43}`, bounded in `p^{108000}`), + the kind the selected ledger pays as 9909. It is not the w-shaped BIT + stock. If a parent did reserve that stock, `rho` would have to dominate + PR2084's 8194. That gives `sigma <= 12556.14` with guard 17, which still + passes. +- **All fourteen recorded stages pass both values.** That is native stages + 1–7 and conservative stages 1–7, each with its branch's own `s` and its own + headroom. For each stage record, the verifier re-derives + `H_j = floor(L_j·gap_j/2) − 4` from the recorded `L_j` and gap. It checks + that the gap is the least of the four recorded gaps, that the stock gap is + `1 − s`, and PR1965's premises (`L ≥ 2`, `L·gap² ≥ 36`, + `0 < gap ≤ 1 − s`). The tightest stage is stage 1 + in both branches, at `H = 6,562,783`. The guards are only 16 and 17. + +## What the 9909 and 252 slots pay for + +The selected certificate charges the complex row +`2·2642 + 9909 + 252 + 1024 = 16469`. Separately, it charges the BIT row +`8194 + 9909 + 252 = 18355`. Both are checked against one cap, 20161 +(`assemble.py` L159, L173, L204). + +- **No selected family has the 9909 or 252 parameters.** The selected BIT + is halving depth 2 with `64²+1` bits, giving 8194. The selected complex + layer's peeled axes and leaves are elementary C kernels (fact 6). The pairs + `(367,27)` and `(9,28)` are historical families. +- **In the selected layer, the two slots pay for nothing.** Its only row + stock is `L^D0(d)`, and its BIT callee borrows internally. Without the + slots, the complex row is `2·2642 + 1024 = 6308`, so they are inherited + slack. Dropping them would not change κ: the physical row only has to stay + below the retained 20161, and only that retained cap enters the outer + assembly, through the strict degree-gap constraint. +- **The BIT's 8194 here is a binary model.** The certificate's 8194 is + PR510's model of the BIT, with `m²+1` bits per level. In that model, 8194 + would fit in the 9909 slot (`6308 + 8194 + 252 = 14754 < 20161`), so the + cap check alone decides nothing about how the BIT gets its stock. +- **The BIT the adapters call is q-adic, and its stock cannot fit the + cap.** The adapters call PR2234's BIT, which has `q > 2^80`. Its level + divisor has at least `4096·80 − 2` bits, because + `|GL_64(F_q)| ≥ q^4096/2`. In the certificate's own row convention + (halving depth × bits per level), that gives a row term of at least + `2·(4096·80 − 2) = 655,356` at `w = 1`. That is over 32 times the 20161 + cap, and it grows with `w`. So the row ledger cannot be holding that + stock. It is borrowed inside the call, as fact 6 says, and this is the + same w-shape point as fact 5 and the `ledger_constant_as_rho` control. ## Controls @@ -105,36 +172,64 @@ Each of these must be rejected: 8. 9909 used as a w-free `rho`. 9. The `S_leaf=1` premise removed. 10. A guard set below sigma. +11. PR2250's adapter callee given external row stock. +12. PR2234's per-level stock coefficient changed to 4098. +13. PR2287's leaves given a BIT reserve. +14. PR2287's divisor family count doubled. +15. A tampered headroom on the last conservative stage. +16. PR2234's prime bound lowered to `q > 2^2`. ## Not claimed -No supplier, κ, cutoff, frontier or selected-record change. Only native -stage 1 is checked. Neither reading is shown to be the one the selected -lowering realizes. The PR2084 coefficient is used as that package's -conditional result, not re-derived. The composition in reading (b) is a -stated argument, not a proved lemma. This is a finite source-bound audit, -not a supplier replay or a multiplication theorem. Overlap was checked -against open and closed PRs, package READMEs and Discussion titles; I didn't -search Discussion bodies. +- No supplier, κ, cutoff, frontier or selected-record change. +- The stage records are the `selected-bootstrap-stock-audit` receipt. Their + cutoffs and gaps are taken as recorded, not recomputed from the selected + savings. +- `rho = 0` rests on PR2287, PR2250, PR2234 and PR2899. The PR ledger + (`docs/research/pr-ledger.json`) records all four as `incorporated` after + a scoped review of written constructions with passing replays. None is an + executed GL64 or O(73,2) machine or a formal proof. PR2234 itself says + "Independent mathematical review remains necessary" (PROOF.md L432). +- PR3385, the physical controller, is only `partially_reviewed`: source-only + archival intake with no scientific verifier run. So are #3113 (B) and + #3421 (`A = 0`). +- No physical O(73,2)/GL64 payload has been run by those sources or by this + package. +- The PR2084 coefficient is used as that package's conditional result, not + re-derived. +- This is a finite source-bound audit, not a supplier replay or a + multiplication theorem. +- Overlap covered open and closed PRs and package READMEs. It also covered + Discussion search for the terms in TASK.json, Discussions #2238 and #2319 + in full, and the latest 100 comments of #1166. ## Open next questions -The structured versions are in [TASK.json](TASK.json). - -1. **Which reading holds?** Inside selected m=73 nodes, is each BIT callee a - completed call, or does the parent reserve its factor? This decides - between `rho = 0` and `rho >= sigma_BIT`. First step: classify the - adapter and peeled-atom call sites in the PR1094 source manifest. Blocked - by: no pinned sentence names the reservation mode for selected m=73 - adapters. -2. **All fourteen stages.** Repeat the guard comparison for native stages - 2–7 and the conservative branch, using each stage's own `s` and headroom. - This is bounded arithmetic once question 1 is settled. -3. **Is the external ledger still source-bound?** The term 9909 was derived - for a fixed-wire historical family. If the selected BIT digit tower had to - sit in the external reserve, that term would not be bound to the selected - producer. First step: trace where the selected assembler routes PR589's - q-adic selector stock. +The structured versions are in [TASK.json](TASK.json). The earlier first +question, which reading the selected layer realizes, is answered by fact 6. +The earlier second question, covering all fourteen stages, is answered in +"What follows for `rho`". The earlier third question, about the external +ledger, is answered in "What the 9909 and 252 slots pay for". + +1. **A source-bound replay of PR3385.** `rho = 0` uses written constructions + that have had a scoped review: PR2287's layer and the PR2234/PR2899 B1 + callee. PR3385 is the physical controller that binds the compact + adapters to B1/C0, and its ledger entry still asks for "independent + scientific review and source-bound replay". First step: run its + registered replay (Python 3.12). Then check B1's borrowing fit `k < e/2` + at the compact-field widths where PR3385's adapters call it. +2. **Does an H3 envelope apply to the complex layer at all?** PR2287 takes + its rows from its own prefix of `q0` chunks, not from bootstrap borrowing. + The bootstrap's stopped producer is the PR589 BIT + (`docs/research/selected-bootstrap-scope-map.md`). If the complex layer + never enters a bootstrap fit, the m=73 sigma is a consistency bound + rather than an obligation. If an H3 fit did apply, it would also have to + count the three H-bit compact fields, about `3dG/K` axes (PR3385 + L177–178). That amount does not have the `sigma·w·(1+log2 e)` shape. + First step: find any selected composition that bootstraps the complex + layer. +3. **The 1024 prefix term.** It is bound here only to the invoice + (`2·512`). This package does not trace which construction step uses it. ## Credit @@ -149,6 +244,11 @@ The structured versions are in [TASK.json](TASK.json). of the 18355 formula. - Josie Elliston (PR1965) and ToikY (`selected-bootstrap-stock-audit`) supplied the stage receipt and guard. +- Jose Manuel supplied the selected complex layer and its physical + controller (PR2287, PR3385), the compact adapters (PR2250, which retains + Douglas Colkitt's compact-control method), the selected BIT interchange + (PR2234) and the physical ordinary wrapper B1 (PR2899, around Nick + Petalas's PR2808 wrapper). Fact 6 reads them; it adds no construction. - Jeremy Kothe (PR1087) and Rohan Arun (PR1094) supplied the selected assembler and invoice. The partial-gauge, three-stage, paired-cube and structured-bulk assembly notes keep their original attribution. diff --git a/research/selected-stock-rho-ledger/SOURCES.json b/research/selected-stock-rho-ledger/SOURCES.json index ca73ef8fc9..26e9f8faf9 100644 --- a/research/selected-stock-rho-ledger/SOURCES.json +++ b/research/selected-stock-rho-ledger/SOURCES.json @@ -14,6 +14,12 @@ "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" }, + { + "path": "docs/research/pr-ledger.json", + "usage": "provenance", + "git_blob": "c682b4c39dd71dba9ffa9983f1e0549cfd2c0e56", + "sha256": "94fab8260d087cfcb4bd9ca5eb55178587cdeb52f597ac401463f8c4378d575d" + }, { "path": "notes/paired-cube-assembly.tex", "usage": "input", @@ -56,12 +62,30 @@ "git_blob": "238226c568742dd5723b03eabae564a2eaa2bda9", "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" }, + { + "path": "research/physical-complex-controller/PROOF.md", + "usage": "provenance", + "git_blob": "c505caecc7ced19a4efc35c423efedda9427bea5", + "sha256": "471185621c0ecce295ffd327b1244aed234efe5ff05a804aaaa11316f1a8319e" + }, + { + "path": "research/physical-ordinary-interchange/README.md", + "usage": "provenance", + "git_blob": "66e3e174a890fd731a7562fec5358400534ea75b", + "sha256": "dec1ca108a1dbd2d81df6f18d4e75040ce7538c804ed697478ae360af8f6b86a" + }, { "path": "research/selected-bit-parent-reserve/README.md", "usage": "input", "git_blob": "86dacf2f68b8e2127c8f6fe87fb98fd71ef1f422", "sha256": "16b84730b7a604e805034008e11bae4f90fe6c91db6098d5bd5d011dded5f4ee" }, + { + "path": "research/selected-bit-recursive-closure/PROOF.md", + "usage": "input", + "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531", + "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344" + }, { "path": "research/selected-bootstrap-stock-audit/RESULT.json", "usage": "input", @@ -74,6 +98,18 @@ "git_blob": "e0854d3afd012f7413147bd927812467843aca77", "sha256": "fe1a29b3757a3fda7124027e7e14228a6f3aa49521e23822909036172807f800" }, + { + "path": "research/selected-complex-compact-adapters/PROOF.md", + "usage": "input", + "git_blob": "685efc529493e4b841c1ce8799d28968b4991d7e", + "sha256": "804446e22304540eb02a5f4da3f71464a217be830a33b11420ea31eea878782c" + }, + { + "path": "research/selected-complex-layer-closure/PROOF.md", + "usage": "input", + "git_blob": "d7ec0d101405a5f099f55f6a73e9791731737fd0", + "sha256": "43feda0342c07a9429699c3a44e8936a3f3fb57ce9b32f38ff3dc06ac887b265" + }, { "path": "research/selected-stock-envelope-m73/README.md", "usage": "input", diff --git a/research/selected-stock-rho-ledger/TASK.json b/research/selected-stock-rho-ledger/TASK.json index ff4d1e7d25..c1bba35b0b 100644 --- a/research/selected-stock-rho-ledger/TASK.json +++ b/research/selected-stock-rho-ledger/TASK.json @@ -62,33 +62,33 @@ ] }, "scope_status": "refined", - "actual_scope": "Source-bind the non-complex terms of the selected m=73 row ledger (9909, 252, 1024) and decide whether they bind the leaf reserve rho in sigma <= (43/26)(1-s)(A+B) + rho at native stage 1.", - "scope_change_reason": "The card asks for an explicit envelope. #3113 and #3421 bound B and A for the m=73 producer and left rho as the only unbound term; this package addresses only rho, at native stage 1, and ends at a named two-way missing lemma rather than one admitted envelope.", + "actual_scope": "Source-bind the non-complex terms of the selected m=73 row ledger (9909, 252, 1024), show they do not bind the leaf reserve rho in sigma <= (43/26)(1-s)(A+B) + rho, and settle rho from the merged selected complex layer (PR2287/PR3385 with PR2250, PR2234, PR2899) check it against all fourteen recorded stage guards, and say what the 9909 and 252 slots pay for in the selected layer.", + "scope_change_reason": "The card asks for an explicit envelope. #3113 and #3421 bound B and A for the m=73 producer and left rho as the only unbound term; this package addresses only rho. It finds rho = 0 conditionally on the merged selected-complex chain, whose authors mark parts of it as under review.", "bottleneck_link": "Inherited implementation obligation (H3 stock fit) for the selected result; it changes no supplier, kappa or cutoff. It prevents an external-ledger constant from being counted as a proved borrowed-stock coefficient.", "budget_minutes": 90, - "stop_rule": "Stop once each ledger term is bound to source and rho is reduced to a named dichotomy with both branches checked against the stage-1 guard; do not attempt the completed-leaf implementation proof or other stages.", + "stop_rule": "Stop once each ledger term is bound to source and every callee of the selected complex layer is classified from pinned source; do not re-derive the completed-callee proofs themselves.", "outcome": "partial", - "evidence": "verify.py: 42 exact checks over 13 pinned inputs plus three PR1087 tarball members, and 10 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... controls=10 checks=42.", + "evidence": "verify.py: 62 exact checks over 15 pinned inputs plus three PR1087 tarball members (and five provenance pins), and 16 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... L_bits=2642 S_leaf=1 ... stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62.", "author": "Mainzu", "ai_assistance": "Substantial assistance from Claude Code (Anthropic, Claude Opus 5.5) for source search, the verifier and drafting; no independent human review is claimed.", "open_questions": [ { - "question": "Inside selected m=73 nodes, is every BIT callee a completed ordinary call with internal borrowing, or does the parent reserve the BIT factor (structured-bulk: 'Both factors are reserved simultaneously')?", - "why_it_matters": "It decides rho = 0 (sigma <= 4362.14) versus rho >= sigma_BIT (w-shaped; 8194 under PR2084), i.e. which conditional envelope the outer proof may cite.", - "first_step": "Locate the selected complex construction's adapter/peeled-atom call sites in the PR1094 source manifest and classify each as completed-call or parent-reserved.", - "blocked_by": "The selected complex lowering is inherited; no pinned sentence names the reservation mode for selected m=73 adapters." + "question": "Does a source-bound replay of PR3385 confirm the physical binding of the compact adapters to B1/C0, and does B1's borrowing fit k < e/2 hold at the compact-field widths where those adapters call it?", + "why_it_matters": "rho = 0 uses written constructions incorporated after scoped review (PR2287, PR2250, PR2234, PR2899); PR3385, which binds them physically, has had source-only archival intake.", + "first_step": "Run PR3385's registered replay on Python 3.12, then compare B1's fit threshold with the (f-1)G-bit compact-field pieces.", + "blocked_by": "Nothing technical; the registered replay needs Python 3.12." }, { - "question": "Do reading (a) and reading (b) also pass at native stages 2-7 and the seven conservative stages?", - "why_it_matters": "This package checks only native stage 1; the outer proof needs all fourteen recorded stages.", - "first_step": "Repeat section 9 of verify.py for every stage record in selected-bootstrap-stock-audit/RESULT.json using its own s and stock_headroom_log2.", - "blocked_by": "Nothing technical; it is bounded arithmetic once question 1's reading is fixed." + "question": "Does an H3 stock envelope apply to the selected complex layer at all, given that PR2287 takes its rows from its own q0-chunk prefix rather than from bootstrap borrowing?", + "why_it_matters": "The bootstrap's stopped producer is the PR589 BIT. If the complex layer never enters a bootstrap fit, the m=73 sigma is a consistency bound rather than an obligation. If it did apply, it would also have to count the three H-bit compact fields (about 3dG/K axes), which do not have the sigma*w*(1+log2 e) shape.", + "first_step": "Search the selected composition for any step that bootstraps the complex layer.", + "blocked_by": "Nothing technical." }, { - "question": "Is the external polynomial reserve itself (degree 16469 < 20161, p^(10^6)) still sufficient for the selected BIT family, whose divisor has a w-dependent digit tower?", - "why_it_matters": "9909 was derived for a historical coarse-bit family with fixed 27-bit wires; if the selected BIT tower must sit in the external reserve, that ledger term is not source-bound to the selected producer.", - "first_step": "Trace where the selected assembler routes PR589's q-adic selector stock: external ledger or internal borrowing (three-stage-cover-assembly.tex states the latter for the historical families).", - "blocked_by": "Same inherited lowering as question 1." + "question": "Which construction step uses the 1024 = 2*512 prefix term of the complex row?", + "why_it_matters": "It is the one ledger term this package binds only to the invoice.", + "first_step": "Trace charged_prefix_bits and row_prefix_extra in invoice_allcold.py to the construction notes.", + "blocked_by": "Nothing technical." } ] } diff --git a/research/selected-stock-rho-ledger/VERIFY.json b/research/selected-stock-rho-ledger/VERIFY.json index fa70cb9301..2a1094ec39 100644 --- a/research/selected-stock-rho-ledger/VERIFY.json +++ b/research/selected-stock-rho-ledger/VERIFY.json @@ -12,8 +12,11 @@ "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", "research/selected-bit-parent-reserve/README.md", + "research/selected-bit-recursive-closure/PROOF.md", "research/selected-bootstrap-stock-audit/RESULT.json", "research/selected-coarse-depth-stock/PROOF.md", + "research/selected-complex-compact-adapters/PROOF.md", + "research/selected-complex-layer-closure/PROOF.md", "research/selected-stock-envelope-m73/README.md", "research/selected-stock-shape-a-zero/PROOF.md" ], @@ -26,7 +29,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Authenticates all live inputs and three tarball members by SHA-256; parses the selected ledger, family pairs, prefix payload, PR589 record and stage-1 receipt; 42 exact checks; 10 mutation controls (tampered byte, ledger constant, family wire bits, Sp(70,2), prefix extra, eleven-stage BIT record, row gap, w-free constant as rho, missing S_leaf premise, guard below sigma) must each be rejected." + "checks": "Authenticates all live inputs and three tarball members by SHA-256; parses the selected ledger, family pairs, prefix payload, PR589 record and all fourteen stage records and the PR2287/PR2250/PR2234 callee contract; the 9909/252 slot and q-adic row arithmetic; 62 exact checks; 16 mutation controls (tampered byte, ledger constant, family wire bits, Sp(70,2), prefix extra, eleven-stage BIT record, row gap, w-free constant as rho, missing S_leaf premise, guard below sigma, adapter callee given external row stock, BIT stock coefficient 4098, leaves given a BIT reserve, divisor families doubled, late-stage headroom tampered, BIT prime bound lowered) must each be rejected." } ] } diff --git a/research/selected-stock-rho-ledger/verify.py b/research/selected-stock-rho-ledger/verify.py index 32b4d4cb4a..61ee76bbfd 100644 --- a/research/selected-stock-rho-ledger/verify.py +++ b/research/selected-stock-rho-ledger/verify.py @@ -4,7 +4,7 @@ Standard library only. Reads the pinned live inputs named in SOURCES.json (and three members of the pinned PR1087 tarball, in memory); nothing from the repository is imported or executed. Every proof-relevant constant is parsed -from source text, then checked by exact integer/rational arithmetic. Ten +from source text, then checked by exact integer/rational arithmetic. Sixteen mutation controls must each be rejected. Mainzu, with substantial Claude Code assistance. Apache-2.0. @@ -185,9 +185,79 @@ def ok(cond, what): sigma_a, sigma_b = base, base + rho_b g_a, g_b = ceil_log2(8 * sigma_a), ceil_log2(8 * sigma_b) ok(g_a <= h1 and g_b <= h1, "sufficient guard ceil(log2(8 sigma)) <= H_1") + + # 10. Mode of the BIT callee inside selected complex nodes (open question 1). + # The "reserved simultaneously" factor is a fixed-wire external one ... + ok("W_b,W_c<2^{43}" in sb and "Nested bit adapters require \\[ Q=W_c^{D_c(e)}W_b^{D_b(e)}. \\]" in sb + and "The sufficient stock is $p^{108000}$" in sb, "simultaneous factor is fixed-wire external") + # ... while the selected adapters' callee gets no external row stock (PR2250) ... + ca = flat(t["research/selected-complex-compact-adapters/PROOF.md"]) + ok("bind its tensor interpretation to the selected R480/T16 complex supplier" in ca, "PR2250 is selected-bound") + ok("It may borrow internally; we grant it no external row stock or ancestor access." in ca, + "PR2250: adapter callee has no external row stock") + # ... and that callee, PR2234's selected BIT, borrows its own 4097w-per-level stock. + rc = flat(t["research/selected-bit-recursive-closure/PROOF.md"]) + tau = re.search(r"tau=1-(\d+)/(\d+)\. Its review status remains separate", ca) + a_ = re.search(r"a = (\d+)/(\d+) = ", rc) + ok(tau is not None and a_ is not None and tau.groups() == a_.groups(), "PR2250's callee is PR2234's interchange") + ok("The machine restores spectators and clears its work." in rc + and "Choose the sufficient stock S=K(w)^D(e) from the original width e" in rc, "PR2234 completed contract") + kb = re.search(r"log_q K < 4096w\+1 <=(\d+)w\. Borrow k=ceil\(log_q S\)=O\(w log e\) leading digits " + r"from the earlier chunk\. Eventually k=L^D0(d)." in cl + and "For a child e', L^D0(e') divides U. A completed child restores its own row labels, so all " + "subsequent siblings reuse the same stock." in cl, "complex row stock is L^D0(d)") + ok("The next qF chunks supply two H-bit front compact fields; the last qB chunks supply one H-bit " + "back field." in cl and "No compact-field bit enters this selector." in cl, + "compact fields are reserved but are not row stock") + ok("First process the delta leftmost selected axes individually and retain their chunks as completed " + "spectators." in cl and "The leaves require only the elementary C kernel." in cl, "peeled axes, leaves elementary") + ok("The bound uses an ordinary binary chunk interchange with cost O(V b^tau), complete spectators and " + "restored work. PR2234 proposes that contract" in cl, "PR2287's ordinary callee is PR2234's contract") + + # 11. Every recorded stage, each with its branch's own s and its own headroom. + branches = json.loads(t["research/selected-bootstrap-stock-audit/RESULT.json"])["branches"] + rows = [(F(branches[k]["common_saving"]), int(st["cutoff_log2"]), F(st["gap"]), int(st["stock_headroom_log2"]), + {g: F(v) for g, v in st["gaps"].items()}) + for k in ("bootstrap", "conservative_bootstrap") for st in branches[k]["stages"]] + ok(len(rows) == 14 and all(0 < r[0] < 1 for r in rows), "fourteen stage records") + ok(all(g == min(gs.values()) and gs["stock"] == 1 - s_ for s_, _, g, _, gs in rows), "gap = least gap; stock gap = 1-s") + ok(all(cl_ >= 2 and cl_ * g * g >= 36 and 0 < g <= 1 - s_ for s_, cl_, g, _, _ in rows), "PR1965 premises, every stage") + ok(all(h == (cl_ * g) // 2 - 4 for _, cl_, g, h, _ in rows), "headroom = floor(L*gap/2)-4, every stage") + stage_g = [(ceil_log2(8 * F(43, 26) * (1 - s_) * b_bits), ceil_log2(8 * (F(43, 26) * (1 - s_) * b_bits + rho_b)), h) + for s_, _, _, h, _ in rows] + ok(all(ga <= h and gb <= h for ga, gb, h in stage_g), "both values pass every stage guard") + h_min = min(h for _, _, h in stage_g) + + # 12. What the 9909 and 252 slots pay for (open question 3). In the selected layer they pay + # for nothing: without them the complex row is 2B+1024. The BIT the adapters call is PR2234's + # q-adic one: its level divisor has at least 4096*80-2 bits, since |GL_64(F_q)| >= q^4096/2 + # with q > 2^80. In the certificate's row convention (halving depth x bits per level) that + # exceeds the cap even at w = 1, so the row ledger cannot be holding that BIT's stock; it is + # borrowed inside the call instead. + cap = int(re.search(r"finite\['retained_row_coefficient'\]==(\d+)", asm).group(1)) + lean = 2 * b_bits + c_prefix + ok(lean < ledger < cap, "the 9909 and 252 slots are slack in the selected layer") + qm = re.search(r"We fix one odd prime q>2\^(\d+) throughout;", rc) + km = re.search(r"log_q K < (\d+)w\+1 <=", rc) + ok(qm is not None and km is not None and int(km.group(1)) == 64 * 64, "PR2234 prime size and level exponent") + qadic = hd * (int(km.group(1)) * int(qm.group(1)) - 2) + ok(qadic > cap, "one q-adic BIT level exceeds the external row cap") return dict(checks=n[0], b=b_bits, ledger=ledger, c=(c_bit, c_leaf, c_prefix), fam=(hb, wb, hl, wl), bit_row=rec["row_coefficient"], sigma_bit=sigma_bit, implicit=implicit, - sigma_a=sigma_a, sigma_b=sigma_b, g=(g_a, g_b), h1=h1) + sigma_a=sigma_a, sigma_b=sigma_b, g=(g_a, g_b), h1=h1, l_bits=l_bits, stages=len(rows), h_min=h_min, lean=lean, qadic=qadic, cap=cap) def controls(pins, raw, texts): @@ -222,6 +292,19 @@ def tamper(): "missing_s_leaf_premise": text_edit("research/selected-coarse-depth-stock/PROOF.md", "one may take S_leaf=1", "one may take S_leaf=2"), "guard_below_sigma": param(h1_override=15), + "adapter_callee_external_stock": text_edit("research/selected-complex-compact-adapters/PROOF.md", + "it no external row stock", "it an external row stock"), + "bit_stock_coefficient_4098": text_edit("research/selected-bit-recursive-closure/PROOF.md", + "<=4097w.", "<=4098w."), + "leaves_given_bit_reserve": text_edit("research/selected-complex-layer-closure/PROOF.md", + "The leaves require only the", "The leaves require a BIT reserve and the"), + "divisor_families_doubled": text_edit("research/selected-complex-layer-closure/PROOF.md", + "W=14336 live families", "W=28672 live families"), + "bit_prime_two_bits": text_edit("research/selected-bit-recursive-closure/PROOF.md", + "q>2^80 throughout", "q>2^2 throughout"), + "late_stage_headroom_tampered": text_edit("research/selected-bootstrap-stock-audit/RESULT.json", + '"stock_headroom_log2": 296674207198239164557594', + '"stock_headroom_log2": 296674207198239164557595'), } for name, run in cases.items(): try: @@ -241,8 +324,10 @@ def main(): f"{r['c'][0]}={r['fam'][0]}*{r['fam'][1]} {r['c'][1]}={r['fam'][2]}*{r['fam'][3]} " f"{r['c'][2]}=2*{r['c'][2] // 2} bit_row={r['bit_row']}={r['sigma_bit']}+{r['c'][0]}+{r['c'][1]} " f"implicit_rho_3113={r['implicit']} rho_a=0 sigma_a<={float(r['sigma_a']):.2f} " - f"rho_b={r['sigma_bit']} sigma_b<={float(r['sigma_b']):.2f} " - f"guard={r['g'][0]},{r['g'][1]}<={r['h1']} controls={k} checks={r['checks']}") + f"rho_b={r['sigma_bit']} sigma_b<={float(r['sigma_b']):.2f} L_bits={r['l_bits']} S_leaf=1 " + f"guard={r['g'][0]},{r['g'][1]}<={r['h1']} stages={r['stages']} H_min={r['h_min']} " + f"lean_row={r['lean']} qadic_bit_row>={r['qadic']}>{r['cap']} " + f"controls={k} checks={r['checks']}") if __name__ == "__main__": From 2b4a97e252b36b9914459fcc6ffeb0da2042fdb9 Mon Sep 17 00:00:00 2001 From: Mainzu <107363567+Mainzu@users.noreply.github.com> Date: Sun, 18 Oct 2026 22:35:40 +0700 Subject: [PATCH 3/5] Answer open question 2: no selected step bootstraps the m=73 layer Co-Authored-By: Claude Opus 5.5 --- research/selected-stock-rho-ledger/README.md | 46 ++++++++++++++----- .../selected-stock-rho-ledger/SOURCES.json | 6 +++ research/selected-stock-rho-ledger/TASK.json | 8 +--- 3 files changed, 41 insertions(+), 19 deletions(-) diff --git a/research/selected-stock-rho-ledger/README.md b/research/selected-stock-rho-ledger/README.md index aad1e64d72..57c0735792 100644 --- a/research/selected-stock-rho-ledger/README.md +++ b/research/selected-stock-rho-ledger/README.md @@ -126,6 +126,8 @@ source text, not typed in. Nothing from the repository is imported or executed. `1 − s`, and PR1965's premises (`L ≥ 2`, `L·gap² ≥ 36`, `0 < gap ≤ 1 − s`). The tightest stage is stage 1 in both branches, at `H = 6,562,783`. The guards are only 16 and 17. + No selected step bootstraps the complex layer (see "Where the H3 fit + applies"), so these are consistency checks, not obligations. ## What the 9909 and 252 slots pay for @@ -158,6 +160,31 @@ The selected certificate charges the complex row stock. It is borrowed inside the call, as fact 6 says, and this is the same w-shape point as fact 5 and the `ledger_constant_as_rho` control. +## Where the H3 fit applies + +No selected step bootstraps the m=73 complex layer. + +- **The bootstrap chain is the bit chain.** The selected assembler builds + one seven-step chain per branch, then calls + `A.assembly(chain[-1],bb,...)` (PR1087 `code/assemble.py` L205–214). +- **The complex saving is a fixed input.** The pinned `engines/outer.py` + (`research/complex-k492-owner-repair/vendor/multicold/`, the copy PR1087 + pins) takes the chain's end as `bit_saving` and the complex root `bb` as + `complex_saving` (L16–17). +- **It only caps `s`.** The complex saving reaches the chain only through + `s=min(c,(1-beta)*bb)-1/10^27` (`assemble.py` L206). That cap is what the + outer slacks `complex_above_bit=b-a` and `leaf_saving_above_bit=(1-beta)*b-a` + need (outer.py L27, L29). +- **The layer itself has no stage.** Its fallbacks are elementary kernels, + not a previous-stage algorithm. PR2287 says "If D<=Q0, apply the selected + C kernels individually" (L139) and "The base cutoff is max(73,d^beta)" + (L424). Where its compact-field inequality fails, it uses "individual + kernels" (L442–443). + +So this package's m=73 sigma is a consistency bound, not an obligation of +the selected record. The H3 envelope the record needs belongs to the bit +producer, for example PR2084's conditional 8194. + ## Controls Each of these must be rejected: @@ -209,7 +236,9 @@ The structured versions are in [TASK.json](TASK.json). The earlier first question, which reading the selected layer realizes, is answered by fact 6. The earlier second question, covering all fourteen stages, is answered in "What follows for `rho`". The earlier third question, about the external -ledger, is answered in "What the 9909 and 252 slots pay for". +ledger, is answered in "What the 9909 and 252 slots pay for". The previous +version's second question, whether an H3 envelope applies to the complex +layer at all, is answered in "Where the H3 fit applies": it does not. 1. **A source-bound replay of PR3385.** `rho = 0` uses written constructions that have had a scoped review: PR2287's layer and the PR2234/PR2899 B1 @@ -218,17 +247,7 @@ ledger, is answered in "What the 9909 and 252 slots pay for". scientific review and source-bound replay". First step: run its registered replay (Python 3.12). Then check B1's borrowing fit `k < e/2` at the compact-field widths where PR3385's adapters call it. -2. **Does an H3 envelope apply to the complex layer at all?** PR2287 takes - its rows from its own prefix of `q0` chunks, not from bootstrap borrowing. - The bootstrap's stopped producer is the PR589 BIT - (`docs/research/selected-bootstrap-scope-map.md`). If the complex layer - never enters a bootstrap fit, the m=73 sigma is a consistency bound - rather than an obligation. If an H3 fit did apply, it would also have to - count the three H-bit compact fields, about `3dG/K` axes (PR3385 - L177–178). That amount does not have the `sigma·w·(1+log2 e)` shape. - First step: find any selected composition that bootstraps the complex - layer. -3. **The 1024 prefix term.** It is bound here only to the invoice +2. **The 1024 prefix term.** It is bound here only to the invoice (`2·512`). This package does not trace which construction step uses it. ## Credit @@ -244,6 +263,9 @@ ledger, is answered in "What the 9909 and 252 slots pay for". of the 18355 formula. - Josie Elliston (PR1965) and ToikY (`selected-bootstrap-stock-audit`) supplied the stage receipt and guard. +- philippeVV (Discussion #1166, comment 18932239) independently named the + PR589 BIT, not the m=73 supplier, as the stopped producer, minutes after + PR2084 opened. - Jose Manuel supplied the selected complex layer and its physical controller (PR2287, PR3385), the compact adapters (PR2250, which retains Douglas Colkitt's compact-control method), the selected BIT interchange diff --git a/research/selected-stock-rho-ledger/SOURCES.json b/research/selected-stock-rho-ledger/SOURCES.json index 26e9f8faf9..03eab650c2 100644 --- a/research/selected-stock-rho-ledger/SOURCES.json +++ b/research/selected-stock-rho-ledger/SOURCES.json @@ -50,6 +50,12 @@ "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py", + "usage": "provenance", + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, { "path": "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", "usage": "input", diff --git a/research/selected-stock-rho-ledger/TASK.json b/research/selected-stock-rho-ledger/TASK.json index c1bba35b0b..fe5c0aa20c 100644 --- a/research/selected-stock-rho-ledger/TASK.json +++ b/research/selected-stock-rho-ledger/TASK.json @@ -68,7 +68,7 @@ "budget_minutes": 90, "stop_rule": "Stop once each ledger term is bound to source and every callee of the selected complex layer is classified from pinned source; do not re-derive the completed-callee proofs themselves.", "outcome": "partial", - "evidence": "verify.py: 62 exact checks over 15 pinned inputs plus three PR1087 tarball members (and five provenance pins), and 16 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... L_bits=2642 S_leaf=1 ... stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62.", + "evidence": "verify.py: 62 exact checks over 15 pinned inputs plus three PR1087 tarball members (and six provenance pins), and 16 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... L_bits=2642 S_leaf=1 ... stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62.", "author": "Mainzu", "ai_assistance": "Substantial assistance from Claude Code (Anthropic, Claude Opus 5.5) for source search, the verifier and drafting; no independent human review is claimed.", "open_questions": [ @@ -78,12 +78,6 @@ "first_step": "Run PR3385's registered replay on Python 3.12, then compare B1's fit threshold with the (f-1)G-bit compact-field pieces.", "blocked_by": "Nothing technical; the registered replay needs Python 3.12." }, - { - "question": "Does an H3 stock envelope apply to the selected complex layer at all, given that PR2287 takes its rows from its own q0-chunk prefix rather than from bootstrap borrowing?", - "why_it_matters": "The bootstrap's stopped producer is the PR589 BIT. If the complex layer never enters a bootstrap fit, the m=73 sigma is a consistency bound rather than an obligation. If it did apply, it would also have to count the three H-bit compact fields (about 3dG/K axes), which do not have the sigma*w*(1+log2 e) shape.", - "first_step": "Search the selected composition for any step that bootstraps the complex layer.", - "blocked_by": "Nothing technical." - }, { "question": "Which construction step uses the 1024 = 2*512 prefix term of the complex row?", "why_it_matters": "It is the one ledger term this package binds only to the invoice.", From 8ee2335cdeca901e987f3855b6df92bbee9a3889 Mon Sep 17 00:00:00 2001 From: Mainzu <107363567+Mainzu@users.noreply.github.com> Date: Sun, 18 Oct 2026 23:51:00 +0700 Subject: [PATCH 4/5] Answer open question 1: PR3385 replay and B1's fit at compact widths Co-Authored-By: Claude Opus 5.5 --- research/selected-stock-rho-ledger/README.md | 76 +++++++++++++++---- .../selected-stock-rho-ledger/SOURCES.json | 36 +++++++++ research/selected-stock-rho-ledger/TASK.json | 8 +- 3 files changed, 98 insertions(+), 22 deletions(-) diff --git a/research/selected-stock-rho-ledger/README.md b/research/selected-stock-rho-ledger/README.md index 57c0735792..8c709d2111 100644 --- a/research/selected-stock-rho-ledger/README.md +++ b/research/selected-stock-rho-ledger/README.md @@ -69,8 +69,9 @@ source text, not typed in. Nothing from the repository is imported or executed. internal borrowed stock. 6. **The selected complex layer's only row stock is its own divisor.** Jose Manuel's PR2287 (`selected-complex-layer-closure/PROOF.md`) is the written - all-size m=73 layer. PR3385 implements it physically; that archive has had - intake checks only, with no scientific verifier run. PR2287 sets + all-size m=73 layer. PR3385 implements it physically; the PR ledger records + intake checks only for that archive, with no scientific verifier run. A + local replay is in "PR3385 replay and B1's fit". PR2287 sets `W = 14336` and `L = W·|O(73,2)|`. Its only row stock is `L^D0(d)`, taken from a prefix of `q0 = ceil(log2 L)·D0(d)` chunks. A child receives `U` with `L^D0(e') | U`, and "a completed child restores its own row labels". @@ -185,6 +186,52 @@ So this package's m=73 sigma is a consistency bound, not an obligation of the selected record. The H3 envelope the record needs belongs to the bit producer, for example PR2084's conditional 8194. +## PR3385 replay and B1's fit + +This is local evidence, outside this package's verifier. It was run with +Python 3.12.10 on Windows 11 at `2b4a97e`. PR3385's 38 package files there +have the same Git blobs as its head `7e5a187`. + +- **The registered replay fails on Windows only.** It stops in the second + check. The cause is a frozen predecessor verifier: member + `inputs/pr2753/verify.py` of + `research/physical-ordinary-interchange/inputs/pr2809.tar` (L72–75). It + compares `str(path.relative_to(...))` with `/`-separated names. On Windows + that string uses `\`, so it raises "no omitted or extra predecessor files". + This is a portability issue, not a mathematical failure. +- **With a local path shim, all three suites pass.** The shim only makes + relative paths print with `/`. It is not part of this package, and the run + is not the registered replay. + - The `sources`, `execution` and `planning` suites print their PASS + markers, over 16 checks. + - All nine receipt hashes in PR3385's `EVIDENCE.md` (L17–25) match. + - The fixtures reach only B1's elementary branch (`check_monomial.py` + L66–67). + - On this laptop the `execution` suite took 727 s, longer than its + registered 420 s timeout. +- **B1 borrows only on very wide compact fields.** + - The adapters call B1 only on compact fields of width `nG`, with + `n = f-1` (PR2250 `PROOF.md` L20, L73–74). + - B1 turns `b` bits into `e = ceil(b/log2 q)` radix-q digits (PR2234 + `PROOF.md` L412–413). + - B1 runs its fitted branch only if `2k < e` and the body has at least 64 + atoms (PR2899 `PROOF.md` L71–78). + - At `q* = 213·2^80+1` (PR3385 `PROOF.md` L43), `k < e/2` holds for + every `e >= 311311` and fails at `e = 311310` + (`bit2234-stock-threshold/README.md` L34–35, L137–140). + - So B1 is fitted when `(f-1)G >= bitlength(q*^311310) = 27,312,693` + bits. Below that it runs its elementary branch, as PR2234 (L408–410), + PR2899 (L80–85) and PR3385 (`PROOF.md` L185–186) say. + - The widths can only reach that size when the precision p is at least + 19,782,090. This uses `f = floor(e/73)` (PR2287 L159–160), plus + `d = floor(p^(997/1000))` and `D <= d` (PR3385 `PROOF.md` L9–10). + - A local exact-integer check, not part of this package, confirms these + numbers. It also finds no fitted width below 311311 at q*. +- **Neither branch takes row stock from the caller.** The fitted branch + borrows `k` leading digits of its own earlier chunk (PR2234 L382–388). The + elementary branch is one atom swap over `Z/q^e` (PR2899 `ordinary.py` + L106–114). So `rho = 0` is unaffected. + ## Controls Each of these must be rejected: @@ -217,9 +264,11 @@ Each of these must be rejected: a scoped review of written constructions with passing replays. None is an executed GL64 or O(73,2) machine or a formal proof. PR2234 itself says "Independent mathematical review remains necessary" (PROOF.md L432). -- PR3385, the physical controller, is only `partially_reviewed`: source-only - archival intake with no scientific verifier run. So are #3113 (B) and - #3421 (`A = 0`). +- PR3385, the physical controller, is only `partially_reviewed` in the PR + ledger, after source-only archival intake. The local Windows run in "PR3385 + replay and B1's fit" used a path shim. It is not the registered replay and + not an independent review of PR3385's refinement. #3113 (B) and #3421 + (`A = 0`) are also only `partially_reviewed`. - No physical O(73,2)/GL64 payload has been run by those sources or by this package. - The PR2084 coefficient is used as that package's conditional result, not @@ -238,16 +287,11 @@ The earlier second question, covering all fourteen stages, is answered in "What follows for `rho`". The earlier third question, about the external ledger, is answered in "What the 9909 and 252 slots pay for". The previous version's second question, whether an H3 envelope applies to the complex -layer at all, is answered in "Where the H3 fit applies": it does not. - -1. **A source-bound replay of PR3385.** `rho = 0` uses written constructions - that have had a scoped review: PR2287's layer and the PR2234/PR2899 B1 - callee. PR3385 is the physical controller that binds the compact - adapters to B1/C0, and its ledger entry still asks for "independent - scientific review and source-bound replay". First step: run its - registered replay (Python 3.12). Then check B1's borrowing fit `k < e/2` - at the compact-field widths where PR3385's adapters call it. -2. **The 1024 prefix term.** It is bound here only to the invoice +layer at all, is answered in "Where the H3 fit applies": it does not. The +previous version's first question, a replay of PR3385 and B1's fit at the +compact widths, is answered in "PR3385 replay and B1's fit". + +1. **The 1024 prefix term.** It is bound here only to the invoice (`2·512`). This package does not trace which construction step uses it. ## Credit @@ -263,6 +307,8 @@ layer at all, is answered in "Where the H3 fit applies": it does not. of the 18355 formula. - Josie Elliston (PR1965) and ToikY (`selected-bootstrap-stock-audit`) supplied the stage receipt and guard. +- Aakash (`bit2234-stock-threshold`) proved the sharp 311311 borrowing-fit + cutoff that the B1 threshold uses. - philippeVV (Discussion #1166, comment 18932239) independently named the PR589 BIT, not the m=73 supplier, as the stopped producer, minutes after PR2084 opened. diff --git a/research/selected-stock-rho-ledger/SOURCES.json b/research/selected-stock-rho-ledger/SOURCES.json index 03eab650c2..1acbe82406 100644 --- a/research/selected-stock-rho-ledger/SOURCES.json +++ b/research/selected-stock-rho-ledger/SOURCES.json @@ -44,6 +44,12 @@ "git_blob": "983ffb6ac8fb9117360cd0797c00c05dfa071c9d", "sha256": "ccf34a6d37c4af14bebeab15be50ab204eb1caebe546385520050ec30089441d" }, + { + "path": "research/bit2234-stock-threshold/README.md", + "usage": "provenance", + "git_blob": "ede0d322c477af91d4c2cc33db0fd10958f45eab", + "sha256": "1e050c9f963421d751d9208092f9a15321ed77810e03912df8eb5eb56bbb06e7" + }, { "path": "research/community-frontier1094-audit/ASSEMBLY.json", "usage": "input", @@ -68,18 +74,48 @@ "git_blob": "238226c568742dd5723b03eabae564a2eaa2bda9", "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" }, + { + "path": "research/physical-complex-controller/EVIDENCE.md", + "usage": "provenance", + "git_blob": "e71b5fbc4d867572695e52a1b10aa8aa074b837d", + "sha256": "24b50eaa5dc28570d7118703cd3547c8232e56231f3fc5ca05e19ab116678370" + }, { "path": "research/physical-complex-controller/PROOF.md", "usage": "provenance", "git_blob": "c505caecc7ced19a4efc35c423efedda9427bea5", "sha256": "471185621c0ecce295ffd327b1244aed234efe5ff05a804aaaa11316f1a8319e" }, + { + "path": "research/physical-complex-controller/check_monomial.py", + "usage": "provenance", + "git_blob": "0369562c62d0c79c41a7ebed7a0e7b894908f4b1", + "sha256": "a301d39afb7475615716e2426c3df8fe0f6e8fa710c13f70ecb2a9026f52cd6d" + }, + { + "path": "research/physical-ordinary-interchange/PROOF.md", + "usage": "provenance", + "git_blob": "12be1f06062090fcc68e598bae250f185e3d8524", + "sha256": "8a1c2145cd8f080026488a571d95813c09679aa323f19aeaef0ea98030136e1c" + }, { "path": "research/physical-ordinary-interchange/README.md", "usage": "provenance", "git_blob": "66e3e174a890fd731a7562fec5358400534ea75b", "sha256": "dec1ca108a1dbd2d81df6f18d4e75040ce7538c804ed697478ae360af8f6b86a" }, + { + "path": "research/physical-ordinary-interchange/inputs/pr2809.tar", + "usage": "provenance", + "git_blob": "21ff4b5b9942dbc82b60b4546d39785daa22ba86", + "sha256": "ee1d4ec05e3c872d264be3b38f71a8c153acf37427f5d3ba87f8e15440c9ccf0" + }, + { + "path": "research/physical-ordinary-interchange/ordinary.py", + "usage": "provenance", + "git_blob": "81b330a4b886a0f4deab7b0811478bab3fbc107a", + "sha256": "7f8338e748bcd42fbef1e7cc47b6c5040dfb3aad216e34759bcb12b8e14f7705" + }, { "path": "research/selected-bit-parent-reserve/README.md", "usage": "input", diff --git a/research/selected-stock-rho-ledger/TASK.json b/research/selected-stock-rho-ledger/TASK.json index fe5c0aa20c..b1be2d8584 100644 --- a/research/selected-stock-rho-ledger/TASK.json +++ b/research/selected-stock-rho-ledger/TASK.json @@ -68,16 +68,10 @@ "budget_minutes": 90, "stop_rule": "Stop once each ledger term is bound to source and every callee of the selected complex layer is classified from pinned source; do not re-derive the completed-callee proofs themselves.", "outcome": "partial", - "evidence": "verify.py: 62 exact checks over 15 pinned inputs plus three PR1087 tarball members (and six provenance pins), and 16 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... L_bits=2642 S_leaf=1 ... stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62.", + "evidence": "verify.py: 62 exact checks over 15 pinned inputs plus three PR1087 tarball members (and twelve provenance pins), and 16 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... L_bits=2642 S_leaf=1 ... stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62. Local evidence outside verify.py (README, \"PR3385 replay and B1's fit\"): PR3385's registered replay fails on Windows only, at the frozen PR2753 verifier's path-separator check; with a local relative-path shim, which is not the registered replay, all three suites pass and all nine EVIDENCE.md receipt hashes match. B1 is fitted only at compact width (f-1)G >= 27,312,693 bits at q*, and elementary below that; neither branch takes caller row stock.", "author": "Mainzu", "ai_assistance": "Substantial assistance from Claude Code (Anthropic, Claude Opus 5.5) for source search, the verifier and drafting; no independent human review is claimed.", "open_questions": [ - { - "question": "Does a source-bound replay of PR3385 confirm the physical binding of the compact adapters to B1/C0, and does B1's borrowing fit k < e/2 hold at the compact-field widths where those adapters call it?", - "why_it_matters": "rho = 0 uses written constructions incorporated after scoped review (PR2287, PR2250, PR2234, PR2899); PR3385, which binds them physically, has had source-only archival intake.", - "first_step": "Run PR3385's registered replay on Python 3.12, then compare B1's fit threshold with the (f-1)G-bit compact-field pieces.", - "blocked_by": "Nothing technical; the registered replay needs Python 3.12." - }, { "question": "Which construction step uses the 1024 = 2*512 prefix term of the complex row?", "why_it_matters": "It is the one ledger term this package binds only to the invoice.", From ad7c0e10e5476136498b377a3a28b80640e55c08 Mon Sep 17 00:00:00 2001 From: Mainzu <107363567+Mainzu@users.noreply.github.com> Date: Mon, 19 Oct 2026 00:38:31 +0700 Subject: [PATCH 5/5] Answer the last open question: the selected layer does not use the 1024 term Co-Authored-By: Claude Opus 5.5 --- research/selected-stock-rho-ledger/README.md | 94 ++++++++++++++++--- .../selected-stock-rho-ledger/SOURCES.json | 18 ++++ research/selected-stock-rho-ledger/TASK.json | 14 +-- 3 files changed, 101 insertions(+), 25 deletions(-) diff --git a/research/selected-stock-rho-ledger/README.md b/research/selected-stock-rho-ledger/README.md index 8c709d2111..26884bb575 100644 --- a/research/selected-stock-rho-ledger/README.md +++ b/research/selected-stock-rho-ledger/README.md @@ -11,7 +11,8 @@ sigma <= (43/26)*(1-s)*(A+B) + rho, A = 0, B = 2642 That leaves `rho`, the leaf reserve, as the only unbound term. This package traces every non-complex term of the selected row ledger to its source. It -shows that those terms cannot serve as `rho`. It then reads the merged +shows that those terms cannot serve as `rho`, and that the selected layer's +construction uses none of them. It then reads the merged selected complex layer to settle how its callees get their stock: the layer's only row stock is its own divisor, so `S_leaf = 1` and `rho = 0`. This holds conditionally on that chain. All fourteen recorded stage guards pass either @@ -48,8 +49,15 @@ source text, not typed in. Nothing from the repository is imported or executed. and ordinary-leaf reserves" (`58344+9909+252`, `10284+9909+252`). The 367-level coarse-bit family is not the selected PR589 BIT producer, whose halving depth is 2. -3. **1024 is the prefix term.** `invoice_allcold.py` sets - `row_prefix_extra = 2*payload`, and `charged_prefix_bits = 512`. +3. **1024 is the row surcharge for the 512-bit prefix payload.** The payload + is the invoice's precision reserve: the bits by which an intermediate value + of the selected complex program may grow. PR1087's invoice needs the local + prefix bits plus `37+144+144+4` (`code/assemble.py` L165). These pay for + the input conversion, one bit per complete invocation sweep, one bit per + bridge sweep, and a 4-bit margin. Here that totals 397 (tarball README + L14). `code/invoice_allcold.py` charges `payload = 512` (L263, L285–288) + and adds `row_prefix_extra = 2*payload` to the complex row (L278, L297). + "What the 1024 term pays for" traces the factor 2. 4. **The selected BIT ledger stacks the same constants.** PR510's `assemble9.py` computes `row = DEPTH*(m*m+1)+9909+252 = 18355`. With PR589's `nine.bit` record (m=64, maximum child 42, 28,425 physical roles, @@ -161,6 +169,52 @@ The selected certificate charges the complex row stock. It is borrowed inside the call, as fact 6 says, and this is the same w-shape point as fact 5 and the `ledger_constant_as_rho` control. +## What the 1024 term pays for + +The 1024 is a precision reserve billed as row stock, and the selected layer +does not use it. + +- **The factor 2 is the halving depth.** + - The term entered with Dugongue's PR514. That PR replaced the old 192-bit + local prefix allowance with a 512-bit global one, for asynchronous + scheduling. + - Its invoice says "512 bits are charged, and an additional 2*512 enters + the two-level physical row bound". PR523 vendors it unchanged, with the + same Git blob as PR514's head, at + `research/punctured112-global/vendor/pr514/code/audit_async_invoice.py` + (scope L96, row formula L87). + - The PR484 invoice it replaced, vendored alongside, has no payload term + (`vendor/audit_scalar_invoice.py` L78). + - Two levels halve the width, because `73² > 2·48²` (PR2287 L129–130). So + the payload is billed once per halving level, like the stock bits. + - Hao Yan's PR858 T16 proof, whose controller PR1087 uses (tarball README + L20–21), calls this "the retained row formula" + (`research/complex-double-replica-owners/PROOF.md` L166–170). + - The same sentence appears earlier in Dugongue's closed + [PR505](https://github.com/CrocSwap/integer-mult-bounds/pull/505). +- **No source says why a precision reserve is row stock.** + - PR505, PR514, PR858, PR1087 and the assembly notes all state or compute + the term. None names a construction step that needs `2^512` extra rows at + each halving level. + - The assembly notes' "physically preceding prefix" is a different object. + It is the run of `q0 = ⌈log2 Q⌉` chunks that supplies the rows. Its single + padding grows volume by less than two (`structured-bulk-assembly.tex` + L84–91). Neither the prefix nor the padding is 512 bits. +- **The selected layer keeps rows and precision apart.** + - PR2287 reserves exactly `L^D0(d)` rows, from `q0 = ⌈log2 L⌉·D0(d)` chunks + (L136–147). That is the `2·2642` term. + - It supplies precision separately, with `Δ = ⌈C0·d⌉` guard bits on each + component (L374–380). + - It calls the finite 397-bit bound "useful bindings, but they are not this + all-depth proof" (L363–364). + - PR3385 does the same physically. It pads the row range once to a multiple + of `L^D0(d)` (`PROOF.md` L190–197), and it appends `Δ` low zeros and + `Δ+1` sign bits to each component (L199–201). +- **So 1024 is inherited slack, like 9909 and 252.** The marker's lean row + of 6308 still contains it. The selected layer's own row need is the stock + term `2·2642` alone. Removing the 1024 would not change κ, because only the + retained 20161 enters the outer assembly. + ## Where the H3 fit applies No selected step bootstraps the m=73 complex layer. @@ -273,26 +327,34 @@ Each of these must be rejected: package. - The PR2084 coefficient is used as that package's conditional result, not re-derived. +- "No source says why" covers only the sources named in "What the 1024 term + pays for". It does not show that no construction could use such a reserve. + It shows only that the selected layer's construction does not. - This is a finite source-bound audit, not a supplier replay or a multiplication theorem. - Overlap covered open and closed PRs and package READMEs. It also covered Discussion search for the terms in TASK.json, Discussions #2238 and #2319 - in full, and the latest 100 comments of #1166. + in full, and the latest 100 comments of #1166. For the 1024 term it also + covered PR and code search for `row_prefix_extra`, `charged_prefix_bits` + and "two-level row". ## Open next questions -The structured versions are in [TASK.json](TASK.json). The earlier first -question, which reading the selected layer realizes, is answered by fact 6. -The earlier second question, covering all fourteen stages, is answered in -"What follows for `rho`". The earlier third question, about the external -ledger, is answered in "What the 9909 and 252 slots pay for". The previous -version's second question, whether an H3 envelope applies to the complex -layer at all, is answered in "Where the H3 fit applies": it does not. The -previous version's first question, a replay of PR3385 and B1's fit at the -compact widths, is answered in "PR3385 replay and B1's fit". +None remain within this card's scope. [TASK.json](TASK.json) records the +reason: every ledger term is now bound, and the H3 envelope that the record +needs belongs to the bit producer (PR2084), outside this package. + +The last question was which construction step uses the 1024 prefix term. +"What the 1024 term pays for" answers it: none in the selected layer. The +earlier questions are answered here: -1. **The 1024 prefix term.** It is bound here only to the invoice - (`2·512`). This package does not trace which construction step uses it. +- which reading the selected layer realizes: fact 6; +- all fourteen stages: "What follows for `rho`"; +- what the 9909 and 252 slots pay for: "What the 9909 and 252 slots pay for"; +- whether an H3 envelope applies to the complex layer: "Where the H3 fit + applies" (it does not); +- the PR3385 replay and B1's fit at compact widths: "PR3385 replay and B1's + fit". ## Credit @@ -320,6 +382,8 @@ compact widths, is answered in "PR3385 replay and B1's fit". - Jeremy Kothe (PR1087) and Rohan Arun (PR1094) supplied the selected assembler and invoice. The partial-gauge, three-stage, paired-cube and structured-bulk assembly notes keep their original attribution. +- Dugongue (PR505, PR514) introduced the 512-bit global prefix allowance and + its two-level row charge. Hao Yan (PR858) retained it in the T16 reserves. Prepared by Mainzu, with substantial Claude Code (Anthropic) assistance. No independent human review is claimed. Apache-2.0. diff --git a/research/selected-stock-rho-ledger/SOURCES.json b/research/selected-stock-rho-ledger/SOURCES.json index 1acbe82406..140ec15505 100644 --- a/research/selected-stock-rho-ledger/SOURCES.json +++ b/research/selected-stock-rho-ledger/SOURCES.json @@ -56,6 +56,12 @@ "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" }, + { + "path": "research/complex-double-replica-owners/PROOF.md", + "usage": "provenance", + "git_blob": "eb980efd5f34eb913714d1e6cb0860ced13ef1bb", + "sha256": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc" + }, { "path": "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py", "usage": "provenance", @@ -116,6 +122,18 @@ "git_blob": "81b330a4b886a0f4deab7b0811478bab3fbc107a", "sha256": "7f8338e748bcd42fbef1e7cc47b6c5040dfb3aad216e34759bcb12b8e14f7705" }, + { + "path": "research/punctured112-global/vendor/pr514/code/audit_async_invoice.py", + "usage": "provenance", + "git_blob": "568edf53a03fa3cfb854586c8f097dbc89a908ae", + "sha256": "04e29dab19cd659f42c926c5dba5ca72e5f789fb31d9fee45c22eb76b7689ac9" + }, + { + "path": "research/punctured112-global/vendor/pr514/vendor/audit_scalar_invoice.py", + "usage": "provenance", + "git_blob": "b03fdf510f19c9c8d2563d58747235c8c19e3596", + "sha256": "652eed65fe8f72ab486dcdbe761f401f8a2d43530f2fb0c5c7777be488cd4648" + }, { "path": "research/selected-bit-parent-reserve/README.md", "usage": "input", diff --git a/research/selected-stock-rho-ledger/TASK.json b/research/selected-stock-rho-ledger/TASK.json index b1be2d8584..aeed3be972 100644 --- a/research/selected-stock-rho-ledger/TASK.json +++ b/research/selected-stock-rho-ledger/TASK.json @@ -62,21 +62,15 @@ ] }, "scope_status": "refined", - "actual_scope": "Source-bind the non-complex terms of the selected m=73 row ledger (9909, 252, 1024), show they do not bind the leaf reserve rho in sigma <= (43/26)(1-s)(A+B) + rho, and settle rho from the merged selected complex layer (PR2287/PR3385 with PR2250, PR2234, PR2899) check it against all fourteen recorded stage guards, and say what the 9909 and 252 slots pay for in the selected layer.", + "actual_scope": "Source-bind the non-complex terms of the selected m=73 row ledger (9909, 252, 1024), show they do not bind the leaf reserve rho in sigma <= (43/26)(1-s)(A+B) + rho, and settle rho from the merged selected complex layer (PR2287/PR3385 with PR2250, PR2234, PR2899) check it against all fourteen recorded stage guards, and say what the 9909, 252 and 1024 terms pay for in the selected layer.", "scope_change_reason": "The card asks for an explicit envelope. #3113 and #3421 bound B and A for the m=73 producer and left rho as the only unbound term; this package addresses only rho. It finds rho = 0 conditionally on the merged selected-complex chain, whose authors mark parts of it as under review.", "bottleneck_link": "Inherited implementation obligation (H3 stock fit) for the selected result; it changes no supplier, kappa or cutoff. It prevents an external-ledger constant from being counted as a proved borrowed-stock coefficient.", "budget_minutes": 90, "stop_rule": "Stop once each ledger term is bound to source and every callee of the selected complex layer is classified from pinned source; do not re-derive the completed-callee proofs themselves.", "outcome": "partial", - "evidence": "verify.py: 62 exact checks over 15 pinned inputs plus three PR1087 tarball members (and twelve provenance pins), and 16 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... L_bits=2642 S_leaf=1 ... stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62. Local evidence outside verify.py (README, \"PR3385 replay and B1's fit\"): PR3385's registered replay fails on Windows only, at the frozen PR2753 verifier's path-separator check; with a local relative-path shim, which is not the registered replay, all three suites pass and all nine EVIDENCE.md receipt hashes match. B1 is fitted only at compact width (f-1)G >= 27,312,693 bits at q*, and elementary below that; neither branch takes caller row stock.", + "evidence": "verify.py: 62 exact checks over 15 pinned inputs plus three PR1087 tarball members (and fifteen provenance pins), and 16 mutation controls that must each be rejected. Marker PASS_SELECTED_STOCK_RHO_LEDGER ... L_bits=2642 S_leaf=1 ... stages=14 H_min=6562783 lean_row=6308 qadic_bit_row>=655356>20161 controls=16 checks=62. Local evidence outside verify.py (README, \"PR3385 replay and B1's fit\"): PR3385's registered replay fails on Windows only, at the frozen PR2753 verifier's path-separator check; with a local relative-path shim, which is not the registered replay, all three suites pass and all nine EVIDENCE.md receipt hashes match. B1 is fitted only at compact width (f-1)G >= 27,312,693 bits at q*, and elementary below that; neither branch takes caller row stock. Source reading outside verify.py (README, \"What the 1024 term pays for\"): 1024 is PR514's two-level row surcharge (halving depth 2 times the 512-bit precision payload), and no pinned source names a construction step for it. The selected layer reserves only L^D0(d) rows and supplies precision with guard bits (PR2287 L136-147, L374-380; PR3385 L190-201), so the term is inherited slack.", "author": "Mainzu", "ai_assistance": "Substantial assistance from Claude Code (Anthropic, Claude Opus 5.5) for source search, the verifier and drafting; no independent human review is claimed.", - "open_questions": [ - { - "question": "Which construction step uses the 1024 = 2*512 prefix term of the complex row?", - "why_it_matters": "It is the one ledger term this package binds only to the invoice.", - "first_step": "Trace charged_prefix_bits and row_prefix_extra in invoice_allcold.py to the construction notes.", - "blocked_by": "Nothing technical." - } - ] + "open_questions": [], + "no_open_questions_reason": "Every ledger term is now bound: 9909 and 252 are historical family charges, and 1024 is PR514's two-level row surcharge for the 512-bit precision payload. The selected layer's construction uses none of them, and rho = 0 is settled conditionally. No selected step bootstraps the m=73 layer, so further m=73 sigma work would only refine a consistency bound; the H3 envelope the record needs belongs to the bit producer (PR2084), outside this package." }