Prove the exact F4 hyperplane intersection law (no new κ)

research/hermitian-hyperplane-intersections/README.md

@@ -0,0 +1,238 @@
+# Exact nondegenerate-hyperplane intersection law over F4
+
+This contribution was produced by Nick Petalas. It proves a scoped algebraic
+intersection theorem and counting law, with exact finite corroboration.
+It answers the intersection obligation left by Maximus Putnam's
+[PR #831](https://github.com/CrocSwap/integer-mult-bounds/pull/831).
+That package's phase calculus and census are cited predecessors, not audit
+subjects here. No new kappa is claimed.
+
+Let V be a nondegenerate Hermitian space of dimension n over
+F4 = F2[t]/(t²+t+1), with conjugation a -> a². Take the form linear in
+its second argument. A restriction is nondegenerate when its radical is zero;
+the zero-dimensional space counts as nondegenerate.
+
+## Result
+
+For n >= 2, write H_u = u-perpendicular for the hyperplane with normal line
+F4 u. Nondegeneracy of H_u is equivalent to h(u,u)=1. For distinct
+nondegenerate hyperplanes H_u,H_v:
+
+- Their intersection is nondegenerate exactly when h(u,v)=0.
+- Otherwise its Hermitian radical has dimension one over F4. Its binary
+  trace radical has dimension two over F2.
+
+Define
+
+    N_n = (4^n - (-2)^n)/6,
+    Z_n = (4^n + (-2)^n)/2.
+
+There are exactly N_n nondegenerate hyperplanes. For each fixed one,
+exactly N_(n-1) other nondegenerate hyperplanes have nondegenerate
+intersection with it, and exactly Z_(n-1)-1 have degenerate intersection.
+The ordered-pair counts are therefore
+
+    nondegenerate: N_n N_(n-1),
+    degenerate:    N_n (Z_(n-1)-1).
+
+For a uniformly chosen ordered pair of distinct nondegenerate hyperplanes,
+the degeneracy probability is (Z_(n-1)-1)/(N_n-1), tending to 3/4.
+This probability describes the stated finite sample space. It does not
+model a supplier's distribution of frames.
+
+The verifier enumerates these complete finite domains:
+
+| Ambient dimension | Nondegenerate hyperplanes | Nondegenerate ordered pairs | Degenerate ordered pairs |
+| --- | --- | --- | --- |
+| 2 | 2 | 2 | 0 |
+| 3 | 12 | 24 | 108 |
+| 4 | 40 | 480 | 1080 |
+| 5 | 176 | 7040 | 23760 |
+
+A family of distinct nondegenerate hyperplanes whose pairwise intersections
+are all nondegenerate has size at most n. Its normal lines are mutually
+orthogonal, and every intersection of any subfamily is nondegenerate.
+The n coordinate hyperplanes attain the bound. This supplies a precise
+sufficient contract for retaining nondegeneracy throughout intersections.
+
+## Proof
+
+### Hermitian coordinates and normal lines
+
+Every nondegenerate Hermitian F4 space has an orthonormal basis. Here is
+an elementary argument to fix the field-specific premise. If every vector
+had norm zero, choose x,y with a=h(x,y) nonzero. Such a pair exists by
+nondegeneracy in positive dimension. For c=t/a,
+
+    h(x+cy,x+cy) = ca + conjugate(ca) = t+t² = 1,
+
+a contradiction. A vector of nonzero norm has norm one, since Hermitian
+norms lie in F2. Split off its nondegenerate line and repeat on the
+nondegenerate orthogonal complement. Thus h can be written as
+h(x,y)=sum_i conjugate(x_i)y_i.
+
+Nondegeneracy of V identifies its hyperplanes with normal lines. The
+radical of u-perpendicular is its intersection with F4 u. It is zero
+exactly when h(u,u) is nonzero, hence one. Each normal line has three
+nonzero vectors, all with the same norm, because every nonzero F4 scalar
+has multiplicative norm one.
+
+### Intersection criterion
+
+Let U=span(u,v), where the normal lines are distinct. Then dim U=2 and
+H_u intersect H_v = U-perpendicular. The radicals of U and U-perpendicular
+are the same subspace U intersect U-perpendicular. In the basis u,v, the
+restricted Hermitian Gram matrix is
+
+    [ 1       z ]
+    [ z²      1 ],       z=h(u,v).
+
+Its determinant is 1+z³. Every nonzero element of F4 has cube one.
+Consequently the matrix has rank two for z=0 and rank one for z!=0.
+This proves the criterion and the exact Hermitian radical dimension.
+Maximus Putnam's #831, PROOF.md section 1, proves that the radical of the
+binary trace form is the same set as the Hermitian radical. Its F2
+dimension is therefore twice its F4 dimension. That trace lemma is a
+credited dependency, not a new result here.
+
+### Exact counts
+
+In orthonormal coordinates the norm of a vector is the parity of its number
+of nonzero coordinates. Let Z_n and O_n count vectors of norm zero and one.
+Each coordinate has one zero and three nonzero possibilities, so
+
+    Z_n + O_n = 4^n,
+    Z_n - O_n = (1-3)^n = (-2)^n.
+
+The displayed Z_n follows and O_n=(4^n-(-2)^n)/2. Dividing O_n by the
+three vectors per nonisotropic line gives N_n. This includes n=0,
+where N_0=0 and Z_0=1.
+
+Fix a normal u and use orthonormal coordinates with u=e_1. A second normal
+has representative v=(a,w), with a in F4 and w in F4^(n-1), and
+h(v,v)=a³+h(w,w)=1. If a=0, the vector w has norm one. These are exactly
+the N_(n-1) nonisotropic lines orthogonal to u, and the intersection
+criterion says precisely these pairs are nondegenerate.
+
+If a!=0, w must have norm zero. The 3 Z_(n-1) vector representatives
+form Z_(n-1) normal lines. One is the original line u, arising from w=0.
+Removing it leaves Z_(n-1)-1 distinct normal lines. Their pairings with u
+are nonzero and all their intersections are degenerate. This also checks
+N_n-1=N_(n-1)+Z_(n-1)-1 and proves both ordered-pair counts. Dividing by
+N_n(N_n-1) gives the probability; its limit follows from the leading
+powers of four.
+
+### Smallest failure and families closed under intersection
+
+In dimension three take u=(1,0,0) and v=(1,1,1). Both have norm one.
+The two input hyperplanes have Hermitian rank two and binary trace rank
+four. Their intersection is the line spanned by (0,1,1), whose restriction
+is zero. In dimension two, distinct hyperplanes intersect in zero, so
+dimension three is the smallest possible failure. Dimension one has no
+pair of distinct hyperplanes.
+
+If a family has only nondegenerate pairwise intersections, the criterion
+makes its normal lines mutually orthogonal. Choose a norm-one vector
+from each. Their Gram matrix is the identity, so they are independent
+and their number is at most n. The span of any chosen subfamily is
+nondegenerate, as is its orthogonal complement. That complement is
+exactly the intersection of the corresponding hyperplanes. Coordinate
+normal vectors attain size n. In particular, under this hyperplane
+hypothesis pairwise checking suffices for every higher intersection.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/hermitian-hyperplane-intersections/verify.py
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/hermitian-hyperplane-intersections/verify.py
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/hermitian-hyperplane-intersections
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/hermitian-hyperplane-intersections --check-source-history
+
+Another CPython 3.12 interpreter may replace the absolute local path.
+The local environment was CPython 3.12.15 on macOS 27.0.1, arm64.
+The two registered commands took 1.62 and 1.61 seconds in direct timed runs;
+each has a 120-second registered limit.
+The direct check prints a generated SHA-256 receipt binding all five package
+files, then PASS_HERMITIAN_HYPERPLANE_INTERSECTIONS. It writes nothing.
+
+The checker constructs every normal line in dimensions two through five.
+For each of the 32,494 ordered distinct pairs it computes an actual
+intersection basis by F4 elimination, its restricted Hermitian Gram rank,
+and its binary trace Gram rank by separate packed-binary elimination.
+It checks each individual normal's two counts, not only their aggregate.
+It also checks all 21,845 vectors in dimensions zero through seven for the
+norm formulas, all 64 field triples for the stated field identities, and
+all 4096 subsets of the twelve normals in dimension three. The numbers
+of pairwise-safe subsets by size zero through three are (1,12,12,4).
+Every safe subset's full intersection is checked directly.
+
+Eight rejection controls cover repeated hyperplanes, isotropic normals,
+a dimension outside the pair domain, an invalid field entry, false
+intersection closure, a count-sign error, omitted conjugation, and the
+wrong binary radical dimension. Positive controls include a nonbinary
+coefficient witness and orthogonal normals. All checks remain active
+under optimized execution. The universal quantifiers follow from the
+written proof, not extrapolation from this finite certificate.
+
+## Limits and engineering decisions
+
+This is a scoped Hermitian hyperplane theorem. It does not identify a
+supplier's actual supports or intersections. For subspaces of higher
+codimension, pairwise nondegeneracy is a different question. No fitting
+labels, physical caller, native conversion, routing, precision, restoration,
+stock or complete paid invoice is supplied. The full complex supplier and
+complete multiplication theorem remain unproved here. Independent human
+and formal proof-kernel review are unclaimed. Lean, Docker and the selected
+construction's full replay were not run.
+
+The original rank-shape card is explicitly changed to this algebraic side
+question, following #831's stated gap. It does not pass that card's supplier
+admission or five-percent improvement gate. The current source-bound baseline
+passed. The card's historical first command,
+research/complex-local-word-ceiling/verify.py, fails with
+KeyError: 'complex_profile' because its selected-profile schema is historical.
+That predecessor remains unchanged; the new verifier does not invoke it.
+
+The checker computes the literal restricted forms and imports no predecessor
+verifier. All loops have fixed finite domains, every function is shorter than 60 lines,
+and validation uses ordinary exceptions. Power-of-ten rule 3 has a bounded
+managed-runtime deviation: Python allocates tuples, lists and integers during
+this offline computation. At most 176 normal lines are retained; matrices
+have at most ten rows and columns; vectors and pairs are streamed. Rule 9
+has eight fixed, immediate, nonescaping callbacks only for rejection controls.
+There is no service or persistent resource. Warning-strict normal and
+optimized commands provide the available diagnostics. No separate static
+analyzer is required by this standard-library environment.
+
+## Open next questions
+
+1. Which families of nondegenerate subspaces of codimension two have every
+   intersection nondegenerate? The hyperplane result gives a complete safe
+   contract only in codimension one. Start with two-dimensional normal
+   spaces in F4^4 and classify the restricted Gram matrix of their sum.
+   Pairwise orthogonality of normal spaces is sufficient but its necessity
+   is unproved and is not asserted here.
+2. Can an actual Eisenstein producer keep all required hyperplane normals
+   mutually orthogonal, with a complete paid consumer? Start by extracting
+   one producer's literal normal lines and checking this theorem's criterion.
+   The missing supports and physical invoice block a supplier conclusion.
+
+These follow-ups are not investigated here. TASK.json records their first
+steps and blockers.
+
+## Credit and source boundary
+
+Produced by Nick Petalas. Maximus Putnam / Maximooch's #831 supplies the
+explicit unresolved intersection obligation and the trace-radical lemma.
+Its retained credit includes Joel Pulikkan / GamingPuzzled's #620 report,
+hipotures' alternating-block predecessor #41 and the endpoint-phase authors.
+The new contribution is the exact intersection criterion, all-dimension
+counts, smallest failure and pairwise-safe family consequence in this
+repository's F4 interface setting. The Hermitian linear algebra and parity
+counting tools are elementary; no historical priority for them is claimed.
+
+SOURCES.json pins the predecessor documents, catalogue and selected record
+at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf as historical
+provenance. They are not live mathematical inputs to the standalone finite
+checker. No predecessor code is copied. Apache-2.0.

research/hermitian-hyperplane-intersections/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/f4-alternating-interface/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "ce615c156225291b7735fd6915781979cb901949",
+      "sha256": "5d0e8d57b2fd29ee943044841c134b32753415d7b7b459b9866422faabd5226c"
+    },
+    {
+      "path": "research/f4-alternating-interface/README.md",
+      "usage": "provenance",
+      "git_blob": "75f6febef56548af37aef306a307ff94cdce6473",
+      "sha256": "ce9f880a853c3e4ea0fa39afa718e253961836b51dc9c45203bb75684805d5fd"
+    }
+  ]
+}

research/hermitian-hyperplane-intersections/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the exact nondegenerate-Hermitian-hyperplane intersection criterion, all-dimension ordered-pair counts over F4, smallest failure and pairwise-safe family bound.",
+  "scope_change_reason": "The original decoder rank-shape card is narrowed to the explicit unresolved intersection obligation in Maximus Putnam PR831. This algebraic side result does not claim a supplier profile or the card admission gate.",
+  "bottleneck_link": "Side result for the F4 alternating-compatible interface: nondegenerate input supports do not ensure nondegenerate intersections. This theorem identifies the exact safe hyperplane contract without assigning an unknown consumer cost zero.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified original intersection theorem and count; do not extend to higher codimension or native implementation.",
+  "outcome": "completed",
+  "evidence": "Written all-dimension proof; exact 32494-pair restricted-form census through dimension five, 21845 norm vectors, all 4096 dimension-three normal subsets and eight rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which codimension-two nondegenerate-subspace families have only nondegenerate intersections?",
+      "why_it_matters": "Hyperplane normal orthogonality is a complete criterion only in codimension one.",
+      "first_step": "Classify the restricted Gram matrices of sums of two-dimensional normal spaces in F4^4.",
+      "blocked_by": "No higher-codimension necessity theorem or classification is provided."
+    },
+    {
+      "question": "Can an actual Eisenstein producer maintain mutually orthogonal hyperplane normals with a complete paid consumer?",
+      "why_it_matters": "The abstract safe-intersection contract alone does not admit a supplier.",
+      "first_step": "Extract one actual producer normal family and check its literal Hermitian pairings.",
+      "blocked_by": "Actual supports, native realization and the complete physical invoice are absent."
+    }
+  ]
+}

research/hermitian-hyperplane-intersections/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete F4 normal-line pair domains through dimension five, literal Hermitian/binary intersection ranks, exact counts and eight rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete certificate under optimized Python; no assertion-dependent checks."
+    }
+  ]
+}