[petalas]

Summary

Scoped written proof with an explicit constructor and exact finite corroboration. For every alternating binary n-space with radical dimension k, the minimum width of an injective ordinary-dot-product realization is:

n = 0:            0
n > 0, k = 0:     n+1
k > 0:            n+k

For an F4 Hermitian form of dimension d and rank a, the width is 2d+1 when a=d>0 and 4d-2a when a<d. The construction preserves all radical directions. When the nonsingular part and radical are both nonzero, shared padding saves one coordinate over separate embeddings. The singular example diag(1,0) has exact width six, attained by binary images 3,6,15,48; separate padding uses seven.

Only research/faithful-alternating-width/ is added. This contribution was produced by Nick Petalas. Credit Maximus Putnam / Maximooch #831 for the trace-radical identity, alternating-compatible interface and degenerate-restriction opening, with its retained Joel Pulikkan / GamingPuzzled, endpoint-normal-form and hipotures / #41 lineage. Credit THU New Media Research Center / thu-nmrc #5464 for its earlier nonalternating degenerate embedding and radical-completion dimension bound. Hyperbolic splitting and the dimension bound are classical; no global literature priority is claimed. Predecessor mathematical and native results are cited, not audited.

Advance CLAIM. Base and submission refresh: canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030. TASK.json explicitly changes the decoder card to this geometric interface lemma. Live claims, local reservations, recent account work, open and merged PR searches and main README formula/object searches found no competing exact theorem in their stated coverage. Sparse working notes, arbitrary historical diffs and unpublished work remain outside that coverage.

Evidence

Before, #831 left degenerate restrictions unresolved and supplied a three-coordinate realization of one nonsingular hyperbolic block. After, PROOF.md proves the exact faithful width for every alternating form, including arbitrary radical dimension, and gives explicit minimum images. This settles a geometric prerequisite; it does not supply the missing physical caller.

• All 33,868 alternating matrices through dimension six pass construction, every Gram-entry check, literal image-span injectivity and literal nullspace checks.
• An independent literal search considers all 34,846 ordered even-vector tuples in ambient widths zero through six and source dimensions zero through three. Its first injective realizations agree on all twelve minimum-width problems. It does not use the constructor or the lower-bound proof to search.
• All 273 deterministic changed-basis fixtures through dimension 32 and ten explicit rejection controls pass. Controls reject collapsed radical directions, a wrong Gram matrix, unnecessary padding and malformed inputs.
• CPython 3.12.15, macOS arm64, standard library only. Warning-strict normal and optimized commands pass locally in 2.398 s and 2.418 s. Their generated JSON receipts agree exactly and bind all six package-file hashes. Each registered timeout is 120 seconds.
• PASS_REGISTERED_RESEARCH_PACKAGE passes both complete registered commands and metadata/source pins. PASS_RESEARCH_COMMIT_BYTES passes all eight package/input files and declared source history at head e4b49c2abd4ffc8cd8cc9392c43fa2e340d9d4d0. The worktree is clean.
• The constructor corpus has canonical SHA256 d119625804bc6c39a3ca7a5298cc6ee48c0285928e5b77465b9d348131af60fa. Receipts are generated by the verifier; none is handwritten.

Exact reproduction from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/faithful-alternating-width/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/faithful-alternating-width/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/faithful-alternating-width
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/faithful-alternating-width --check-source-history

Other installations can substitute their CPython 3.12 executable. Replay is read-only and prints PASS_FAITHFUL_ALTERNATING_WIDTH in its JSON receipt. The written proof is uniform; the executable constructor enforces n<=32.

Limitations

The result preserves binary vector identities and Gram pairings. It does not preserve a prescribed quadratic phase or weight modulo four. Native absolute phases, source/read incidence, nested physical frames, dirty restoration, physical hosting, paid compiler/caller costs, precision/tape and the complete multiplication theorem remain open. No new kappa or selected-frontier change is claimed. Independent human and formal proof-kernel review are unclaimed. Predecessor scientific replays, Lean, Docker and the selected cold replay were not run.

Open next questions

1. Determine the minimum faithful width with a specified quadratic refinement equal to ambient weight modulo four. Start with a hyperbolic block and one radical direction, separating whether the refinement vanishes on the radical. Quadratic type and weight congruences are missing.
2. Apply one minimum embedding to a literal degenerate source/read interface with declared entry/exit frames and phases, then price the complete physical itinerary and caller. The native implementation and full bill remain absent.

Related open work

No open PR found in the covered searches studies this exact faithful alternating-dot width or the singular Hermitian-trace width. The source #831 and related nonalternating-embedding predecessor #5464 are merged.

• #6441 determines faithfulness widths of point-column group-algebra actions. It preserves a representation of an entire algebra; this package preserves one bilinear space. No common numerical quantity is compared.
• #6449 classifies shortest formal permutation circuits using a faithful regular-action check. It does not study Gram-preserving label embeddings, and no common numerical quantity is computed.

The completion refresh inspected the eight other open PRs created by this account since the advance CLAIM. They concern dyadic snapshot and cut capacities, tensor reconstruction, stopped-recursion costs, a ternary COPY floor, nilpotent-Schur replay, a Gaussian inverse bound and rank-exchange credit. None studies this exact faithful alternating-dot width or reports a competing value computed here. No extra computations were run to check another contribution.

CI notes

Both hosted checks passed for exact head e4b49c2abd4ffc8cd8cc9392c43fa2e340d9d4d0 in run 41549931730: plan in 4m28s and registered replay in 1m32s. The completed checks were read once; the current PR head matches this commit.

Hosted CI certified execution of the registered normal and optimized finite checks. It does not supply independent human or formal proof-kernel acceptance of the written universal proof. All required local checks and the committed-byte/source-history preflight also passed.

Merge Danger

Door: two-way. Blast radius: isolated. Six new files in one opt-in research package; shared source, pinned evidence and the selected frontier are unchanged.