[theon199]

Result and scope

Add a source-pinned, independently implemented finite audit of PR #5459's automorphism determinant formula over F9, an odd-characteristic extension field absent from its checker. All 12,315 checked substitutions agree with the formula. No new kappa, supplier, full theorem proof or selected-frontier change is claimed.

The audit also demonstrates a concrete verification limitation: on the identity map of F9[x]/x^9, the incorrect determinant i has the same F3 norm as the true determinant 1. A norm-only oracle accepts that counterfeit; the exact F9 check rejects it. This is a counterexample to a verification shortcut, not to PR #5459.

Coverage and independence

• All 72 automorphisms of F9[x]/x^3.
• All 11,208 substitutions of F9[x]/x^9 with nonzero linear coefficient and at most two nonzero nonlinear monomials; not the full nonlinear group.
• All 576 height-preserving invertible linear substitutions on F9[x,y]/(x^3,y^9), all 376 identity-tangent single-monomial tails, and 83 deterministic dense nonlinear samples (seed 83).
• 156,978 generator-times-basis products, 11,280 division-free Leibniz determinant cross-checks and 163 restriction-of-scalars F3 determinant checks.
• Nine semantic controls, including invalid nonlinear relations despite invertible tangent, semilinear p-Frobenius, corrupted columns, wrong exponents and norm information loss.

No predecessor executable is imported or run. Exact source proof/checker bytes are retained for binding and attribution. Field arithmetic, quotient evaluation, Gaussian elimination, division-free determinant and prime-field norm checks are separately written. Domains can overlap; counts are checked presentations. Finite replay does not prove the general all-field theorem.

Reproduce and evidence

Python 3.12, standard library:

python3 -B scripts/research_package.py --package research/f9-character-audit

Expected: PASS_F9_CHARACTER_AUDIT in normal and optimized modes, then PASS_REGISTERED_RESEARCH_PACKAGE. The deterministic receipt is research/f9-character-audit/RESULT.json; source pins, exact domains and limitations are in its README, REFERENCE.json and VALIDATION.md. The standalone verifier works without Git or network.

Local verification includes the registered normal/optimized replays, exact committed-byte and source-history checks, a read-only Git-free export replay, source/receipt corruption controls and git diff --check. Hosted CI and independent human/proof-kernel approval are separate and unclaimed.

Base, overlap and limitations

Exact canonical base: 32890bc5de034ab8fc93ac88ead7279a6a416d04. Audited PR #5459 source: bef3575ddb19c44434a7e2460a353eac7c4d9387. The pending source bytes are included, so replay requires no unmerged Git object. Main-branch predecessors #5316 and #5252 are provenance-only.

OS assignment seed 83 selected independent verification. Three candidates and bounded PR/Discussion overlap coverage are recorded in CLAIM.md. The current selected conditional saving is 0.003027288235 (#5413); its five assumptions are unchanged. The catalogue formal-interface card is explicitly marked changed scope: this finite side audit does not claim its proof-kernel gate. No pinned sprint issue existed, so the claim and result are local.

This does not verify full covariant autotopism images, unit characters, general equal-height blocks, arbitrary finite fields, recognition, physical costs or multiplication admission. Next useful checks are nontrivial equal-height F9 blocks and the full inverse-input autotopism convention. The package states bounded starting points rather than claiming those tasks solved.

Credit

Ali Romman (#5459/#5316), Nick Petalas (#5252), David Ganz and their retained classical local-algebra/character-theory sources. New independent audit and packaging prepared for Charan / theon199 with substantial OpenAI Codex assistance. No subagents or independent human review. Apache-2.0; source notices retained.