Independently audit BIT COPY support propagation at the retained caller

research/bit-copy-support-audit/FRAME-RANK-CROSS.json

@@ -0,0 +1,26 @@
+{
+  "checked_MOVE_events": 2904,
+  "checked_final_cap_equalities": 111,
+  "checked_frame_ranks": 636,
+  "inputs": {
+    "GEOMETRY": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022",
+    "WORD": "c46ccd7d3eedabc6a7efbb1a91ec13f2928bad8ee0bac57c6e593a092d13d96c"
+  },
+  "method": "independent Fraction Gaussian elimination with forward row reduction; no producer or submitted checker import",
+  "rank_census": {
+    "0": 1,
+    "1": 111,
+    "2": 153,
+    "4": 70,
+    "6": 180,
+    "7": 120,
+    "8": 1
+  },
+  "scope_excludes": [
+    "K/R coefficients",
+    "K-supported recipient projected ranks",
+    "decoded scalar endpoint",
+    "physical MOVE semantics"
+  ],
+  "status": "PASS"
+}

research/bit-copy-support-audit/INDEPENDENT-REVIEW.json

@@ -0,0 +1,112 @@
+{
+  "checked_utc": "2026-10-20T14:34:50.392487+00:00",
+  "cli_addendum": {
+    "change": "--output made optional, conditional receipt write; no mathematical or guard changes",
+    "final_code_sha256": "0c078ec9831c53c2671d398be9a991db34747fe76db1bf7691aaf2546d808826",
+    "final_normal_optimized_receipts_byte_equal": true,
+    "prior_code_sha256": "bb9afe457a4bb61881d12ad2b1969e62666a3c87434fbeb690ced9ee59fc6c4a"
+  },
+  "files": {
+    "FRAME-RANK-CROSS-V2.json": {
+      "bytes": 703,
+      "sha256": "9761d8b5fca1bbd8e0e5da956e9af47eecbcd71c7423bc531eb2e1b457f3e781"
+    },
+    "FRAME-RANK-CROSS.json": {
+      "bytes": 703,
+      "sha256": "9761d8b5fca1bbd8e0e5da956e9af47eecbcd71c7423bc531eb2e1b457f3e781"
+    },
+    "ORACLE-NORMAL.json": {
+      "bytes": 6495,
+      "sha256": "938b42ded10164d2d6e331f0592ae3f676e0d120ba3c9bc5c33545319226f8f7"
+    },
+    "ORACLE-OPT.json": {
+      "bytes": 6495,
+      "sha256": "938b42ded10164d2d6e331f0592ae3f676e0d120ba3c9bc5c33545319226f8f7"
+    },
+    "PROOF.md": {
+      "bytes": 15036,
+      "sha256": "e808578fb46b2eba8e407acd710ee214ae2e31bc02c72e189e592e60111c2ef5"
+    },
+    "REVIEW.md": {
+      "bytes": 5087,
+      "sha256": "2ed386bf3e9303005402408ac89f946547fe95663c6c78ac7cd896cffc087b29"
+    },
+    "SOURCE-NORMAL.json": {
+      "bytes": 10437,
+      "sha256": "930c7fe833fe5a8184f074a83ca03481f749ec8c5d7d9c47c2c30185cd8fad57"
+    },
+    "SOURCE-OPT.json": {
+      "bytes": 10437,
+      "sha256": "930c7fe833fe5a8184f074a83ca03481f749ec8c5d7d9c47c2c30185cd8fad57"
+    },
+    "SOURCE-V2-NORMAL.json": {
+      "bytes": 10437,
+      "sha256": "080f4a39d9cea4a37afb1df8626a0b7ef9fe15c0a0c9a614740c03d51146f270"
+    },
+    "SOURCE-V2-OPT.json": {
+      "bytes": 10437,
+      "sha256": "080f4a39d9cea4a37afb1df8626a0b7ef9fe15c0a0c9a614740c03d51146f270"
+    },
+    "frame_rank_cross.py": {
+      "bytes": 2803,
+      "sha256": "34aba82f60452cb341942f8f5577030fea4a74b804dad04e17fbae24cf08e91d"
+    },
+    "independent_oracle.py": {
+      "bytes": 11887,
+      "sha256": "58ead94a392f2f74d27f408fa98cf7077a0edae3e15352b7897759ee6197dfa3"
+    },
+    "oracle-NOTES.txt": {
+      "bytes": 4106,
+      "sha256": "5f80466e60f99250ef65f4c0b6cbd7eadc159f064b79196183f5679e2b9609c2"
+    },
+    "predecessor-PROOF.md": {
+      "bytes": 14738,
+      "sha256": "0993a370d83b7a3cae2fe98b8b36b274719f94c66ac189b2b87be118863762bd"
+    },
+    "source_check.py": {
+      "bytes": 10789,
+      "sha256": "0c078ec9831c53c2671d398be9a991db34747fe76db1bf7691aaf2546d808826"
+    }
+  },
+  "limits": [
+    "no full root-closure reconstruction",
+    "no K/R or K-supported recipient/projected ranks",
+    "no all-660-column endpoint replay",
+    "no physical MOVE/compiler/caller feasibility",
+    "no recursive invoice or precision or full outer theorem",
+    "no human or formal-kernel acceptance",
+    "no new kappa"
+  ],
+  "outstanding_findings": [],
+  "predecessor_head": "ddfc3133cbdf548e163c867d5671f8f01dd5d5ae",
+  "resolved_findings": [
+    {
+      "finding": "Required K-supported recipient and projected-recipient rank computations were attributed to the new checker, but it does not reconstruct K/R.",
+      "old_location": "PROOF.md original lines197-198",
+      "resolution": "Corrected proof separates all 636 frame ranks and 111 cap equalities from predecessor K-supported recipient/projected-rank evidence.",
+      "severity": "scope correctness"
+    }
+  ],
+  "reviewer": "separate OpenAI Codex agent; not human or formal-kernel acceptance",
+  "status": "PASS_SCOPED_AGENT_REVIEW_AFTER_SCOPE_CORRECTION",
+  "verification": {
+    "oracle_closed_walks": 1632,
+    "oracle_normal_exit": 0,
+    "oracle_optimized_exit": 0,
+    "oracle_receipts_byte_equal": true,
+    "oracle_symbolic_states": 34208,
+    "oracle_transitions": 317824,
+    "source_ADD_events": 36005,
+    "source_MOVE_events": 2904,
+    "source_cap_equalities": 111,
+    "source_checker_normal_exit": 0,
+    "source_checker_optimized_exit": 0,
+    "source_final_cli_no_output_optimized_exit": 0,
+    "source_frame_ranks": 636,
+    "source_receipts_byte_equal": true,
+    "source_records": 38927,
+    "third_rank_cross_exit": 0,
+    "tiny_closure_states": 283,
+    "tiny_closure_transitions": 1780
+  }
+}

research/bit-copy-support-audit/INDEPENDENT-REVIEW.md

@@ -0,0 +1,21 @@
+# Independent scoped review
+
+Status: PASS after the one scope correction recorded below. This is an additional OpenAI Codex agent review, not human acceptance or a formal-kernel proof.
+
+Reviewed the fixed-L paired-execution induction, branch intervention/decomposition, closed nested-walk dimension inequality, finite-branch projection argument, literal-source applicability checker, and separately written finite oracle. The audited predecessor is Ross Richardson's PR4200 at `ddfc3133cbdf548e163c867d5671f8f01dd5d5ae`.
+
+The paired-run invariant is valid when the public schedule and frames are fixed, the compared public initial values agree, changed private injections occur only at frames containing L, and every actual data dependency preserves containment of L. Identical dirty initial values may be arbitrarily correlated. In the scalar-linear specialization, suppressing a branch's increments isolates its coefficient even when q is itself a linear functional of the dirty/public input; changing q at its ordinary source would be a different experiment. Cancellation can remove nonzero coefficients but cannot violate the invariant. Upward public MOVE and common-frame ADD are sufficient edge restrictions; the proof correctly avoids claiming they are necessary for every possible globally cancelling program.
+
+For a closed nested private walk, the running intersection loses at most each downward codimension, and total downward charge equals half the all-direction charge. The projected-root dimension and finite-union inequalities follow conditionally on the required recipient rank evidence. The rank-seven floor is explicitly credited to the predecessor. The relaxed downward-MOVE and unequal-frame-ADD controls violate the named restrictions; they are not bugs in the predecessor or admitted original words.
+
+An initial proof bullet overstated the new source check by saying it computed required K-supported recipient and projected-recipient ranks. The checker does not reconstruct K/R, so that was a real scope error. The corrected proof now explicitly leaves those ranks as predecessor evidence and states the newly executed rank checks precisely. The change is confined to that applicability/coverage wording. No unresolved correctness finding remains within the declared scope.
+
+Verification performed independently:
+
+- Source applicability checker, normal and optimized Python: both exit zero and byte-identical 10,437-byte receipts (SHA256 `080f4a39d9cea4a37afb1df8626a0b7ef9fe15c0a0c9a614740c03d51146f270`). It authenticates raw WORD/GEOMETRY inputs and checks 38,927 records, including 2,904 upward MOVEs and 36,005 common-frame ADDs. The exact postscatter interval, immutable nine source registers, target non-source property, and final cap equalities are checked. The finite difference-state closure has 283 states and 1,780 transition occurrences; six nonzero-q relaxation failures and four legal double-read cancellations behave as claimed.
+- Separately authored oracle, normal and optimized Python: both exit zero and byte-identical 6,495-byte receipts (SHA256 `938b42ded10164d2d6e331f0592ae3f676e0d120ba3c9bc5c33545319226f8f7`). It checks 34,208 admissible symbolic states, 317,824 transitions, and 1,632 closed walks across two eight-frame rational families. Dirty/cancellation and named hypothesis-relaxation controls are meaningful. Runtime checks use explicit exceptions, so optimized mode retains them.
+- A third, review-only Fraction Gaussian-elimination script imports neither implementation. It independently recomputes all 636 catalog-frame ranks, agrees with every submitted rank, checks all 2,904 MOVE rank differences, and establishes all 111 rank-seven root-orthogonal final cap equalities. This corroborates the new check's finite geometry, not K/R coefficients or physical MOVE semantics.
+
+Unreviewed obligations remain complete root closures, K/R and K-supported recipient ranks, all 660 decoded columns/full endpoint semantics, physical MOVE/compiler/caller feasibility, the recursive invoice, precision, and the full outer multiplication theorem. No selected-result or kappa improvement is established. Source credit remains with Ross Richardson and his review agent for the obstruction/projection argument and with Ali Romman, Sagar Thakrar, DreamingOfClouds/eumemic, PR589/PR555, and the retained NOTICE lineage for source word/transport. Historical decoder-floor credit is distinct and retained in the proof.
+
+Final CLI addendum: the source checker made `--output` optional and conditionally writes the receipt. This changes no mathematical recurrence or guard. Both final-code output modes replayed successfully, normal/optimized JSON bytes agree, and a no-output optimized invocation also passed. The previous receipt hash `930c7fe833fe5a8184f074a83ca03481f749ec8c5d7d9c47c2c30185cd8fad57` belongs to the prior CLI code and is preserved separately. The final source-checker SHA256 is `0c078ec9831c53c2671d398be9a991db34747fe76db1bf7691aaf2546d808826`; proof SHA256 is `e808578fb46b2eba8e407acd710ee214ae2e31bc02c72e189e592e60111c2ef5`.

research/bit-copy-support-audit/ORACLE-NOTES.txt

@@ -0,0 +1,63 @@
+Independent support-propagation oracle
+====================================
+
+Scope: this interpreter was written without reading any primary implementation
+or predecessor verifier. The only predecessor mathematics read was PROOF.md at
+PR4200 commit ddfc3133cbdf548e163c867d5671f8f01dd5d5ae. Guidance was read from
+the session checkout at canonical-main 12fa8c5c844be21bfefb38a19503fbd867a11244.
+
+Assumptions of the support statement:
+1. A snapshot q is unchanged by reads. Geometry is over Q, coefficient algebra
+   over F2. Arbitrary dirty public inputs have independent formal columns.
+2. L is contained in every private frame visited, including every read frame.
+3. A private read adds scalar*q to a public receiver at exactly the same frame.
+4. Public MOVE preserves the normalized decoded linear form and only moves to
+   a containing frame; public ADD uses two exactly equal current frames.
+5. Operations are a fixed finite linear schedule, or one may separately apply
+   the argument to each fixed schedule. Arbitrary data-dependent frame choices
+   do not automatically have a single F2-linear matrix interpretation.
+
+Written induction (all dimensions/register counts; not a formal-kernel proof):
+For each public register R, mark its q coefficient. Initially all marks are
+zero, so the invariant 'a nonzero mark implies L <= frame(R)' holds. At a
+private read, the recipient frame is the private read frame and contains L.
+An upward MOVE preserves the mark and containment by transitivity. Equal-frame
+ADD changes one mark by a scalar multiple of another mark, whose frame is the
+same recipient frame. If the resulting mark is nonzero, at least one input
+mark was nonzero and supplies the needed containment. Cancellation may remove
+a mark; it cannot create a marked frame outside this set. This inductive proof
+covers any finite number of private reads, public ADDs, and loops/revisits in
+the fixed schedule. It does not assume zero dirty public inputs or source/helper
+restoration; such constraints can restrict, but not enlarge, this support set.
+
+Private intersection bound: for every visited frame take the running meet.
+An upward nested step cannot shrink it; a downward rank-d step shrinks its
+dimension by at most d. A closed walk has equal total up/down dimension change,
+so dim(L) >= dim(G) - m/2 for entrance G and all-direction rank sum m.
+
+Finite checks: two eight-frame lattices in Q^3, one coordinate and one generated
+by a genuinely rational noncoordinate basis. For every possible L, every ordered
+pair of public frames, and every pair of 3-column linear forms satisfying the
+support invariant, exhaust all admissible 0/1 scalar reads, equal-frame scalar
+ADDs and upward MOVE targets. Independent dirty columns range over every F2
+linear combination in these finite states. Separately enumerate every strict
+nested closed private walk of zero through four edges in each family. The
+five-operation cancellation loop restores both dirty inputs for all eight
+concrete q/a/b assignments. Dropping either public monotonicity or frame
+equality gives an explicit q coefficient in the zero frame while L is a line.
+Those are counterexamples to relaxed hypotheses, not predecessor bugs.
+
+Remaining: no actual R438 event binding, no query-rank/paid-moment certification,
+no arbitrary rational-geometry exhaustive search, no arbitrary-characteristic
+specialization, no physical compiler/caller/invoice/precision/outer theorem.
+The all-parameter contribution is the short written support induction above;
+the finite enumeration only corroborates it and isolates its hypotheses.
+
+Attribution: Ross Richardson (RossRichardson), PR4200, supplies the source support argument and the
+actual R438 context, with Ali Romman, Sagar Thakrar, DreamingOfClouds/eumemic,
+PR589/PR555 and the retained source NOTICE lineage. This independent oracle
+uses substantial OpenAI Codex assistance; Apache-2.0 repository contribution.
+
+Replay:
+python3 -I -B independent_oracle.py --out /tmp/independent-support-result.json
+python3 -I -O -W error -B independent_oracle.py --out /tmp/independent-support-result-O.json

research/bit-copy-support-audit/ORACLE-PROVENANCE.json

@@ -0,0 +1,31 @@
+{
+  "commands": [
+    "python3 -I -B independent_oracle.py --out RESULT.json",
+    "python3 -I -O -W error -B independent_oracle.py --out RESULT-O.json"
+  ],
+  "file_sha256": {
+    "NOTES.txt": "5f80466e60f99250ef65f4c0b6cbd7eadc159f064b79196183f5679e2b9609c2",
+    "RESULT-O.json": "938b42ded10164d2d6e331f0592ae3f676e0d120ba3c9bc5c33545319226f8f7",
+    "RESULT.json": "938b42ded10164d2d6e331f0592ae3f676e0d120ba3c9bc5c33545319226f8f7",
+    "independent_oracle.py": "58ead94a392f2f74d27f408fa98cf7077a0edae3e15352b7897759ee6197dfa3"
+  },
+  "guards": "explicit RuntimeError; no assert in independent_oracle.py",
+  "normal_optimized_results_byte_identical": true,
+  "python": "3.12.14",
+  "source_head": "ddfc3133cbdf548e163c867d5671f8f01dd5d5ae",
+  "source_main_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "source_pr": 4200,
+  "source_sha256": {
+    "AGENTS.md": "eb25d8ec495b80190a4b1a634710819bb74f0fae88d5203285c2b75b6f147347",
+    "CONTRIBUTING.md": "8a49fe97e2ad088a2b2e0c5b222aaab08752783b1f9c1260790d7dd13011d215",
+    "autoresearch.md": "8c98d179208c34a8c6768931e13f3bbeaa1cb63d59c660799ffde05c40935d9b",
+    "research/bit-copy-path/construction/PROOF.md": "0993a370d83b7a3cae2fe98b8b36b274719f94c66ac189b2b87be118863762bd"
+  },
+  "status": "PASS",
+  "retained_original_to_package": {
+    "NOTES.txt": "ORACLE-NOTES.txt",
+    "RESULT.json": "ORACLE-RESULT.json",
+    "RESULT-O.json": "ORACLE-RESULT.json",
+    "independent_oracle.py": "independent_oracle.py"
+  }
+}