[ToikY]

This lowers the dense guard scan already proposed in PR4100 to an explicit three-tape finite-control program. Given an admitted ordered finite-alphabet stencil, it enumerates all M=2^L addresses, writes an owned BAD mask, preserves the stencil, blanks private counter data/right marker and returns every head. The written proof derives exactly 8ML+15M+13L+18 cell/head actions and M+2L+6 visited cells. Finite alphabet/control gives a constant-factor bit-machine lowering. O(ML)=O(V) uses the source’s L=Theta(p), R=Theta(p), V=MR premises.

The geometry/threshold/stencil producer and admission path are unpriced host adapters. This is the detector from a supplied stencil, with no E callback. It does not price exception extraction, inverse keys, sorting, payload routing, reinsertion, ordinary callees, full E/CRT, precision/native/outer composition or a new κ.

Validation: eight normal/optimized registered checks pass. Primary executes6,525,207 literal actions over49,408 complete source-bound addresses, plus all-SKIP small-counter cases. A separate preimplementation oracle covers49,152 addresses/196,608 parity and spectator toggles/12 boundaries. A pinned comparison checks all49,408 masks plus181 generic stencils/1,300 addresses; a separate cost checker covers14 cases/2,058 addresses and detects an underbilled READ without changing output or ownership. Real mutants detect wrong thresholds/significance, unadjusted full-K guard tests, a skipped counter bit and omitted owned-output return. All three canonical source inputs stay unchanged. Finite evidence corroborates the quantified proof; it is not full caller acceptance.

Reproduce with Python3.12/standard library: python3.12 -B scripts/research_package.py --package research/crt-dense-guard-scan. Exact scope, source pins, conditional input contract and next questions are retained in TASK.json, PROOF.md and EVIDENCE.md. Smallest follow-up: construct and admit the ordered stencil at the transported source caller with every producer/consumer step charged.

Task uniform-transfer-audit, refined scope 0593fcf1b94f3cd8f1be, priority7, canonical base/current main 12fa8c5c844be21bfefb38a19503fbd867a11244. Before submission, complete pagination covered316 open/draft PR bodies plus current hub/4173 and focused dense-guard Discussion search; broader code/closed/Discussion coverage is partial. PR4197’s staged-word forests, PR4198’s Stein producer and PR4200’s BIT COPY floor address distinct obligations.

Credit: Cinna Davis already supplies the predicate and ordered-scan proposal in CRT.md238–253; Hiroki KUMAZAKI (@kumagi), PR4169 at835c3563ee7ede8ceaf329ede7372e50f7823136 and PR4174 at5fec853f0c048871de3b8098d1e30d4ee19cda23, supplies repair and placement/descriptor work with scan tariffs left open. Douglas Colkitt/OpenAI framework and complete retained source NOTICE lineage are preserved. Substantial OpenAI Codex assistance, including separate-agent semantic and cost review; no independent human/formal-kernel acceptance. Apache-2.0. No merge/frontier change; maintainer edits disabled.

Exact published head 4f49743a9df0cf7501cdc62bd5707a122fa071e9 passed the24-file committed-byte/source-history preflight and all eight checks from a Git-free export of the committed bytes. All exported package/input bytes stayed unchanged.

[rcfc-jreed]

Independent scoped audit of the literal three-tape CRT guard scan at 4f49743a: no defect found in the finite cost / fixture / seal layer

Code-disjoint reimplementation; does not import package machine.py / verify.py / cost_check.py / cross_check.py. Package bytes from head 4f49743a9df0cf7501cdc62bd5707a122fa071e9 via GitHub contents API. CLAIM.

What passes (18 of 18):

1. Pins / seals. Base 12fa8c5c…. RESULT/COST/CROSS/REPORT/PRIMARY/INITIAL all PASS. machine.py binds COST kernel + REPORT/PRIMARY seals; README metadata-only addendum documented.
2. Cost formulas. All 14 COST rows: actions=8ML+15M+13L+18, visited=M+2L+6, R+W+Mv equality; underbilled READ fault present.
3. Fixtures. Three source fixtures, 49408 addresses, 6525207 total actions; good+bad=addresses; heads returned / private blank. All-skip boundaries match COST rows.
4. Cross / controls. Dual CROSS runs agree with RESULT masks/actions; generic 181/1300; semantic/ownership/counter mutants + unpriced adapter rejections present.

Not covered: geometry→stencil admission production; full E evaluator; live machine re-execution; new κ.

This is a finite replay of committed receipts, not a formal proof.

check_4201.py

#!/usr/bin/env python3
"""Independent finite controls for PR4201 (literal three-tape CRT guard scan).

Recomputes cost affine formulas, fixture address/action totals, and review seals.
Does not import package machine.py / verify.py / cost_check.py / cross_check.py.

Package head 4f49743a9df0cf7501cdc62bd5707a122fa071e9 via GitHub API.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).
Apache-2.0.
"""
from __future__ import annotations

import argparse, hashlib, json, sys
from pathlib import Path

HEAD = "4f49743a9df0cf7501cdc62bd5707a122fa071e9"
BASE = "12fa8c5c844be21bfefb38a19503fbd867a11244"
results = []


def check(name, ok, detail=""):
    results.append((name, bool(ok), detail))
    print(("PASS " if ok else "FAIL ") + name + ((": " + str(detail)) if detail else ""), flush=True)
    return bool(ok)


def load(pkg, name):
    return json.loads((pkg / name).read_text(encoding="utf-8"))


def sha(path: Path):
    return hashlib.sha256(path.read_bytes()).hexdigest()


def total_actions(M, L):
    return 8 * M * L + 15 * M + 13 * L + 18


def visited_cells(M, L):
    return M + 2 * L + 6


def run(pkg: Path):
    sources = load(pkg, "SOURCES.json")
    task = load(pkg, "TASK.json")
    verify = load(pkg, "VERIFY.json")
    result = load(pkg, "RESULT.json")
    cost = load(pkg, "COST-CHECK-RESULT.json")
    cross = load(pkg, "CROSS-REPLAY.json")
    report = load(pkg, "REPORT.json")
    primary = load(pkg, "PRIMARY-REVIEW.json")
    initial = load(pkg, "INITIAL-REVIEW.json")

    check("I1 SOURCES/TASK/RESULT/REPORT/PRIMARY base_commit == 12fa8c5c…",
          sources["base_commit"] == BASE == task["base_commit"] == result["base_commit"]
          == report["base_commit"] == primary["base_commit"] == initial["base_commit"])
    check("I2 RESULT PASS_LITERAL_DENSE_GUARD_MASK; VERIFY ready; TASK completed",
          result["result"] == "PASS_LITERAL_DENSE_GUARD_MASK"
          and verify["status"] == "ready"
          and task["outcome"] == "completed")
    check("I3 COST PASS_INDEPENDENT_LITERAL_GUARD_COST; CROSS normal≡optimized; REPORT PASS",
          cost["result"] == "PASS_INDEPENDENT_LITERAL_GUARD_COST"
          and cross["status"] == "PASS_INDEPENDENT_CROSS_NORMAL_OPTIMIZED"
          and report["status"] == "PASS_INDEPENDENT_LITERAL_DENSE_GUARD_COST_INTERFACE_REVIEW"
          and primary["status"] == "PASS_SCOPED_INDEPENDENT_SEMANTIC_REVIEW"
          and initial["status"] == "PASS_PREIMPLEMENTATION_GUARD_REVIEW")

    check("P1 COST.kernel_sha256 == machine.py; REPORT primary file seals match",
          cost["kernel_sha256"] == sha(pkg / "machine.py")
          and all(sha(pkg / Path(r["path"]).name) == r["sha256"]
                  for r in report["primary_files_reviewed"]))
    bad_pri = [rel for rel, dig in primary["reviewed_primary_sha256"].items()
               if sha(pkg / rel) != dig]
    check("P2 PRIMARY reviewed_primary_sha256 matches current primary files",
          not bad_pri, bad_pri)
    add = primary["metadata_addendum"]
    check("P3 README metadata-only addendum: integrated sha matches; original recorded",
          add["status"] == "PASS_EXACT_METADATA_ONLY_INTEGRATION_DIFF"
          and add["integrated_readme_sha256"] == sha(pkg / "README.md")
          and add["original_readme_sha256"] == primary["original_reviewed_primary_sha256"]["README.md"]
          and add["other_five_primary_hashes_unchanged"] is True)
    bad_ret = [rel for rel, dig in primary["retained_review_files_sha256"].items()
               if sha(pkg / rel) != dig]
    check("P4 PRIMARY retained review-file seals match", not bad_ret, bad_ret)

    # Cost formulas
    bad_c = []
    for row in cost["rows"]:
        M, L = row["M"], row["L"]
        if (row["actions"] != total_actions(M, L)
                or row["visited_cells"] != visited_cells(M, L)
                or row["reads"] + row["writes"] + row["moves"] != row["actions"]):
            bad_c.append(row["name"])
    check("F1 all 14 COST rows: actions=8ML+15M+13L+18; visited=M+2L+6; R+W+Mv=actions",
          not bad_c and cost["cases"] == 14 == len(cost["rows"]), bad_c)
    check("F2 REPORT exact_quantified_counts state the same affine formulas",
          report["exact_quantified_counts"]["total_cell_head_actions"] == "8ML+15M+13L+18"
          and report["exact_quantified_counts"]["visited_cells_including_all_markers"] == "M+2L+6")
    ub = cost["cost_fault_controls"]
    check("F3 underbilled READ cost-fault control present (invoice detection)",
          len(ub) == 1 and "READ omitted" in ub[0]["name"])

    # RESULT fixtures
    fixtures = result["fixtures"]
    check("R1 three source fixtures; addresses sum 49408; good+bad=addresses each",
          len(fixtures) == 3
          and sum(f["addresses"] for f in fixtures) == 49408
          == primary["source_fixture_addresses_per_cross_run"]
          and all(f["good_addresses"] + f["bad_addresses"] == f["addresses"] for f in fixtures)
          and all(f["heads_returned"] and f["private_data_blank"] for f in fixtures))
    check("R2 fixture total_cell_head_actions == reads+writes+moves; sum actions 6525207",
          all(f["total_cell_head_actions"] == f["read_actions"] + f["write_actions"] + f["move_actions"]
              for f in fixtures)
          and sum(f["total_cell_head_actions"] for f in fixtures) == 6525207)
    # all-skip boundaries match cost all_skip rows by mask sha
    skips = {r["mask_sha256"]: r for r in cost["rows"] if r["name"] == "all_skip"}
    bad_s = []
    for b in result["all_skip_boundaries"]:
        row = skips.get(b["mask_ascii_sha256"])
        if not row or row["actions"] != b["total_cell_head_actions"] or row["visited_cells"] != b["visited_cells_including_owned_mask"]:
            bad_s.append(b["address_bits"])
    check("R3 all_skip_boundaries match COST all_skip rows by mask sha / actions / visited",
          not bad_s and len(result["all_skip_boundaries"]) == 3, bad_s)

    # Negative controls present
    neg = result["negative_controls"]
    check("N1 negative controls: semantic/ownership/counter mutants + unpriced adapter rejections",
          len(neg["semantic_mutants"]) >= 1
          and len(neg["ownership_mutants"]) >= 1
          and len(neg["counter_mutants"]) >= 1
          and len(neg["unpriced_adapter_rejections"]) >= 4)

    # CROSS replay consistency
    check("X1 both CROSS runs exit 0; source fixtures match RESULT masks/actions; generic 181/1300",
          len(cross["runs"]) == 2
          and all(run["exit_code"] == 0 for run in cross["runs"])
          and all(run["receipt"]["source_fixture_addresses"] == 49408 for run in cross["runs"])
          and all(run["receipt"]["generic_stencils"]["cases"] == 181
                  and run["receipt"]["generic_stencils"]["addresses"] == 1300
                  for run in cross["runs"]))
    # compare first run source fixtures to RESULT
    xf = cross["runs"][0]["receipt"]["source_fixtures"]
    by_mask = {f["mask_ascii_sha256"]: f for f in fixtures}
    bad_x = []
    for row in xf:
        f = by_mask.get(row["mask_ascii_sha256"])
        if not f or f["addresses"] != row["addresses"] or f["total_cell_head_actions"] != row["observed_actions"]:
            bad_x.append(row["name"])
    check("X2 CROSS source fixture masks/addresses/actions match RESULT fixtures", not bad_x, bad_x)

    check("NEG1 claiming geometry/admission production or full E is outside RESULT limitations/REPORT obligations",
          any("stencil" in x.lower() or "admitted" in x.lower() for x in result["limitations"])
          and report["material_defects_remaining"] == [])

    failed = [name for name, ok, _ in results if not ok]
    print(f"\n{len(results) - len(failed)}/{len(results)} PASS", flush=True)
    if failed:
        print("FAILED:", ", ".join(failed), flush=True)
        return 1
    return 0


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--pkg", required=True)
    ap.add_argument("--expect-head", default=HEAD)
    args = ap.parse_args()
    check("HEAD pin recorded (API fetch)", args.expect_head == HEAD, args.expect_head)
    return run(Path(args.pkg))


if __name__ == "__main__":
    sys.exit(main())

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).

[rcfc-jreed]

Independent scoped audit of #4201 CRT dense-guard three-tape scan at 4f49743a: 16/16

Code-disjoint checks; nested PACKAGE/ROOT forks of verify.py, independent_guard_oracle.py, cross_check.py, and cost_check.py. Head 4f49743a9df0cf7501cdc62bd5707a122fa071e9. CLAIM.

No packaging defect in SOURCES scope. All 5 digests match.

What passes: sealed RESULT / COST-CHECK-RESULT / CROSS-REPLAY / REPORT PASS tokens; fresh forks regenerate matching PASS results for all four VERIFY entrypoints.

Not covered here: Lean; new κ; merge/close; geometry/admission as a priced production placement theorem.

Finite pin/seal/tape-scan replay ≠ formal proof.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).