[jmbarrancoml]

I instantiate the retained block-factor rounding handoff at PR4100's narrow Gaussian boundary gap delta>=1/(16p²). I keep the original two-product block order and exact dyadic Strassen products, then round coefficient/inverse pages and completed RHS/solution blocks. I derive the complete residual before bounding the rounded state, so the error estimate has no factor equal to the number of row blocks.

For eta=2^(1-P) and Y0=max(1,||RHS||max), the condition eta<=2^-21*p^-9 gives two-pass solution error below 2^40*p^16*eta*Y0, output magnitude at most 2^20*p^7*Y0, and exact arithmetic temporaries at most 2^46*p^16*Y0 on the 2P grid. These explicit constants give O(p)-bit words when P and log(Y0) are O(p). I account for rounded diagonal-block inverses, consecutive-block geometry, both upper-pass reversals and temporary padding. I preserve the complete ceiling-based batching tariff and its R>=w simplification boundary.

I execute the authenticated retained block_solve and recursive mul through a rounding adapter. Independent ordinary elimination and matrix products supply exact solutions and residuals. Fifteen systems cover sixty triangular passes, 548 matrix products and 12,164 actual Strassen leaf products. All fifteen have nonzero rounding error. Controls distinguish an inverse of a rounded block from a rounded reference inverse, nonconsecutive inverse blocks, insufficient precision, wrong direction, unhandled corners, omitted predecessor blocks and omitted output rounding.

At head a20501df8fc07f5ceb32e6fd64bce9ad8fe594bf, both registered ordinary/optimized checks pass. I passed the 20-file committed-byte/source-history preflight and official export integrity. Both Git-free export commands pass in 0.422 and 0.430 seconds, with all 21 files including the receipt unchanged. Export SHA256: 4c422a21fc5860d92818d4ed5a6b4f6c2072296c8a39466ec63cfac768993dd5; receipt SHA256: 2901b6f41cbe4f40814737949ffd95a280d6a8fa9d8aa7da6d4fda1ea2a0fc63. Scientific receipt: 4941625250a4d71c7c76ba4963e1593b5fddf48cffd3b0bc121e1de4cf82ebfb.

I matched both successful hosted records to the committed export and checked the successful unchanged-input step. Test merge 11b0d728a4a4d8f0f60bb89fb50489617c0719b5 has the published tree 281da10ce2985fc3e81283dbe3167a03d63a20d0.

I start from canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7, and pin PR4100 at 337d04939571a637aeab54a0f58f54fde811663a. I refreshed main, source feedback and 100 recent PR records before publication. Discussion4182 records the claim, bounded overlap, complete obligation ledger and prior coverage. The new PR4184 free-word audit is complementary.

I restrict the theorem to the stated naturally ordered finite-section narrow boundary and exact reference LU/inverse-page preparation. I do not assert the same result for an arbitrary rounded LU factorization, unhandled cyclic geometry or a broad Schur inverse. Physical factor-page/tape integration, analytic reference preparation and complete multiplication-theorem acceptance remain separate. I keep the selected frontier unchanged.

Jose Manuel (jmbarrancoml), with substantial OpenAI Codex assistance. I credit Vlado Vojdanovski's block proposal and prototype, the earlier qualitative stability and Schur audits, Cinna Davis's conditioning argument, the original Gaussian/Harvey–van der Hoeven lineage, and the scalar physical solver's prior residual analysis. I retain the classical Strassen and stability attribution. Source-analysis agents belong to the author process; I claim no independent human or formal-kernel acceptance.

[rcfc-jreed]

Independent scoped audit of the rounded boundary-block package at a20501df: no defect found in the finite error/residual / seal layer

Code-disjoint reimplementation; does not import package verify.py. Package bytes from head a20501df8fc07f5ceb32e6fd64bce9ad8fe594bf via GitHub contents API. CLAIM.

What passes (10 of 10):

1. Pins. Base 12fa8c5c…. Thirteen SOURCES inputs authenticate. RESULT PASS_ROUNDED_BOUNDARY_BLOCKS; scope excludes physical tape and full multiplication theorem.
2. Cases. 15 cases; every top-level error < error_bound; dual answer_sha256; production_batch_domain.
3. Passes. 60 lower/upper invoices: error < error_bound, residual ≤ residual_bound; seven named controls; p∈{1,2,4}.

Not covered: live block-solve re-execution; physical tape; broad inverse; new κ.

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

check_4186.py

#!/usr/bin/env python3
"""Independent finite controls for PR4186 (rounded boundary block solves).

Recomputes error < error_bound on all cases/passes, seals, and honesty flags.
Does not import package verify.py.

Package head a20501df8fc07f5ceb32e6fd64bce9ad8fe594bf 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 fractions import Fraction
from pathlib import Path

HEAD = "a20501df8fc07f5ceb32e6fd64bce9ad8fe594bf"
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 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 run(pkg: Path, deps: Path):
    sources = load(pkg, "SOURCES.json")
    verify = load(pkg, "VERIFY.json")
    result = load(pkg, "RESULT.json")

    check("I1 SOURCES base_commit == 12fa8c5c…; VERIFY ready",
          sources["base_commit"] == BASE and verify["status"] == "ready")
    check("I2 RESULT PASS_ROUNDED_BOUNDARY_BLOCKS; no physical tape / full mult theorem in scope",
          result["status"] == "PASS_ROUNDED_BOUNDARY_BLOCKS"
          and "no physical tape" in result["scope"].lower()
          and "multiplication theorem" in result["scope"].lower())

    n_in, bad = auth_sources(sources, deps)
    check("S1 SOURCES input files authenticate (sha256 + git blob)",
          not bad and n_in == 13, bad)

    check("C1 case_count=15 matches cases dict; 7 named controls; real_triangular_passes=60",
          result["case_count"] == 15 == len(result["cases"])
          and len(result["controls"]) == 7
          and result["real_triangular_passes"] == 60)

    bad_e, bad_p, bad_a = [], [], []
    pass_total = 0
    for name, case in result["cases"].items():
        if Fraction(case["error"]) >= Fraction(case["error_bound"]):
            bad_e.append(name)
        if len(case["answer_sha256"]) != 2 or any(len(h) != 64 for h in case["answer_sha256"]):
            bad_a.append(name)
        if case["production_batch_domain"] is not True:
            bad_a.append(("domain", name))
        for pi, pass_row in enumerate(case["passes"]):
            for side in ("lower", "upper"):
                row = pass_row[side]
                pass_total += 1
                if Fraction(row["error"]) >= Fraction(row["error_bound"]):
                    bad_p.append((name, pi, side, "error"))
                if Fraction(row["residual"]) >= Fraction(row["residual_bound"]):
                    # residual may equal residual_bound? use >
                    if Fraction(row["residual"]) > Fraction(row["residual_bound"]):
                        bad_p.append((name, pi, side, "residual"))
    check("C2 every case error < error_bound; dual answer_sha256; production_batch_domain",
          not bad_e and not bad_a, {"error": bad_e, "other": bad_a[:4]})
    check("C3 every lower/upper pass: error < error_bound; residual ≤ residual_bound",
          not bad_p, bad_p[:6])
    check("C4 pass invoice count = real_triangular_passes (=60)",
          pass_total == result["real_triangular_passes"] == 60)

    # naming / parameter sanity
    ps = {case["p"] for case in result["cases"].values()}
    check("C5 p-values cover {1,2,4}; all error_bound default 1/256 except near-gap-p4",
          ps == {1, 2, 4}
          and result["cases"]["near-gap-p4"]["error_bound"] == "53/16384"
          and all(c["error_bound"] == "1/256"
                  for n, c in result["cases"].items() if n != "near-gap-p4"))

    check("N1 controls name seven semantic/admission faults",
          set(result["controls"]) >= {
              "rounded-input inverse page", "nonconsecutive inverse block",
              "insufficient absorption precision", "unreversed upper direction",
              "unhandled cyclic corner", "omitted previous block",
              "omitted solved-block rounding",
          })

    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 #4186 rounded block-solve fine-prime boundary at a20501df: 7/7

Code-disjoint nested HERE/ROOT fork of verify.py. Head a20501df8fc07f5ceb32e6fd64bce9ad8fe594bf. CLAIM.

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

What passes: fork regenerates PASS against sealed RESULT.json.

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

Finite pin/seal/interval replay ≠ formal proof.

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