Prove sharp selected-unit minima for two #4729 Gram families (no new κ)

research/selected-unit-family-minima/README.md

@@ -0,0 +1,237 @@
+# Two exact selected-centre unit obstructions
+
+**Claim type: scoped proof with finite exact exclusion certificates.** No κ is
+claimed. The unrestricted minimum selected-port count stays open.
+
+For the pinned source matrix in Ali Romman's PR #4729, the minimum
+selected-port count is **38 in the integral two-block congruence family**
+defined below, and **39 when the selected Gram has one integral
+three-coordinate block and five remaining diagonal entries 20**. These
+are scoped proofs with finite exact exclusion certificates. They close
+two natural routes to a smaller simultaneous raw unit; they do not
+determine the minimum over arbitrary selected sets. Both positive
+sharpness constructions are credited to the predecessor; a literal
+39-port index set is retained as a calibration. Every exclusion also holds after
+conjugation by any word in the root reflections defined below.
+
+## Setting and precise statements
+
+Let R be the fixed eight-by-112 integer matrix in the included pinned
+SOURCE-INTERFACE.json. Each column r has squared norm four and RR^T=56I.
+For a subset S of distinct column indices put G=sum_(p in S) r_p r_p^T.
+With K=R^T/4, PR #4729 proves that both raw responses are dyadic units
+exactly when det(52I-G) and det(4I-G) are nonzero signed powers of two.
+This scalar criterion is the only interface premise used here.
+
+1. Partition eight coordinates into r+q=8. For any integral r-by-q B,
+   put V=[[0,B],[0,0]] and
+   G_B=52I-32(I+V/4)(I+V^T/4). No selected set with fewer than 38
+   ports has Gram equal to a signed coordinate conjugate of G_B and
+   satisfies both unit conditions. A 38-port set exists in this family.
+2. No selected set with at most 38 ports has Gram equal to a signed
+   coordinate conjugate of H direct-sum 20I_5 for an integral symmetric
+   three-by-three H and satisfies both unit conditions. A 39-port set
+   exists in this family.
+
+Both exclusions remain true after any subsequent conjugation by a word
+of the reflections O_r=I-rr^T/2 generated by the enlarged configuration
+consisting of the source columns and the eight axis columns 2e_i.
+This extension concerns the stated family targets and preserves their
+cardinality and determinant tests. It is not an arbitrary orthogonal
+conjugacy claim.
+
+## Proof of the two-block reduction
+
+Direct multiplication and Schur elimination give
+
+    G_B=[[20I-2BB^T,-8B],[-8B^T,20I]],
+    det(52I-G_B)=2^40,
+    det(4I-G_B)=(-16)^q 2^r det(3BB^T-8I),
+    trace(G_B)/4=40-||B||_F^2/2.
+
+A realized Gram is positive semidefinite. Eliminating its lower block
+20I shows that 50I-13BB^T is positive semidefinite. It is in fact
+positive definite, since a rational eigenvalue of an integral matrix
+must be an integer, whereas 50/13 is not. Hence every entry of B is
+0 or plus/minus one and every row and column has squared norm at most
+three. An improving selection has even ||B||_F^2 at least six.
+
+Transpose B if necessary so its row count is at most four. The unit
+and positive-definiteness tests are invariant under transpose, but the
+two resulting eight-dimensional target Grams must both be considered.
+Normalize each nonzero row's first nonzero entry to be positive, and
+enumerate row multisets. Repeated rows are retained. A zero row can be
+removed and replaced by a zero column; this only relocates an isolated
+diagonal entry 20 in the full Gram. Signed row and column operations
+give signed coordinate conjugations.
+
+The exact enumeration has 189, 6786, 47905 and 52360 nonzero-row
+multisets in row counts one through four. Respectively 0, 880, 260 and
+93 satisfy the improving unit and positive-definiteness tests. Signed
+row/column canonicalization leaves 0, 2, 3 and 6 classes. The eleven
+classes, with both orientations and all required coordinate placements,
+are covered by the integer exclusion certificates described below.
+This bounded enumeration is regenerated by verify.py.
+
+## Proof of the three-coordinate reduction
+
+Write trace(H)=s, and x^3-sx^2+ux-d for its characteristic polynomial.
+The trace identity gives s=4|S|-100, so |S|<=38 implies that s is one
+of 0,4,...,52. Positive semidefiniteness implies u,d>=0, nonnegative
+cubic discriminant, and eigenvalues in [0,52]. Put
+Q=det(52I-H) and W=det(4I-H). The nonnegative eigenvalues of 52I-H
+and the nonzero unit condition imply Q>0. Their complementary scalar factors are
+powers of two, so Q=2^a and W=epsilon*2^b. Bounds Q<=52^3<2^18 and
+|W|<=48^3<2^17 give 0<=a<=17 and 0<=b<=16. Expanding gives
+
+    Q-W=48(2928-56s+u),
+    d=64-16s+4u-W.
+
+There are 8568 bounded parameter tuples. The exact nonnegative
+coefficient/discriminant filters leave twenty polynomials. To realize
+an integral symmetric H, order its diagonal entries a0<=b0<=c0 and
+make the first two off-diagonal entries x,y nonnegative by coordinate
+signs. The third, z, takes both possible signs. The identities
+
+    x^2+y^2+z^2=a0*b0+a0*c0+b0*c0-u,
+    a0*b0*c0+2xyz-a0*z^2-b0*y^2-c0*x^2=d
+
+and bounds x^2<=a0*b0, y^2<=a0*c0, z^2<=b0*c0 give a finite
+integer enumeration including zero and singular cases. It leaves
+twenty-four signed-permutation classes. All their required placements
+are excluded below. The verifier independently regenerates this list.
+
+## Coordinate coverage and exact exclusions
+
+The source supports are exactly the fourteen affine planes in F2^3,
+each with all eight projective sign choices. Thus all coordinate sign
+changes preserve the source lines. A coordinate permutation preserving
+the support system is affine: after translating it to fix zero,
+preservation of {0,a,b,a+b} forces additivity. The stabilizer therefore
+has order 8*7*6*4=1344 and index 30 in S8.
+
+The inverse-image support-system key of a permutation gives exactly
+these thirty placement classes. Equal keys make two placed target
+Grams differ by a source automorphism. The verifier checks all 40320
+coordinate permutations and the active-permutation convention, rather
+than assuming arbitrary coordinate permutations preserve the roots.
+
+Let the enlarged list contain all 120 roots, and let F_y be an integer
+linear functional on upper-triangular Gram entries. For coefficients
+0<=x_r<=1,
+
+    F_y(sum_r x_r rr^T) <= sum_r max(0,F_y(rr^T)).
+
+A strict opposite inequality at the target is an exact box-separating
+certificate. The two-block certificate contains 900 indexed cases,
+covering all classes/orientations/placements, including padding
+duplicates. Its fifteen serialized generators reduce to the eleven
+nonzero-row classes above. All have strict integer box inequalities. Solver status is
+not used in this proof.
+
+For the three-coordinate class there are 720 indexed cases. Every
+pair of enlarged roots has even inner product. Therefore every integral
+sum G of their outer products satisfies s^T G t=0 modulo four for any
+two such roots. Explicit root-pair violations exclude 600 cases.
+Strict integer box inequalities exclude the remaining 120. The verifier
+rebuilds every target and checks every inequality or residue exactly.
+
+Every O_r permutes the enlarged projective root set. This follows by
+checking all 14400 root/reflection pairs exactly; no identification of
+an abstract reflection group is needed. It therefore preserves both
+the Boolean subset model and its box relaxation. The root-pair
+congruences are preserved too. The exclusions extend to all words in
+these reflections.
+
+## Sharpness
+
+The included predecessor S38 selection is exactly the witness in
+Ali Romman's PR #4729 at b556092ca912bfe6b2d94d754f51f2068d935c89.
+It is a two-block target with
+B=[[1,1,0,0,0,0],[0,0,1,1,0,0]]. Its full unit determinants are
+2^40 and 2^28. It supplies the upper bound 38; this construction is
+credited prior work.
+
+The included S39 selection has Gram H direct-sum 20I_5 with
+
+    H=[[16,-8,-8],[-8,20,0],[-8,0,20]].
+
+Its unit determinants are 2^40 and 2^30. Both literal selections,
+cardinalities and Gram identities are checked from the pinned columns.
+The S39 construction supplies the sharp upper bound in the second
+family and is not a global improvement on S38. The norm-two-row
+39-port construction already appears in PR #4729's retained dyadic
+proof and is credited there; this literal index set is a replay control.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and no third-party packages:
+
+```sh
+python3 scripts/research_package.py --package research/selected-unit-family-minima --check-only
+python3.12 scripts/research_package.py --package research/selected-unit-family-minima
+python3.12 -W error -B research/selected-unit-family-minima/verify.py
+```
+
+`verify.py` takes under two seconds. It rebuilds both finite reductions, the
+coordinate coverage and the reflection closure, and checks every exact
+certificate in `BOX-CERTIFICATES.json` and `THREE-BLOCK-CERTIFICATES.json`. It
+then rebuilds both sharpness witnesses from the literal columns and compares
+the result with the generated receipt `REPLAY.json`.
+
+`SOURCE-INTERFACE.json` is a byte copy of
+`research/raw-selected-centre-units/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json`
+at #4729 head `b556092ca912bfe6b2d94d754f51f2068d935c89` (Git blob
+`4201e9a04c12273b919e2cae60a6b6482c8150f3`). #4729 is not merged, so that
+commit is not reachable from this repository and `SOURCES.json` cannot pin
+it. Instead the verifier checks the copy's SHA256,
+`5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3`. The
+two-unit criterion is taken from that head's `PROOF.md` (SHA256
+`1f3f7e86573379cfecacd938a8915520e9a1e452abb45637b12d799c7e4329df`).
+
+## Verification and limits
+
+The standard-library verifier was written separately from the search
+code that produced the certificates. It uses no LP, integer solver,
+network, Git checkout or predecessor code. It passes both normally and
+with `-O`, so the proof does not rest on `assert` statements.
+
+The unrestricted minimum below 38 is still open. More general upper
+shears, nonintegral shear coefficients, several coupled blocks,
+different determinant families and arbitrary changed source matrices
+are outside these obstructions. Search failures outside the proved
+classes are not universal exclusions. No new exponent, complete
+supplier, native invoice, physical caller, recursive admission,
+precision or multiplication theorem is claimed.
+
+The selected-construction replay was not run and is not a dependency
+of these scalar results. Lean, Docker and historical native replays were not run.
+
+## Open next questions
+
+- Seek a smaller raw unit outside the integral two-layer family; the
+  exact certificates show why its apparent abstract 34-port targets
+  cannot be selected from the actual columns.
+- Couple at least four coordinates, use several interacting blocks,
+  or change the first-unit congruence model. A single integral
+  three-coordinate block cannot reach 38.
+- Before applying any scalar witness to a supplier, provide its actual
+  routed access, endpoint, restoration, physical cost and precision
+  contracts. These are independent obligations.
+
+The structured versions are in [TASK.json](TASK.json).
+
+## Credit
+
+This package was produced by Nick Petalas.
+
+Ali Romman's PR #4729 supplies the source matrix, the two-unit criterion, the
+38-port witness and the explicit open minimum question. Its historical
+source lineage includes dcharb78's PR #3133 and Jeremy Diviney's
+PR #3148. Its retained notices credit Rohan Arun for native lowering
+and owner construction, Cinna Davis's PR #2226 for dirty borrowing,
+and Jeremy Kothe's PR #2588 for retained methods. This result uses
+the scalar source configuration; the native programs are outside
+its implementation premises. Exact source heads,
+paths and hashes are in SOURCES.json. The new contribution is the
+complete scoped exclusions and the sharp single-block result.