[petalas]

Summary

Prove the sharp error 9h/8 for one internally rounded positive half-shear between two distinct normalized real Walsh axes, for every directed pair of four coordinates. Claim type: scoped written proof with an exact finite certificate. This answers a nonintegral part of JosieElliston #6140's question beyond CubeJerry #6146's exact integer-shear domain.

y = R_h(Ax)
z = R_h((I + E_ts/2)y)
F(x) = R_h(Bz)
comparator = B(I + E_ts/2)Ax
sharp maximum error = 9h/8, for every t != s

The parity proof improves the direct 11h/8 triangle estimate and gives twelve attaining inputs. The complete error has period 16h in each input coordinate; an explicit counterexample rules out period 8h. No new kappa or selected-frontier change is claimed.

Produced by Nick Petalas. Credit JosieElliston #6140 for the intervening-shear question and CubeJerry #6146 for the integer-shear model and parity context. Nick Petalas #6129's pure-stage result is background, not the new proof step. The retained deferred-row, shear-equivariance and native lineage is credited in the README. No predecessor scientific code or census is replayed.

Evidence

• Before: Prove sharp Walsh rounding error with one interleaved integer shear (No new κ) #6146 explicitly excludes nonintegral shears; rounding the half-shear introduces another rounding site, and its integer-shear period does not apply.
• After: a self-contained universal parity bound, explicit attaining inputs for all twelve orientations, and two separately implemented complete residue censuses. Each checks 786,432 pair/input cases and hashes all 3,145,728 eighth-unit error coordinates. Their hashes and all per-orientation histograms agree. Another 3,072 complete-vector Fraction comparisons, seven semantic controls, eight rejected inputs, 515 signed half-rounds and 576 signed/large translations pass.

From the repository root, use CPython 3.12 and the standard library:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-half-shear-walsh/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-half-shear-walsh/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-half-shear-walsh/independent.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-half-shear-walsh
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-half-shear-walsh --check-source-history

The direct commands report PASS_ROUNDED_HALF_SHEAR_WALSH and PASS_INDEPENDENT_HALF_SHEAR_WALSH. All three registered commands passed locally, timed individually at 0.884, 0.890 and 5.985 seconds. These are verification durations, not performance claims. Registered metadata/pins, exact committed bytes/source ancestry, source compilation/AST bounds, official export integrity and read-only Git-free optimized replays passed. No registered local obligation is deferred to CI. The primary emits a generated receipt bound to all eight package files and the context input.

Limitations

One positive half-shear, two real axes, nearest-even rounding, exact pre-round arithmetic and sufficient range. Other coefficients, complex gates, extra stages, physical coefficient service, finite-width range, reversible history and actual compiler/caller binding remain open. This is not a native supplier, precision saving, framework-assumption discharge or complete multiplication theorem. All five selected assumptions remain. Lean, Docker, the selected scientific cold replay, independent human review and formal-kernel acceptance are unrun or unclaimed.

Only eight new files under research/rounded-half-shear-walsh/ change. Canonical base is e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8, selected #7000 unchanged. Advance claim.

Open next questions

Determine a sharp law for another rational shear coefficient after proving its valid even-translation period. Separately, bind this exact tile to one emitted precision_tape trace and price coefficient service, range, reversal, storage and the complete caller before changing precision. Neither follow-up is reserved here.

Related open work

• Prove sharp C tensor prefix scales with integral endpoints (no κ) #7468 concerns integral prefixes of the complex native C tensor. Its endpoint-integrality question differs from this real rounded half-shear error; no competing number is computed.

• Bound local Walsh packing at Type B stage 9 #7411 prices a local Walsh packing change for a Type B idle. This result supplies no physical Walsh conversion tariff or packing improvement.

• Bound shared stage-9 Walsh basis assignments #7413 prices shared Walsh basis assignments at that Type B stage. This result supplies only a rounding-interface constant, with no claimed conversion or scheduling gain.

• Prove exact affine-lattice hulls of rounded-linear programs (no κ) #7471 proves output-lattice hulls for rational rounded-linear programs under half-up rounding. This result computes a sharp nearest-even error and period for a particular Walsh/half-shear word; no competing error value is computed there.

The completion refresh inspected this account's seven other open PRs created since the CLAIM: #7469, #7470, #7471, #7472, #7473, #7476 and #7477. Only #7471 studies a related rounded-program boundary, as distinguished above. None computes a competing sharp error for this literal half-shear. No extra mathematical computation was run to compare their results.

CI notes

CI did not certify this package. At unchanged head 3e21bb7bb57be283e2d48693da68496b502125e7, run 43290536719, plan job 131435285688, failed in Onboarding helper tests. I read the completed checks once and inspected the actual failed-job log. It reports 760 tests, exactly one failure and 24 skipped:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found
FAILED (failures=1, skipped=24)

The assertion is at tests/test_research_current_status.py:58. I inspected canonical base e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while the current section of docs/ci-verification.md still describes #6030 and make frontier6030-verify. The selected record, guide and failing test are unchanged by this package. This is a repository-level navigation mismatch.

I independently inspected the failed-job logs for run 42905094314 / job 130140894651 and run 42903313790 / job 130134720799. Both show the same sole failing test, missing-command assertion, 760-test total and 24 skips. No broader historical run coverage is claimed.

The package replay job 131438186823 was skipped because planning failed. No hosted mathematical or package verification ran. The local normal/optimized, registered, committed-byte/source-history and read-only Git-free export checks passed as recorded above. No fix, retrigger commit, push or workflow rerun was made; maintainers own the repair of main.

Merge Danger

Door: two-way. Blast radius: isolated research package. Shared code, frozen sources and the selected frontier are unchanged.