From 176557475ed40d656dfffbbba79c99fdf9553f1b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 14:58:34 +0100 Subject: [PATCH] feat(research): prove the exact F4 hyperplane intersection law --- .../README.md | 238 +++++++++++++++++ .../SOURCES.json | 30 +++ .../TASK.json | 78 ++++++ .../VERIFY.json | 32 +++ .../verify.py | 252 ++++++++++++++++++ 5 files changed, 630 insertions(+) create mode 100644 research/hermitian-hyperplane-intersections/README.md create mode 100644 research/hermitian-hyperplane-intersections/SOURCES.json create mode 100644 research/hermitian-hyperplane-intersections/TASK.json create mode 100644 research/hermitian-hyperplane-intersections/VERIFY.json create mode 100644 research/hermitian-hyperplane-intersections/verify.py diff --git a/research/hermitian-hyperplane-intersections/README.md b/research/hermitian-hyperplane-intersections/README.md new file mode 100644 index 0000000000..5de2d65c9d --- /dev/null +++ b/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. diff --git a/research/hermitian-hyperplane-intersections/SOURCES.json b/research/hermitian-hyperplane-intersections/SOURCES.json new file mode 100644 index 0000000000..018a306456 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/hermitian-hyperplane-intersections/TASK.json b/research/hermitian-hyperplane-intersections/TASK.json new file mode 100644 index 0000000000..f82ecf6f23 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/hermitian-hyperplane-intersections/VERIFY.json b/research/hermitian-hyperplane-intersections/VERIFY.json new file mode 100644 index 0000000000..d8a1ff4bb7 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/hermitian-hyperplane-intersections/verify.py b/research/hermitian-hyperplane-intersections/verify.py new file mode 100644 index 0000000000..2872833bff --- /dev/null +++ b/research/hermitian-hyperplane-intersections/verify.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +"""Exact F4 intersection certificate. Produced by Nick Petalas. Apache-2.0. + +Independent human and formal proof-kernel review are unclaimed. +The all-dimension statement is proved in README.md; this is finite evidence. +""" + +import hashlib +import itertools +import json +from pathlib import Path + + +MAX_PAIR_DIMENSION = 5 +MAX_NORM_DIMENSION = 7 +CONJUGATE = (0, 1, 3, 2) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(a, b): + """Polynomial basis 1,t with t^2=t+1; elements are two-bit integers.""" + low = (a & 1) * (b & 1) + middle = ((a & 1) * (b >> 1)) ^ ((a >> 1) * (b & 1)) + high = (a >> 1) * (b >> 1) + return (low ^ high) | ((middle ^ high) << 1) + + +def hermitian(u, v): + result = 0 + for a, b in zip(u, v, strict=True): + result ^= multiply(CONJUGATE[a], b) + return result + + +def rref(matrix, columns): + need(0 <= columns <= 10 and len(matrix) <= 10, "matrix size bound") + need(all(len(row) == columns for row in matrix), "rectangular matrix") + rows = [list(row) for row in matrix] + need(all(0 <= x < 4 for row in rows for x in row), "F4 entries") + pivots = [] + for column in range(columns): + candidates = [i for i in range(len(pivots), len(rows)) if rows[i][column]] + if not candidates: + continue + index = len(pivots) + rows[index], rows[candidates[0]] = rows[candidates[0]], rows[index] + inverse = CONJUGATE[rows[index][column]] + rows[index] = [multiply(inverse, x) for x in rows[index]] + for i in range(len(rows)): + if i != index and rows[i][column]: + coefficient = rows[i][column] + rows[i] = [x ^ multiply(coefficient, y) + for x, y in zip(rows[i], rows[index], strict=True)] + pivots.append(column) + return rows, pivots + + +def kernel(matrix, columns): + rows, pivots = rref(matrix, columns) + basis = [] + for free in range(columns): + if free not in pivots: + vector = [int(j == free) for j in range(columns)] + for row, pivot in zip(rows, pivots): + vector[pivot] = row[free] + basis.append(tuple(vector)) + return basis + + +def binary_rank(rows): + need(len(rows) <= 10, "binary rank dimension") + pivots = [0] * 10 + result = 0 + for row in rows: + need(0 <= row < 1024, "binary row bound") + value = row + for column in range(9, -1, -1): + if value & (1 << column): + if pivots[column]: + value ^= pivots[column] + else: + pivots[column] = value + result += 1 + break + return result + + +def restriction_ranks(basis): + gram = [[hermitian(u, v) for v in basis] for u in basis] + rank4 = len(rref(gram, len(basis))[1]) + binary_basis = [tuple(multiply(a, x) for x in v) + for v in basis for a in (1, 2)] + binary_rows = [] + for u in binary_basis: + row = 0 + for j, v in enumerate(binary_basis): + value = hermitian(u, v) + trace = value ^ CONJUGATE[value] + need(trace in (0, 1), "trace lies in F2") + row |= trace << j + binary_rows.append(row) + return rank4, binary_rank(binary_rows) + + +def intersection(u, v): + n = len(u) + need(2 <= n <= MAX_PAIR_DIMENSION and len(v) == n, "pair dimension") + need(hermitian(u, u) == hermitian(v, v) == 1, "nonisotropic normals") + basis = kernel([[CONJUGATE[x] for x in u], [CONJUGATE[x] for x in v]], n) + need(len(basis) == n - 2, "distinct normal lines") + need(all(hermitian(u, x) == hermitian(v, x) == 0 for x in basis), + "literal common kernel") + rank4, rank2 = restriction_ranks(basis) + return n - 2 - rank4, 2 * (n - 2) - rank2 + + +def norm_counts(n): + return ((4**n + (-2)**n) // 2, (4**n - (-2)**n) // 2) + + +def hyperplane_count(n): + return (4**n - (-2)**n) // 6 + + +def norm_one_lines(n): + return [v for v in itertools.product(range(4), repeat=n) + if next((x for x in v if x), 0) == 1 and hermitian(v, v) == 1] + + +def field_and_norm_checks(): + field_cases = 0 + for a, b, c in itertools.product(range(4), repeat=3): + need(multiply(a, b ^ c) == (multiply(a, b) ^ multiply(a, c)), + "field distributivity") + need(multiply(multiply(a, b), c) == multiply(a, multiply(b, c)), + "field associativity") + need(multiply(a, b) == multiply(b, a), "field commutativity") + need(multiply(a, a) == CONJUGATE[a], "field conjugation") + need(multiply(CONJUGATE[a], a) == int(a != 0), "field norm") + field_cases += 1 + vector_cases = 0 + for n in range(MAX_NORM_DIMENSION + 1): + observed = [0, 0] + for v in itertools.product(range(4), repeat=n): + norm = hermitian(v, v) + need(norm in (0, 1), "Hermitian norm in F2") + observed[norm] += 1 + vector_cases += 1 + need(tuple(observed) == norm_counts(n), "closed norm counts") + return field_cases, vector_cases + + +def census(): + results = [] + for n in range(2, MAX_PAIR_DIMENSION + 1): + lines = norm_one_lines(n) + need(len(lines) == hyperplane_count(n), "hyperplane count") + counts = [0, 0] + for u in lines: + per_normal = [0, 0] + for v in lines: + if u == v: + continue + radical4, radical2 = intersection(u, v) + predicted = int(hermitian(u, v) != 0) + need(radical4 == predicted, "F4 radical criterion") + need(radical2 == 2 * predicted, "binary radical criterion") + per_normal[radical4] += 1 + expected = [hyperplane_count(n - 1), norm_counts(n - 1)[0] - 1] + need(per_normal == expected, "counts for every individual normal") + counts = [a + b for a, b in zip(counts, per_normal, strict=True)] + need(sum(counts) == len(lines) * (len(lines) - 1), "complete pair domain") + results.append({"dimension": n, "hyperplanes": len(lines), + "nondegenerate_ordered_pairs": counts[0], + "degenerate_ordered_pairs": counts[1]}) + return results + + +def orthogonal_families(): + """Exhaust every subset of the twelve normal lines in dimension three.""" + lines = norm_one_lines(3) + sizes = [0] * 13 + for mask in range(1 << len(lines)): + chosen = [v for j, v in enumerate(lines) if mask & (1 << j)] + safe = all(hermitian(u, v) == 0 for u, v in itertools.combinations(chosen, 2)) + if not safe: + continue + need(len(chosen) <= 3, "pairwise-safe family size") + basis = kernel([[CONJUGATE[x] for x in v] for v in chosen], 3) + rank4, rank2 = restriction_ranks(basis) + need(rank4 == len(basis) and rank2 == 2 * len(basis), + "higher intersection nondegenerate") + sizes[len(chosen)] += 1 + need(sizes[3] > 0 and sum(sizes[4:]) == 0, "sharp dimension-three cap") + return sizes[:4] + + +def must_reject(operation, message): + try: + operation() + except ValueError: + return + raise ValueError("control accepted: " + message) + + +def controls(): + u, v = (1, 0, 0), (1, 1, 1) + need(intersection(u, v) == (1, 2), "smallest failing witness") + for normal in (u, v): + basis = kernel([[CONJUGATE[x] for x in normal]], 3) + need(restriction_ranks(basis) == (2, 4), "nondegenerate input planes") + need(intersection((1, 0), (0, 1)) == (0, 0), "dimension-two safe control") + need(intersection(u, (0, 1, 0)) == (0, 0), "orthogonal safe control") + must_reject(lambda: intersection(u, u), "duplicate hyperplane") + must_reject(lambda: intersection(u, (0, 1, 1)), "isotropic normal") + must_reject(lambda: intersection((1,), (1,)), "dimension below domain") + must_reject(lambda: rref([[4]], 1), "invalid field entry") + must_reject(lambda: need(intersection(u, v) == (0, 0), "false closure"), + "nondegeneracy inherited by intersection") + must_reject(lambda: need(hyperplane_count(3) == (4**3 + (-2)**3) // 6, + "count sign mutation"), "wrong count sign") + must_reject(lambda: need(multiply(2, 2) == hermitian((2,), (2,)), + "unconjugated norm"), "missing conjugation") + must_reject(lambda: need(intersection(u, v)[1] == 1, "binary radical"), + "missing binary dimension doubling") + need(intersection(u, (1, 2, 1)) == (1, 2), "nonbinary coefficient witness") + return 8 + + +def receipt(result): + package = Path(__file__).resolve().parent + files = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in files} + print(json.dumps({"result": result, "package_sha256": hashes}, sort_keys=True)) + + +def main(): + field_cases, vector_cases = field_and_norm_checks() + result = {"field_triples": field_cases, "norm_vectors": vector_cases, + "census": census(), "safe_family_counts_dimension_three": orthogonal_families(), + "rejecting_controls": controls()} + receipt(result) + print("PASS_HERMITIAN_HYPERPLANE_INTERSECTIONS") + + +if __name__ == "__main__": + main()