Prove exact faithful widths for degenerate alternating labels (no κ)

research/faithful-alternating-width/PROOF.md

@@ -0,0 +1,131 @@
+# Exact faithful width of an alternating binary space
+
+Let V be an n-dimensional vector space over F2, and let B be an
+alternating bilinear form on V. Alternating means B(x,x)=0 for every x;
+in characteristic two this also implies symmetry. Write r=rank(B) and
+k=n-r for its radical dimension. A faithful dot realization is an
+injective linear map f:V -> F2^m satisfying f(x) dot f(y)=B(x,y).
+The target has its ordinary coordinate dot product.
+
+The exact minimum m is
+
+```text
+0        if n=0;
+n+1      if n>0 and k=0;
+n+k      if k>0.
+```
+
+This theorem preserves the entire input vector space, including its
+radical. It does not prescribe a quadratic refinement or a native word.
+
+## Lower bounds
+
+Let W=f(V), and let R=f(rad(B)). Injectivity gives dim(W)=n and dim(R)=k.
+The isometry condition gives R subset W-perp in the nondegenerate ambient
+dot space. Thus k <= m-n, proving m>=n+k.
+
+If k=0 and n>0, equality m=n would make f surjective. The ordinary dot
+product would then be alternating, contrary to e_1 dot e_1=1. Hence
+m>=n+1. For n=0 the empty map attains zero.
+
+The first argument is the usual radical-completion bound. The
+nonalternating instance in THU New Media Research Center's PR5464,
+`research/odd-e8-polarized-native/EMBEDDING-PROOF.md` section 2, already
+uses it. The new scope here is the exact alternating answer with arbitrary
+radical, together with a constructor and the singular-trace corollary.
+
+## An explicit minimum realization
+
+The elementary hyperbolic splitting algorithm gives a basis in which
+
+```text
+B = H^(direct sum s) direct sum 0_k,
+H = [[0,1],[1,0]],  r=2s.
+```
+
+For completeness, if B is nonzero choose u,v with B(u,v)=1. Replace any
+other basis vector z by z+B(z,v)u+B(z,u)v. It becomes perpendicular to
+u,v, and the changed vectors together with u,v are still a basis. Split
+off this pair and repeat. When the remaining form is zero the remaining
+basis vectors span the radical. This also proves r is even.
+
+First realize the s hyperbolic pairs on coordinates 0 through r by
+
+```text
+u_i = e_(2i) + e_(2i+1),
+v_i = sum_(j=2i+1)^r e_j,       0 <= i < s.
+```
+
+Each u_i has even weight, and each v_i has weight r-2i, also even.
+Their pairings are u_i dot u_j=0, v_i dot v_j=0 and
+u_i dot v_j=[i=j]. For the second equality, when i<j the intersection
+of the two suffixes is v_j, whose weight is even. For the last equality,
+both coordinates of u_i lie in v_j if i>j, neither if i<j, and exactly
+one if i=j. Consequently these r vectors are independent.
+
+When k=0, these vectors realize B in m=r+1=n+1 coordinates.
+
+When k>0, append one coordinate and use
+
+```text
+z_0 = sum_(j=0)^(r+1) e_j.
+```
+
+It has even weight r+2 and is perpendicular to all u_i,v_i because they
+have even weight. Its last coordinate proves independence from them.
+For each 1<=j<k, append a disjoint coordinate pair and put
+
+```text
+z_j = e_(r+2j) + e_(r+2j+1).
+```
+
+Each z_j has zero self-pairing and is perpendicular to every other
+displayed vector. Its private coordinates prove independence. The full
+map has r+k=n independent images in exactly r+2k=n+k coordinates.
+This also covers r=0, where all images are disjoint two-coordinate pairs.
+Transporting this map through the adapted basis gives the required
+realization in the original input coordinates. The lower bounds show
+that every displayed width is optimal.
+
+One radical direction absorbs the extra coordinate needed by a
+nonsingular alternating space. Treating a nonzero H block and each
+radical direction independently would instead use r+1+2k coordinates.
+The construction removes precisely that unnecessary extra coordinate
+when r>0 and k>0.
+
+## F4 Hermitian trace corollary
+
+Let h be a Hermitian form on an F4 space of dimension d and F4 rank a.
+For B(x,y)=Tr_(F4/F2)(h(x,y)), Maximooch's PR831 proves that B is
+alternating and that its radical is exactly the binary version of the
+Hermitian radical. That identity is a cited premise here. Therefore
+
+```text
+n=2d,  r=2a,  k=2(d-a),
+
+minimum faithful dot width = 0             if d=0;
+                            2d+1          if a=d>0;
+                            4d-2a         if a<d.
+```
+
+The singular case has an exact answer without assuming that a support
+restriction or intersection is nondegenerate. No radical vector is
+discarded or identified with another input vector.
+
+For example h=diag(1,0) has trace Gram H direct sum 0_2 in the binary
+basis (1,t) on each F4 coordinate, where t^2+t+1=0. The explicit images
+3,6,15,48, written as six-bit integers with the low bit first, have that
+Gram matrix and are independent. Width six is necessary and sufficient.
+The three-bit H embedding alone loses both radical directions. Separately
+adding two isotropic pairs would use seven bits; shared padding saves one.
+
+## Exact limits
+
+Preserving B does not preserve the ambient weight modulo four or an
+arbitrary supplied quadratic phase. For H, the images 3 and 6 have weights
+two, so they do not preserve a refinement that vanishes on both input
+basis vectors. This theorem supplies binary vector identities and Gram
+pairings only. It does not supply a compatible Gaussian/native phase,
+source/read incidence, nested frame itinerary, physical owner schedule,
+dirty restoration, paid caller, precision/tape bound or multiplication
+theorem. Those costs and obligations remain unresolved.

research/faithful-alternating-width/README.md

@@ -0,0 +1,123 @@
+# Exact faithful width for degenerate alternating trace labels
+
+An alternating binary n-space with radical dimension k has the following
+minimum ambient width for an injective ordinary-dot-product realization:
+
+```text
+0        if n=0;
+n+1      if n>0 and k=0;
+n+k      if k>0.
+```
+
+For an F4 Hermitian form of dimension d and rank a, this is `2d+1` when
+`a=d>0`, and `4d-2a` when `a<d`. The zero-dimensional case needs no bits.
+This answers the faithful label-width part of the degenerate-restriction
+opening in [Maximooch's PR831](https://github.com/CrocSwap/integer-mult-bounds/pull/831).
+It is a scoped written proof with a constructive algorithm and finite exact
+corroboration. No new kappa or selected-frontier change is claimed.
+
+[PROOF.md](PROOF.md) gives the all-dimension lower bound and explicit
+attaining vectors. The construction retains every radical direction. When
+both the nonsingular part and radical are nonzero, sharing one padding
+coordinate saves one bit over embedding those parts separately.
+For example `H direct sum 0_2`, the trace form of `diag(1,0)` over F4,
+embeds faithfully with images `3,6,15,48` in six bits. Six is optimal;
+separate padding would use seven.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/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
+```
+
+The standalone verifier enumerates every alternating matrix through dimension
+six and constructs an injective realization for each. It checks every Gram
+entry, every vector image and every null vector on that domain. A separate
+literal search enumerates all ordered even-vector tuples in ambient widths
+zero through six for source dimensions zero through three; their first
+injective realizations must give the asserted minimum. Further changed-basis
+fixtures reach dimension 32. Explicit rejection controls cover invalid forms,
+radical collapse, a wrong Gram matrix and unnecessary padding.
+
+The first local replay passed 33,868 forms, all twelve independent literal
+minimum problems after 34,846 candidate tuples, 273 larger fixtures and ten
+rejection controls. The constructor corpus has canonical SHA256
+`d119625804bc6c39a3ca7a5298cc6ee48c0285928e5b77465b9d348131af60fa`.
+The written proof supplies the uniform result; these bounded computations
+corroborate it.
+
+Replay prints `PASS_FAITHFUL_ALTERNATING_WIDTH` in a generated JSON receipt
+bound to the six package-file hashes. It writes no files. Normal and optimized
+commands use the same explicit checks. Registered replay additionally
+authenticates the pinned source/provenance metadata. It does not execute or
+audit the predecessors' verifiers or native programs.
+
+## Scope and limits
+
+This changes the complex-rank-shape-decoder card to a geometric interface
+lemma. The cheap selected-baseline binding command passed before the change.
+The lemma identifies an exact width cost that Gram rank alone misses; it
+does not price a complete decoder or claim a full signed-moment improvement.
+
+Only binary linear identities and Gram pairings are preserved. A prescribed
+quadratic phase or weight modulo four can impose further conditions. Source
+incidence, nested physical frames, native absolute phase, dirty restoration,
+hosting, paid compiler/caller costs and all-size multiplication obligations
+remain open. No predecessor scientific replay, Lean, Docker or selected cold
+replay was run.
+
+## Open next questions
+
+1. What is the minimum faithful width when a specified quadratic refinement
+   must also equal ambient Hamming weight modulo four? This determines
+   whether the minimum Gram embedding preserves the required native phase.
+   Start with one hyperbolic block and one radical direction, separating
+   whether the refinement vanishes on the radical. Quadratic type and
+   ambient weight congruences are the missing constraints.
+2. Can a concrete degenerate source/read interface use this minimum embedding
+   with a favorable complete invoice? Start by declaring one actual label
+   space, all entry/exit frames and its prescribed phases. The physical
+   itinerary, native implementation and full caller bill remain missing.
+
+## Sources and credit
+
+This contribution was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed. New material is Apache-2.0.
+
+Credit Maximus Putnam / Maximooch, PR831, for the Hermitian trace-radical
+identity, the alternating-compatible interface and its degenerate-restriction
+opening; Joel Pulikkan / GamingPuzzled, the endpoint normal-form authors and
+hipotures / PR41 retain the lineage credited there. Credit THU New Media
+Research Center / thu-nmrc, PR5464, for its earlier nonalternating degenerate
+embedding and radical-completion lower bound. Its native construction is a
+separate result and is not replayed here. Hyperbolic splitting and the
+dimension bound are classical linear algebra; no global literature priority
+is claimed. The new deliverable is the uniform alternating minimum, explicit
+constructor and singular-trace width corollary under this faithful contract.
+Exact source bytes and the original priority card are pinned in SOURCES.json.
+
+The advance claim is [recorded in the handoff thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362861).
+
+## Verification implementation bounds
+
+The constructor accepts alternating forms through dimension 32 and emits at
+most 64 bits per image. Its hyperbolic split has at most sixteen stages and
+at most 496 candidate pairs per stage. It uses no recursion. The full-matrix
+census is streamed through dimension six, with at most 64 vectors in each
+literal image span. The independent minimum search uses at most 31 candidate
+vectors per coordinate and source dimension at most three. It retains just
+the first width for each of twelve Gram matrices. Each function is shorter
+than sixty lines. Explicit invariant and rejection checks remain active with
+optimized Python. Warning-strict normal and optimized replay are registered.
+
+Power-of-Ten rule 3 has a CPython managed-allocation deviation in verify.py.
+Integer, list, set and JSON allocations occur during verification. Their
+live sizes are bounded by the dimensions and streamed domains above; no
+corpus of all 33,868 embeddings is retained. The complete boundary and maximum
+dimension are exercised locally. A fixed-allocation implementation would be
+a separate port if this verifier becomes a constrained native component.

research/faithful-alternating-width/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/f4-alternating-interface/PROOF.md",
+      "usage": "input",
+      "git_blob": "ce615c156225291b7735fd6915781979cb901949",
+      "sha256": "5d0e8d57b2fd29ee943044841c134b32753415d7b7b459b9866422faabd5226c"
+    },
+    {
+      "path": "research/odd-e8-polarized-native/EMBEDDING-PROOF.md",
+      "usage": "input",
+      "git_blob": "1da5cc1a5262f14aa444ed13bc5ebe747701eb64",
+      "sha256": "4af1bdce75a5eb70ca3049d5087f8c85c650e465e50f52e81e5ae548d70cb1f1"
+    }
+  ]
+}