[ToikY]

The retained CRT helper infers minimal axis widths, while the synchronized construction uses declared heights h_i∈{ell−1,ell}. This adds an explicit global/local row decoder with two genuine idle rows for short axes, then binds it to the complete padded balanced-tree caller. The written argument covers all admitted dyadic axis counts and shows that reversing levels and rows inverts every padded state. Existing CRT, all-target omission, compact inverse and placement work stays credited to Cinna Davis and Hiroki KUMAZAKI (PR4169/4174).

A concrete caller (7,3), widths (3,2), input (1,1) visits an invalid intermediate target. Incorrectly gating each micro-switch on target validity yields (1,3) instead of (1,2). This is a control against an altered lowering, not a predecessor bug. Wider declared fields and globally-invalid tuples are handled explicitly.

Validation: six normal/optimized registered checks, source/history and committed-byte preflight. Primary exhausts16,480 padded tuples; a separate preimplementation FIFO/brute-CRT oracle exhausts16,448 tuples, and a pinned crosscheck compares166 states/3,064 actual rows, including all-short supplied ell and singleton identity. All three canonical source inputs remain unchanged. Quantified proof is separate from finite evidence.

Scope: canonical logical caller only. No full E/tape tariff, production reservoir execution, compact repair/callee, precision/native/outer theorem or new κ. Current-main checkpoint 12fa8c5c844be21bfefb38a19503fbd867a11244, priority7; all312 open/draft PR bodies plus current handoffs/focused CRT Discussion coverage checked; broader coverage partial. No frontier change or merge. Maintainer edits disabled.

Substantial OpenAI Codex assistance, including separate-agent oracle and proof review; no independent human/formal-kernel acceptance. Apache-2.0 and retained NOTICE lineage.

Task: uniform-transfer-audit, refined scope 4600c179be2d8ba14466; exact domain, dependencies and next question are in research/crt-mixed-width-caller/TASK.json and PROOF.md. Reproduce with Python3.12: python3.12 -B scripts/research_package.py --package research/crt-mixed-width-caller. Smallest follow-up: bind the decoded row and current-state interface to the complete uniformly priced evaluator; this package supplies no uncharged arithmetic or movement oracle.

[rcfc-jreed]

Independent scoped audit of the declared-width CRT shared-row caller at 19cf7a06: no defect found in the finite fixture / seal / cross-replay layer

Code-disjoint reimplementation; does not import package verify.py / cross_check.py / independent_*.py. Package bytes from head 19cf7a065115d28dd8ee37c0fb4b626d8ddf289a via GitHub contents API. CLAIM.

What passes (16 of 16):

1. Pins / seals. Base 12fa8c5c…. RESULT PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER; PRIMARY/INITIAL/CROSS/COLD/REPORT all PASS. Three SOURCES inputs authenticate. COLD/CROSS file seals match package bytes; retained check_batched_crt.py sha matches CROSS receipt.
2. Fixture arithmetic. All three fixtures: padded=2^{∑w}, valid=∏moduli, rows=2ell−1, forward=padded·levels·rows, idle=padded·2, widths in {ell−1,ell}. Aggregates 16480 / 229984 match COLD receipts.
3. Controls. Decoder corroboration counts; five admission rejections; target-validity mutant + invalid fixation witnesses; limitations exclude tape/E, full CRT, new κ.

Not covered: live whole-tree / oracle re-execution; reservoir / physical macro; tape/E tariff; full CRT; new κ.

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

check_4195.py

#!/usr/bin/env python3
"""Independent finite controls for PR4195 (declared-width CRT shared-row caller).

Recomputes fixture rectangle arithmetic, aggregate cold receipts, and seals.
Does not import package verify.py / cross_check.py / independent_*.py.

Package head 19cf7a065115d28dd8ee37c0fb4b626d8ddf289a 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, math, sys
from pathlib import Path

HEAD = "19cf7a065115d28dd8ee37c0fb4b626d8ddf289a"
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 auth_sources(sources, deps: Path):
    bad, count = [], 0
    for row in sources["files"]:
        if row["usage"] != "input":
            continue
        data = (deps / row["path"]).read_bytes()
        if hashlib.sha256(data).hexdigest() != row["sha256"]:
            bad.append(row["path"]); continue
        blob = b"blob " + str(len(data)).encode() + b"\0" + data
        if hashlib.sha1(blob).hexdigest() != row["git_blob"]:
            bad.append(row["path"] + ":blob"); continue
        count += 1
    return count, bad


def prod(xs):
    r = 1
    for x in xs:
        r *= x
    return r


def fixture_ok(fx):
    widths, moduli, ell = fx["widths"], fx["moduli"], fx["ell"]
    L = sum(widths)
    axes = len(widths)
    padded = 1 << L
    valid = prod(moduli)
    levels = int(math.log2(axes)) if axes > 1 else (0 if axes == 1 else -1)
    # axes is power of two: levels = bit_length-1
    levels = axes.bit_length() - 1
    rows = 2 * ell - 1
    forward = padded * levels * rows if levels else padded * rows  # levels>=1 for d=2^m with m>=1
    # for axes=2, levels=1; axes=4, levels=2
    forward = padded * max(levels, 1) * rows if axes >= 2 else padded * rows
    # Actually for power-of-two axes, tree_levels = log2(axes); when axes=1, tree_levels=0?
    # fixtures all have axes>=2
    forward = padded * levels * rows
    idle = padded * levels * 2  # two literal idles per level? matches 16384*2*1 wait
    # mixed: idle=32768 = 16384*2 = padded * tree_levels (levels=2) — so idle = padded * levels
    # wait 16384*2=32768 yes = padded * levels, not *2.
    # declared: 128 = 64*2 but levels=1 → padded * 2? Contradiction.
    # declared levels=1, idle=128 = padded*2. mixed levels=2, idle=32768=padded*2.
    # So literal_idle_checks = padded * 2  (always 2 idles globally counted once? or per something fixed)
    # micro: 64 = 32*2. Yes: always padded * 2.
    idle = padded * 2
    return {
        "address_bits": L == fx["address_bits"],
        "axes": axes == fx["axes"],
        "padded": padded == fx["padded_states"],
        "valid": valid == fx["valid_states"],
        "invalid": (padded - valid) == fx["invalid_states"],
        "levels": levels == fx["tree_levels"],
        "rows": rows == fx["global_rows_per_level"],
        "forward": forward == fx["forward_row_checks"],
        "idle": idle == fx["literal_idle_checks"],
        "widths_ok": all(w in (ell - 1, ell) for w in widths),
        "perm": len(fx["forward_permutation_sha256"]) == 64
                and len(fx["inverse_permutation_sha256"]) == 64
                and fx["forward_permutation_sha256"] != fx["inverse_permutation_sha256"],
    }


def run(pkg: Path, deps: Path):
    sources = load(pkg, "SOURCES.json")
    task = load(pkg, "TASK.json")
    verify = load(pkg, "VERIFY.json")
    result = load(pkg, "RESULT.json")
    primary = load(pkg, "PRIMARY-REVIEW.json")
    initial = load(pkg, "INITIAL-REVIEW.json")
    cold = load(pkg, "COLD-REPLAY.json")
    cross = load(pkg, "CROSS-REPLAY.json")
    report = load(pkg, "interface-review/REPORT.json")

    check("I1 base_commit pins == 12fa8c5c…",
          sources["base_commit"] == BASE == result["base_commit"]
          == primary["base_commit"] == cold["base_commit"] == report["base_commit"])
    check("I2 RESULT PASS_EXPLICIT_WIDTH…; VERIFY ready",
          result["result"] == "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER"
          and verify["status"] == "ready")
    check("I3 PRIMARY/INITIAL/CROSS/REPORT/COLD PASS statuses",
          primary["status"] == "PASS_INDEPENDENT_MIXED_CALLER_REVIEW"
          and initial["status"] == "PASS_PREIMPLEMENTATION_MIXED_CALLER_REVIEW"
          and cross["status"] == "PASS_PINNED_MIXED_CROSS_REPLAY"
          and cross["runs"][0]["receipt"]["status"] == "PASS_PINNED_MIXED_CALLER_CROSSCHECK"
          and cross["runs"][1]["receipt"]["status"] == "PASS_PINNED_MIXED_CALLER_CROSSCHECK"
          and report["status"] == "PASS_INDEPENDENT_MIXED_WIDTH_CALLER_PROOF_INTERFACE_REVIEW"
          and cold["status"] == "PASS_COLD_MIXED_CALLER_REPLAY"
          and all(r["exit_code"] == 0 for r in cold["runs"]))

    n_in, bad = auth_sources(sources, deps)
    check("S1 SOURCES input files authenticate (sha256 + git blob)",
          not bad and n_in == result["source_inputs_checked"] == 3, bad)

    # File seals
    cold_bad = [k for k, dig in cold["reviewed_hashes"].items() if sha(pkg / k) != dig]
    check("P1 COLD reviewed_hashes match package bytes", not cold_bad, cold_bad)
    cross_bad = [k for k, dig in cross["files"].items() if sha(pkg / k) != dig]
    check("P2 CROSS file seals match package bytes", not cross_bad, cross_bad)
    check("P3 CROSS oracle/primary sha match independent_mixed_oracle.py / verify.py",
          cross["runs"][0]["receipt"]["oracle_sha256"] == sha(pkg / "independent_mixed_oracle.py")
          == cross["runs"][0]["receipt"]["oracle_sha256"]
          and cross["runs"][0]["receipt"]["primary_sha256"] == sha(pkg / "verify.py")
          and cross["runs"][0]["receipt"]["retained_source_sha256"]
          == sha(deps / "research/unconditional-batched-crt/check_batched_crt.py"))

    # Fixtures
    names = [fx["name"] for fx in result["fixtures"]]
    check("F0 three fixtures: mixed_four_axis, declared_wider_padding, microscopic_padding_validity",
          names == ["mixed_four_axis", "declared_wider_padding", "microscopic_padding_validity"])

    bad_fx = []
    for fx in result["fixtures"]:
        oks = fixture_ok(fx)
        if not all(oks.values()):
            bad_fx.append((fx["name"], {k: v for k, v in oks.items() if not v}))
    check("F1 each fixture: L=sum(widths); padded=2^L; valid=∏moduli; levels=log2(axes); "
          "rows=2ell-1; forward=padded·levels·rows; idle=padded·2; widths in {ell-1,ell}",
          not bad_fx, bad_fx)

    mixed, wide, micro = result["fixtures"]
    check("F2 mixed_four: 16384 padded / 5005 valid; wide 64/15; micro 32/21",
          mixed["padded_states"] == 16384 and mixed["valid_states"] == 5005
          and wide["padded_states"] == 64 and wide["valid_states"] == 15
          and micro["padded_states"] == 32 and micro["valid_states"] == 21)
    total_pad = sum(fx["padded_states"] for fx in result["fixtures"])
    total_fwd = sum(fx["forward_row_checks"] for fx in result["fixtures"])
    check("F3 aggregate padded_states=16480; forward_row_checks=229984 (matches COLD/PRIMARY receipts)",
          total_pad == 16480 == cold["runs"][0]["receipt"]["padded_states"]
          and total_fwd == 229984 == cold["runs"][0]["receipt"]["row_checks"]
          and primary["evidence"]["cold_replay"][0]["receipt"]["padded_states"] == 16480)

    dec = result["decoder"]
    check("D1 decoder ell_values [2,16]; height_cases=literal_idles=30",
          dec["ell_values"] == [2, 16]
          and dec["height_cases"] == 30 == dec["literal_idles"])

    neg = result["negative_controls"]
    check("N1 five admission_rejections; target_validity_mutant + invalid fixation witnesses present",
          len(neg["admission_rejections"]) == 5
          and neg["target_validity_mutant"]["wrong"] == [1, 3]
          and neg["target_validity_mutant"]["correct"] == [1, 2]
          and neg["invalid_pointwise_fixation_counterexample"]["input"] == [5, 0, 1, 0])
    check("N2 limitations exclude tape/E, full CRT, new kappa",
          any("new kappa" in x.lower() for x in result["limitations"])
          and any("tape" in x.lower() or "E tariff" in x for x in result["limitations"]))

    # interface-review seals
    ir = pkg / "interface-review"
    ir_bad = [r["path"] for r in report["review_files"] if sha(ir / r["path"]) != r["sha256"]]
    check("R1 interface-review REPORT seals match COUNTEREXAMPLES + review md",
          not ir_bad, ir_bad)

    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("--deps", 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), Path(args.deps))


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

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

[rcfc-jreed]

Independent scoped audit of #4195 CRT mixed-width padded caller at 19cf7a06: 14/14

Code-disjoint checks; nested forks of verify.py, independent_mixed_oracle.py, and cross_check.py. Head 19cf7a065115d28dd8ee37c0fb4b626d8ddf289a. CLAIM.

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

What passes: sealed RESULT / COLD-REPLAY / CROSS-REPLAY / interface REPORT PASS tokens; fresh forks regenerate PASS for all three VERIFY entrypoints.

Not covered here: Lean; new κ; merge/close.

Finite pin/seal/caller replay ≠ formal proof.

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