From e1e6f9de0610b44072ff864cba8bb0d46062c02d Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Sat, 7 Nov 2026 23:26:00 +0800 Subject: [PATCH] Close the P104 block-dimension gap and sharpen the Hall witness Prove the sharp original subsystem value, transfer the known Petersen obstruction to the authenticated P104 mask, and derive the exact nonlinear binary broadcast corollary. Include independent exact certificate checks. Prepared for @CubeJerry with substantial OpenAI assistance. No new kappa. --- .../p104-sharp-block-hall-dimension/PROOF.md | 315 +++++++++++++++ .../p104-sharp-block-hall-dimension/README.md | 212 ++++++++++ .../SOURCES.json | 43 ++ .../p104-sharp-block-hall-dimension/TASK.json | 107 +++++ .../VERIFY.json | 53 +++ .../audit_petersen.py | 148 +++++++ .../petersen-dual.json | 377 ++++++++++++++++++ .../p104-sharp-block-hall-dimension/verify.py | 337 ++++++++++++++++ 8 files changed, 1592 insertions(+) create mode 100644 research/p104-sharp-block-hall-dimension/PROOF.md create mode 100644 research/p104-sharp-block-hall-dimension/README.md create mode 100644 research/p104-sharp-block-hall-dimension/SOURCES.json create mode 100644 research/p104-sharp-block-hall-dimension/TASK.json create mode 100644 research/p104-sharp-block-hall-dimension/VERIFY.json create mode 100644 research/p104-sharp-block-hall-dimension/audit_petersen.py create mode 100644 research/p104-sharp-block-hall-dimension/petersen-dual.json create mode 100644 research/p104-sharp-block-hall-dimension/verify.py diff --git a/research/p104-sharp-block-hall-dimension/PROOF.md b/research/p104-sharp-block-hall-dimension/PROOF.md new file mode 100644 index 0000000000..f8aeb29ca6 --- /dev/null +++ b/research/p104-sharp-block-hall-dimension/PROOF.md @@ -0,0 +1,315 @@ +# Proof: the two fourteen-port subsystems have different sharp dimensions + +All port numbers denote zero-based positions in the authenticated P104 source +array identified in [README.md](README.md). The zero relation is + +\[ +Z(v,w)\iff v\ne w\quad\text{and}\quad +\operatorname{popcount}(p_v\mathbin{\&}p_w)\equiv0\pmod2. +\] + +Throughout, `k` is a positive integer, `F` is an arbitrary field, and +`U_v,W_v` are `k × d` matrices over `F` satisfying the stated zero relation +and invertible diagonal pairings. A smaller subsystem imposes only the +constraints among its retained ports. + +## 1. Rank axioms from asymmetric labels + +Put `V_v=im(U_v^T)` and + +\[ +f(A)=\dim_F\!\left(\sum_{v\in A}V_v\right). +\] + +The diagonal invertibility gives `dim(V_v)=k`: if `U_v^T x=0`, then +`W_v U_v^T x=0`, whence `x=0`. Also `f(empty)=0`, `f(A)<=d`, and `f` is +monotone. The dimension formula, together with +`span(V_{A intersection B})` contained in +`span(V_A) intersection span(V_B)`, gives submodularity: + +\[ +f(A)+f(B)\ge f(A\cup B)+f(A\cap B). +\] + +If `v` is forced zero to every member of `A`, then `W_v` annihilates +`span(V_A)` and is injective on `V_v`. Their intersection is therefore zero, +so + +\[ +f(A\cup\{v\})-f(A)=k. \tag{Z} +\] + +This uses no symmetry assumption. Every subsequent inequality concerns +integer dimensions, so the rational certificate coefficients do not require +division by two in the field. + +## 2. Original subsystem: lower bound `ceil(17k/2)` + +Define + +\[ +I=\{74,81,86,91\},\qquad +S=\{62,63,69,99,67,68,95,100,101\}. +\] + +The original fourteen-port set in #6846 is `R0=I union S union {57}`. +Every member of `I` is forced zero to every member of `S` and to the other +members of `I`. Thus repeated application of (Z) gives +`f(I union S)=4k+f(S)`. Thirteen ports already suffice for the lower bound. + +To prove `2f(S)>=9k`, set + +~~~text +A = {62,69,99,68,100} +B = {62,99,67,95,100} +C = A union B +E = {69,67,100} +F = {62,100} +Q = {69,99,67,68,100} +T = {62,69,67} +~~~ + +The following finite premises are checked directly against the pinned ports: +`63` is forced zero to `A`; `101` to `B`; `99` to `F`; `95` to `Q`; +`68` to `E`; and the three members of `T` are pairwise forced zero. +The relevant set identities are + +\[ +A\cap B=F\cup\{99\},\quad E\cap F=\{100\},\quad +Q\cup\{95\}\subseteq C,\quad E\cup\{68\}\subseteq Q, +\quad T\subseteq E\cup F. +\] + +Consequently, + +\[ +\begin{aligned} +2f(S) +&\ge f(A)+f(B)+2k &&\text{by (Z) and monotonicity}\\ +&\ge f(C)+f(F)+3k &&\text{by submodularity and (Z) for 99}\\ +&\ge f(Q)+f(F)+4k &&\text{by (Z) for 95 and monotonicity}\\ +&\ge f(E)+f(F)+5k &&\text{by (Z) for 68 and monotonicity}\\ +&\ge f(E\cup F)+f(\{100\})+5k &&\text{by submodularity}\\ +&\ge 3k+k+5k=9k. &&\text{since T is pairwise forced zero} +\end{aligned} +\] + +Therefore + +\[ +d\ge f(I\cup S)=4k+f(S)\ge\frac{17k}{2}. +\] + +Since `d` is an integer, `d>=ceil(17k/2)`. The verifier independently expands +the displayed argument into 17 elementary axiom rows whose exact sum is +`2f(S)-9k>=0`, including every monotone inclusion and the empty-set identity. + +## 3. Original subsystem: matching upper bound for every field and block size + +A coordinate group assigns one ambient standard basis coordinate to every +port listed in that group. Let the rows of `U_v=W_v` be the distinct standard +coordinates assigned to port `v`. If every port receives `k` coordinates and +every forced-zero pair receives disjoint coordinate sets, the diagonal +pairing is `I_k` and all required off-diagonal products vanish over every +field. The ordering of the rows within a port can be fixed by increasing +coordinate index. + +For `k=2,d=17`, use two coordinates for each group in the first row and one +for each group in the second: + +| Multiplicity | Coordinate groups | +|---|---| +| 2 | `{74}`, `{81}`, `{86}`, `{91,57}`, `{99,67}`, `{69,100}` | +| 1 | `{62,68}`, `{62,95}`, `{63,95}`, `{63,101}`, `{68,101}` | + +There are `12+5=17` coordinates. Every original port receives two distinct +coordinates. Every two-port group is an allowed pair, as checked against the +source. This proves the `k=2,d=17` upper bound without arithmetic cancellation +or characteristic restrictions. + +For `k=1,d=9`, use one coordinate for each group + +~~~text +{74}, {81}, {86}, {91,57}, {99,67}, {69,100}, {62,68}, {63,95}, {101}. +~~~ + +For `k=2q+r`, `r in {0,1}`, take the direct sum of `q` copies of the first +construction and `r` copies of the second. Its inner dimension is + +\[ +17q+9r=\left\lceil\frac{17k}{2}\right\rceil. +\] + +Together with Section 2 this proves exactness for the original fourteen +ports. Restricting the same constructions proves exactness for the +thirteen-port lower-bound subset `I union S` as well. The nine-core `S` +itself has exact minimum `ceil(9k/2)`, by deleting the four isolated coordinate +blocks (each of dimension `k`) from the construction. + +## 4. Replacing port 57 by 61: the Petersen core + +Let + +\[ +P=S\cup\{61\}=\{61,62,63,67,68,69,95,99,100,101\}. +\] + +All four members of `I` are forced zero to every member of `P`; in fact `P` +is their complete common forced-zero neighborhood among all 104 ports. +The graph of allowed distinct pairs on `P` is the Petersen graph. An explicit +isomorphism to its outer-pentagon / inner-pentagram presentation is + +~~~text +outer = [61,69,100,62,95] +inner = [99,101,67,68,63]. +~~~ + +Its edges are exactly `outer[i]--outer[i+1]`, `outer[i]--inner[i]`, and +`inner[i]--inner[i+2]`, with indices modulo five. The verifier compares the +complete unordered edge sets; degree counts alone are not used to identify +the graph. The following rank argument is checked directly against the +source relation and does not rely on recognizing the graph name. + +### Exact all-field certificate for `f(P)>=5k` + +The file [petersen-dual.json](petersen-dual.json) contains 43 rows. The ordered +vertex list is `P` in the ascending order displayed above. For a subset mask +`s`, its set is `{P[i] : the i-th bit of s is 1}`. The row meanings are: + +| Descriptor | Left side | Right side | Type | +|---|---|---|---| +| `["mono",s,i]` | `f(s)-f(s+i)` | `0` | `<=` | +| `["submod",s,i,j]` | `f(s)+f(s+i+j)-f(s+i)-f(s+j)` | `0` | `<=` | +| `["zero",s,i]` | `f(s+i)-f(s)` | `k` | `=` | +| `["empty"]` | `f(empty)` | `0` | `=` | + +Here `s+i` denotes adjoining `P[i]`, not integer addition; each named vertex +is required to lie outside `s`. Every `zero` row has all its required +forced-zero contacts checked. All 26 inequality multipliers are `-1/2`, so +each multiplied inequality has the correct `>=` orientation. The 16 +zero-additivity rows have signed half-integer multipliers; equalities allow +either sign. The remaining row is the empty-set equality. + +Adding the rows gives **exactly** + +\[ +f(P)\ge5k. +\] + +More explicitly, the coefficient of `f(P)` is `1`; the coefficients of all +other subset-rank variables are zero; and the weighted sum of the +zero-additivity right sides is `5k`. Multiplying the entire certificate by +two yields integer coefficients. `verify.py` reconstructs the rows as +frozensets of actual port IDs and checks this identity with rational +arithmetic. The separately written `audit_petersen.py` reconstructs the rows +using bitmask variables and a different coefficient accumulator. Neither +uses numerical tolerances or trusts the reported LP objective. + +This finite exact axiom combination is a proof for every field and every +positive integer `k`, because Section 1 proves each axiom for every such +label system. A numerical linear program was used only to discover it. + +It follows that the replacement subsystem +`R1=I union P=(R0 minus {57}) union {61}` satisfies + +\[ +d\ge f(I\cup P)=4k+f(P)\ge9k. +\] + +The replacement subsystem attains `9k` over every field. Assign one block of +`k` standard coordinates to each singleton in `I` and to each matching edge + +~~~text +{61,69}, {62,95}, {63,101}, {67,100}, {68,99}. +~~~ + +These are five allowed disjoint edges covering all ten core ports. Every +port receives exactly one coordinate block, with `U_v=W_v` its standard +basis rows. This proves exactness of `9k` on `R1`, and of `5k` on `P`. + +## 5. Consequence for the full mask and its limits + +Any realization of all 104 ports restricts to `R1`, hence has `d>=9k` over +every field. In every characteristic-two field, interpreting each original +nine-bit port as a vector gives a scalar realization: odd weight makes the +diagonal one, and even overlap makes each forced-zero product zero. Tensoring +with `I_k` attains `9k`. Thus the full-mask minimum is exactly `9k` in +characteristic two. + +Over other characteristics, a binary dot product that is zero modulo two +need not be zero in the field. The argument therefore supplies only the +full-mask lower bound there. It supplies no necessity theorem for the label +pattern in a legal multiplication circuit and no reduction in complete +supplier cost. **No new κ.** + +The general Petersen lower bound and four-isolate construction precede this +work: see Thiago's #1744 and its credit to Blasiak, Kleinberg and Lubetzky. +The source-specific advance is the explicit P104 transfer, the sharp +original-subsystem contrast, and the exact closure of the open block +interval in DreamingOfClouds' #6846. + +## 6. Exact nonlinear binary broadcast corollary + +Use the same allowed-pair graph as a side-information graph. Each vertex `v` +has an independent uniform `k`-bit message `X_v`; receiver `v` knows the +messages at its allowed neighbors and must recover `X_v` without error. +Let `B` be any deterministic fixed-length binary broadcast, permitting +arbitrary nonlinear encoding and decoding. Write `V` for the vertex set and +define, with entropy measured in bits, + +\[ +r(S)=H(B\mid X_{V\setminus S}). +\] + +This function satisfies exactly the axioms used in both preceding proofs. +Deterministic encoding gives `r(empty)=0`. Removing conditioning variables +proves monotonicity. Moreover + +\[ +r(S)=H(B,X_{V\setminus S})-k|V\setminus S|. +\] + +Entropy submodularity, complementation of the index sets, and subtraction of +the displayed modular function prove submodularity of `r`. If `v` is forced +zero to every member of `S`, all neighbors of `v` belong to +`Z=V\setminus(S\cup\{v\})`. Independence and zero-error decoding give + +\[ +\begin{aligned} +r(S\cup\{v\})-r(S) + &=I(B;X_v\mid X_Z)\\ + &=H(X_v\mid X_Z)-H(X_v\mid B,X_Z)=k. +\end{aligned} +\] + +Thus the same 17-row short proof and 43-row certificate, already checked +exactly, are also entropy inequalities. In the full 104-port problem the +certificates bound `r(I union P)`, which is at most `r(V)=H(B)` by +monotonicity. Since an `L`-bit fixed-length broadcast has `H(B)<=L`, they imply + +| Side-information graph | Minimum fixed binary broadcast length | +|---|---| +| Original fourteen ports `R0` | `ceil(17k/2)` | +| Replacement fourteen ports `R1` | `9k` | +| Complete 104-port graph | `9k` | + +Here the lower bounds apply to nonlinear encoders. The upper bounds are +explicit linear codes. For each coordinate in a subsystem witness, transmit +the XOR of the message bits assigned to that coordinate. Every other port +sharing the coordinate is an allowed neighbor, so a receiver subtracts the +known bits and recovers its own bit. The verified coordinate assignments give +the stated lengths for every `k`, using direct sums for the original odd-width +case. + +For the full graph, broadcast the nine `k`-bit blocks +`B_a = XOR_{v: ports[v]_a=1} X_v`. Receiver `v` XORs those blocks selected by +its port vector. Its own coefficient is one; every other nonzero coefficient +is on an allowed neighbor, so it can subtract those known messages. The +existing full binary Gram check verifies all these coefficients. + +This is a source-specific index-coding corollary of the same certificate, +following the established entropy/Petersen method in #1744. The general +nonlinear Petersen result is credited there to Blasiak, Kleinberg and Lubetzky. +No new universal entropy inequality is claimed. This fixed-length zero-error +broadcast model is an explicit assumption and is not a physical reversible +supplier or a paid multiplication algorithm. diff --git a/research/p104-sharp-block-hall-dimension/README.md b/research/p104-sharp-block-hall-dimension/README.md new file mode 100644 index 0000000000..3a0e9f88a2 --- /dev/null +++ b/research/p104-sharp-block-hall-dimension/README.md @@ -0,0 +1,212 @@ +# Sharp block dimensions for the P104 Hall mask + +**No new κ.** Under the exact asymmetric label-pattern hypothesis of +CrocSwap/integer-mult-bounds#6846, the complete P104 mask requires inner +dimension **at least `9k` over every field**, for every positive integer block +size `k`. This closes the interval `8k < d < 9k` left open there. The proof +transfers the established four-isolates-plus-Petersen obstruction to an +authenticated P104 subconfiguration; it does not introduce a new general +Petersen rank theorem. + +The predecessor's original fourteen ports behave differently: their exact +minimum is **`ceil(17k/2)` over every field**. In particular, `k=2,d=17` is +possible on that subsystem. Replacing just port `57` by port `61` produces +another fourteen-port subsystem whose exact minimum is `9k`. The distinction +explains both why the original Hall witness cannot exclude the whole block +interval and why the full source mask nevertheless does. + +| Object, with the zero convention below | Proven minimum / lower bound | +|---|---| +| Original fourteen ports from #6846 | Exact `ceil(17k/2)` over every field | +| Same selection with `57` replaced by `61` | Exact `9k` over every field | +| All 104 source ports | At least `9k` over every field | +| All 104 source ports in characteristic two | Exact `9k` | + +No dimension-`9k` upper bound for the full mask in other characteristics is +asserted. No supplier circuit or complete paid invoice is constructed. + +The same exact certificates also give an index-coding corollary: even with +arbitrary nonlinear deterministic encoding, the minimum fixed-length binary +broadcast for independent `k`-bit messages is `ceil(17k/2)` on the original +subsystem and `9k` on the replacement subsystem and full 104-port graph. +Section 6 of [PROOF.md](PROOF.md) supplies the entropy reduction and explicit +attaining parity broadcasts. This abstract side-information model does not +establish a physical supplier or change κ. + +## Exact object and hypothesis + +The input is the unchanged +[#5561 word](../p104-designer-toolkit-v2/words/5561.json.gz) at canonical base +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +Its compressed SHA256 is +`b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44`; +Git blob `c367d865a154ffd2ae0b6f6053469580a139f487`. +The `ports` array contains 104 distinct odd-weight nine-bit integers. All +indices below are zero-based array positions, not port integer values. + +For a field `F`, choose arbitrary `k × d` matrices `U_v,W_v` for each retained +port. Require `W_v U_v^T` to be invertible and require +`W_v U_w^T=0` whenever `v != w` and +`popcount(ports[v] & ports[w])` is even. Both ordered products are constrained +on a forced-zero pair; no symmetry or equality of `U` and `W` is assumed. +Additional zeros are permitted. + +This is exactly the explicit pattern hypothesis in #6846. It is **not** +established here for every legal multiplier, caller, frame change, or decoder. +In particular, it must not be confused with the opposite parity convention +used for the real-valued completion in +[P104-LEMMAS.md](../p104-designer-toolkit-v2/P104-LEMMAS.md). + +## What is new relative to the archive + +DreamingOfClouds' #6846 proves impossibility at `d=8k` from +`K={62,63,69,74,81,86,91,99}` and `O={57,67,68,95,100,101}`. +Its second open question explicitly leaves intermediate block dimensions +unsettled. The reviewed predecessor head is +`01651795be9570c47977a73f9cf3e8eeb3fbe64a` in +`DreamingOfClouds/integer-mult-bounds`; the scope here is that stated mask and +question, not an unmerged circuit dependency. + +The relevant earlier archive result is Thiago's merged #1744, +[research/p112-characteristic-two-minrank](../p112-characteristic-two-minrank/README.md), +head `78033981ec296b545b3cb50435668fe98e764e65`. It already proves the same +all-field `9k` obstruction on P111 and P112 by embedding four isolates and a +Petersen graph, with an exact 113-term certificate in an augmented-rank +formulation. It credits the known Petersen broadcast-rate theorem to +[Blasiak, Kleinberg and Lubetzky, Fact 5.6(1)](https://www.cs.cornell.edu/~ablasiak/papers/bkl-beta.pdf). +The present package connects that mechanism to the precise P104 question: + +- It authenticates a concrete P104 embedding using only fourteen source ports. +- It proves the sharp `ceil(17k/2)` value of the predecessor's original + fourteen-port selection, including a `k=2,d=17` witness. +- It gives a separate 43-row exact subspace-rank certificate for the Petersen + core and checks it with two separately written implementations. +- It explicitly separates the full-mask lower bound, subsystem sharpness, + characteristic-two full-mask sharpness, and unproved supplier applicability. + +The smaller certificate is given for inspectability; its row count is not a +performance comparison with the different formulation in #1744. No novelty is +claimed for fractional Haemers representations, coordinate-cover upper +bounds, the Petersen value, or the natural binary upper construction. See also +[Bukh and Cox, *On a fractional version of Haemers' bound*, arXiv:1802.00476v2](https://arxiv.org/abs/1802.00476v2), +Section 2, for the block-fitting framework. + +## Proof and exact witnesses + +[PROOF.md](PROOF.md) gives the linear-algebra argument and a short hand proof +of the original subsystem's lower bound. For any admissible labels, let +`f(A)` be the dimension of the sum of the row spaces of the matrices `U_v` +for `v in A`. This is a monotone submodular rank function. If `v` is forced +zero to every member of `A`, the invertible diagonal pairing implies the +exact identity `f(A+v)=f(A)+k`. This elementary fact handles asymmetric labels +and every characteristic. + +Four ports `I={74,81,86,91}` are isolated in the allowed-pair graph. Their +common forced-zero neighborhood is exactly +`P={61,62,63,67,68,69,95,99,100,101}`. The allowed-pair graph on `P` is the +Petersen graph. The exact certificate establishes `f(P)>=5k`, hence +`d>=f(P+I)>=9k`. The same four isolated ports combined with +`S=P-{61}` give the original subsystem's `17k/2` lower bound. A two-coordinate +assignment per port attains it at `k=2`, and direct sums give all block sizes. + +The universal statements follow from the displayed proof and exact axiom +combination, not from finite searches. The numerical linear programs used to +discover the certificate are absent from the trusted replay. + +## Reproduce and expected result + +From the repository root, with Python 3.12 and no external dependencies: + +```sh +python3.12 scripts/research_package.py --package research/p104-sharp-block-hall-dimension +``` + +The registered replay runs both verifiers normally and with `-O`. Expected +markers are `PASS_P104_SHARP_BLOCK_HALL_DIMENSION` and +`PASS_P104_PETERSEN_EXACT_RANK_PROOF`, each twice. Direct standalone replay is +`python3.12 -I -B research/p104-sharp-block-hall-dimension/verify.py`. + +The main verifier authenticates the source bytes and index convention, +expands all 17 axiom rows of the short proof, regenerates all 43 Petersen +certificate rows as sets of actual port IDs, checks their coefficient sum +exactly, verifies an explicit Petersen isomorphism, checks all ordered +required pairings of the coordinate witnesses for `k=1,...,12`, and computes +all 10,816 entries of the binary full-mask Gram matrix. `audit_petersen.py` +was separately written and checks the same Petersen certificate using an +integer-mask coefficient accumulator. Neither implementation imports the +other, a predecessor verifier, or a numerical optimizer. + +Ten main negative controls reject a source-byte mutation, a removed required +zero, the reversed parity convention, a reversed inequality sign, a deleted +inequality, a changed equality coefficient, a false zero premise, a corrupted +upper witness, deletion of its seventeenth coordinate, and a singular +diagonal. The separate audit has four coefficient/premise controls. All +acceptance gates use explicit exceptions and remain active under `-O`. +The finite block-size runs check implementations of the explicit witnesses; +the direct-sum proof establishes all positive integer block sizes. + +## Scope, assumptions and completion status + +This is a completed rank-geometry side result, not a completed answer to the +catalogue's supplier-budget question. The original catalogue card is retained +in [TASK.json](TASK.json), with the scope change recorded. Exact live input and +historical provenance pins are in [SOURCES.json](SOURCES.json). Reproduction +commands and input-trigger declarations are in [VERIFY.json](VERIFY.json). +The coordinated claim was local-only because the connected GitHub interface +could not post to the current Discussion board; no reservation issue was +created. + +The selected record at the base reports `κ=0.003125804`. This package leaves +that record and its five framework assumptions untouched: `native_all_columns`, +`owned_erasure`, `compiler`, `precision_tape`, and `analytic_recovery`. The +rank proof itself uses none of those assumptions; applying it to a proposed +supplier requires a separate proof that the supplier obeys the label pattern. +No partial numerical improvement or optimistic invoice is promoted to a +multiplication bound. + +## Open next questions + +1. **Applicability or paid relaxation.** For a particular legal caller, which + operations force exactly this zero pattern, and can a priced helper change + enough contacts to remove the Petersen witness? A useful first step is to + map the fourteen required contacts to that caller's explicit operations, + then price every altered boundary, restoration and ownership cost. An + abstract graph relaxation alone cannot improve the selected bound. +2. **Full-mask upper bounds outside characteristic two.** What is the exact + block-rank parameter over a specified field such as the rationals or + complex numbers? The present `9k` lower bound remains valid, but the binary + upper construction does not transfer merely by interpreting its entries + as integers. A first step is a source-pinned fitting construction or a + stronger exact rank certificate; no such construction is supplied here. + +## Attribution + +Prepared by **@CubeJerry**, with substantial **OpenAI GPT-6 Astra Pro** +assistance for mathematical exploration, proof writing, exact checks and +packaging. The original-subsystem proof and the Petersen extension were +independently developed within the research team and then cross-checked; +the two certificate checkers were written separately. The final arguments +and their precise limits are recorded above. + +The entropy corollary was derived separately by the lead and checked by the +rank-proof worker before integration. It uses the same verified source contacts, +axiom coefficients and upper-witness Gram entries; no finite experiment is +presented as a proof about all nonlinear codes. + +Credit DreamingOfClouds for the Hall witness and open question in #6846; +Thiago for the source-bound P111/P112 obstruction and verification approach +in #1744; Blasiak, Kleinberg and Lubetzky for the underlying Petersen result; +Bukh and Cox for the fractional Haemers framework; and the authors of #5561 +and its credited predecessors for the unchanged P104 native word. Inputs are +referenced without modification or re-vendoring. New work is Apache-2.0; +existing source attribution and licenses remain applicable. + +## Concurrent work checked at completion + +DreamingOfClouds' open #6854, head +`3d355ae61f174c5f7101c9eb292722afa5a5f9ac`, excludes dimension exactly `8k` +for every subset of at least 97 of the 120 E8 lines under its stated mask. +It explicitly leaves `8k= 0 and has nonnegative weight. Equalities + may have signed weights. A zero identity is f(A+v)-f(A)-k = 0. + Sets contain actual source port IDs, not subset-mask integer variables. + """ + def __init__(self, vertices, zero): + self.vertices = frozenset(vertices) + self.zero_pair = zero + self.coefficients = defaultdict(Fraction) + self.k_coefficient = Fraction() + self.rows = 0 + + def term(self, vertices, coefficient): + vertices = frozenset(vertices) + require(vertices <= self.vertices, 'rank set outside universe') + self.coefficients[vertices] += Fraction(coefficient) + + def monotonicity(self, smaller, larger, weight=1): + weight = Fraction(weight) + require(weight >= 0 and set(smaller) <= set(larger), 'monotonicity premise/sign') + self.term(larger, weight) + self.term(smaller, -weight) + self.rows += 1 + + def submodularity(self, first, second, weight=1): + weight = Fraction(weight) + require(weight >= 0, 'submodularity multiplier sign') + first, second = frozenset(first), frozenset(second) + self.term(first, weight) + self.term(second, weight) + self.term(first | second, -weight) + self.term(first & second, -weight) + self.rows += 1 + + def zero_additivity(self, base, vertex, weight=1): + base, weight = frozenset(base), Fraction(weight) + require(vertex in self.vertices and vertex not in base, 'zero identity vertex') + require(all(self.zero_pair(vertex, other) for other in base), 'false zero identity') + self.term(base | {vertex}, weight) + self.term(base, -weight) + self.k_coefficient -= weight + self.rows += 1 + + def empty(self, weight=1): + self.term((), weight) + self.rows += 1 + + def conclude(self, vertices, multiplier, k_bound): + actual = {a: c for a, c in self.coefficients.items() if c} + require(actual == {frozenset(vertices): Fraction(multiplier)}, + 'rank coefficients do not cancel to stated target') + require(self.k_coefficient == -k_bound, 'rank certificate k coefficient') + return self.rows + + +def check_nine_core(zero): + """Expand the short proof from PROOF.md, including every monotone step.""" + A = frozenset((62, 69, 99, 68, 100)) + B = frozenset((62, 99, 67, 95, 100)) + C = A | B + E = frozenset((69, 67, 100)) + F = frozenset((62, 100)) + Q = frozenset((69, 99, 67, 68, 100)) + T = frozenset((62, 69, 67)) + ledger = RankLedger(S, zero) + ledger.monotonicity(A | {63}, S) + ledger.zero_additivity(A, 63) + ledger.monotonicity(B | {101}, S) + ledger.zero_additivity(B, 101) + ledger.submodularity(A, B) + require(A & B == F | {99}, 'short proof intersection') + ledger.zero_additivity(F, 99) + ledger.monotonicity(Q | {95}, C) + ledger.zero_additivity(Q, 95) + ledger.monotonicity(E | {68}, Q) + ledger.zero_additivity(E, 68) + ledger.submodularity(E, F) + require(E & F == {100}, 'short proof final intersection') + ledger.monotonicity(T, E | F) + ledger.zero_additivity((), 62) + ledger.zero_additivity({62}, 69) + ledger.zero_additivity({62, 69}, 67) + ledger.zero_additivity((), 100) + ledger.empty(2) + return ledger.conclude(S, 2, 9) + + +def check_petersen(certificate, zero): + """Independently translate the lead's bitmask certificate to port sets.""" + require(certificate['vertices'] == P, 'Petersen vertex order') + ledger = RankLedger(P, zero) + def subset(mask): + require(type(mask) is int and 0 <= mask < 2 ** len(P), 'subset mask') + return frozenset(v for i, v in enumerate(P) if (mask >> i) & 1) + def vertex(index): + require(type(index) is int and 0 <= index < len(P), 'vertex index') + return P[index] + for descriptor, coefficient in certificate['ub']: + require(len(descriptor) in (3, 4), 'inequality descriptor length') + coefficient = -Fraction(coefficient) + require(coefficient >= 0, 'inequality multiplier sign') + base = subset(descriptor[1]) + v = vertex(descriptor[2]) + require(v not in base, 'inequality vertex in base') + if descriptor[0] == 'mono': + require(len(descriptor) == 3, 'monotonicity descriptor') + ledger.monotonicity(base, base | {v}, coefficient) + else: + require(descriptor[0] == 'submod' and len(descriptor) == 4, + 'submodularity descriptor') + w = vertex(descriptor[3]) + require(w not in base and v != w, 'submodularity vertices') + ledger.submodularity(base | {v}, base | {w}, coefficient) + for descriptor, coefficient in certificate['eq']: + if descriptor == ['empty']: + ledger.empty(coefficient) + else: + require(len(descriptor) == 3 and descriptor[0] == 'zero', 'equality descriptor') + ledger.zero_additivity(subset(descriptor[1]), vertex(descriptor[2]), coefficient) + return ledger.conclude(P, 1, 5) + + +def check_petersen_graph(zero): + # Standard outer pentagon / inner pentagram presentation, with five spokes. + outer = [61, 69, 100, 62, 95] + inner = [99, 101, 67, 68, 63] + expected = set() + for i in range(5): + expected.add(frozenset((outer[i], outer[(i+1) % 5]))) + expected.add(frozenset((outer[i], inner[i]))) + expected.add(frozenset((inner[i], inner[(i+2) % 5]))) + actual = {frozenset((u,v)) for u,v in combinations(P, 2) if not zero(u,v)} + require(actual == expected and len(expected) == 15, 'Petersen graph isomorphism') + + +def check_isolated_sum(core, zero): + require(all(zero(i, j) for i, j in combinations(I, 2)), 'four mutually zero ports') + require(all(zero(i, v) for i in I for v in core), 'isolate/core contact') + ledger = RankLedger(set(core) | I, zero) + previous = frozenset(core) + for i in sorted(I): + ledger.zero_additivity(previous, i) + previous = previous | {i} + require({a:c for a,c in ledger.coefficients.items() if c} == + {frozenset(core): Fraction(-1), frozenset(core) | I: Fraction(1)}, + 'isolated-sum identity') + require(ledger.k_coefficient == -4, 'isolated-sum constant') + + +OLD_ONE = [(74,), (81,), (86,), (91,57), (99,67), (69,100), + (62,68), (63,95), (101,)] +OLD_TWO = [group for group in [(74,), (81,), (86,), (91,57), (99,67), (69,100)] + for _ in range(2)] + [(62,68), (62,95), (63,95), (63,101), (68,101)] +NEW_ONE = [(74,), (81,), (86,), (91,), (61,69), (62,95), (63,101), (67,100), (68,99)] + + +def coordinates(groups, vertices): + result = {v: [] for v in vertices} + for coordinate, group in enumerate(groups): + require(len(group) == len(set(group)), 'duplicate port in coordinate group') + for v in group: + require(v in result, 'coordinate uses unknown vertex') + result[v].append(coordinate) + return result, len(groups) + + +def direct_sum(parts, vertices): + result = {v: [] for v in vertices} + offset = 0 + for mapping, dimension in parts: + require(set(mapping) == set(vertices), 'direct-sum coverage') + for v in vertices: + result[v].extend(offset + coordinate for coordinate in mapping[v]) + offset += dimension + return result, offset + + +def check_coordinate_pairings(mapping, dimension, k, vertices, zero): + require(set(mapping) == set(vertices), 'upper witness vertex coverage') + for v in vertices: + require(len(mapping[v]) == k, 'upper witness row count') + require(all(type(c) is int and 0 <= c < dimension for c in mapping[v]), + 'upper witness coordinate outside dimension') + diagonal = [[int(a == b) for b in mapping[v]] for a in mapping[v]] + require(diagonal == [[int(i == j) for j in range(k)] for i in range(k)], + 'upper witness diagonal is not identity') + for v, w in product(vertices, repeat=2): + if zero(v, w): + require(all(a != b for a in mapping[v] for b in mapping[w]), + 'upper witness violates a forced zero') + + +def check_full_characteristic_two(ports): + """Literal 9-bit rows; integer parity checks certify every Gram entry.""" + rows = [[(p >> bit) & 1 for bit in range(9)] for p in ports] + for i, j in product(range(104), repeat=2): + entry = sum(x*y for x, y in zip(rows[i], rows[j])) % 2 + expected = (ports[i] & ports[j]).bit_count() % 2 + require(entry == expected, 'binary Gram entry') + require(i != j or entry == 1, 'binary diagonal') + # Exact binary elimination is a consistency check, not the lower proof. + basis = {} + for value in ports: + while value: + bit = value.bit_length() - 1 + if bit in basis: + value ^= basis[bit] + else: + basis[bit] = value + break + require(len(basis) == 9, 'binary port rank') + + +def rejects(call, label): + try: + call() + except ValueError: + return label + raise ValueError('negative control was accepted: ' + label) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--source', type=Path, default=SOURCE) + args = parser.parse_args() + raw = args.source.read_bytes() + ports = source_ports(raw) + zero = zero_relation(ports) + cert = json.loads((HERE / 'petersen-dual.json').read_text()) + short_rows = check_nine_core(zero) + petersen_rows = check_petersen(cert, zero) + check_petersen_graph(zero) + check_isolated_sum(S, zero) + check_isolated_sum(P, zero) + require([v for v in range(104) if all(zero(v, i) for i in I)] == P, + 'common forced-zero neighborhood') + one, two, new = coordinates(OLD_ONE, OLD), coordinates(OLD_TWO, OLD), coordinates(NEW_ONE, NEW) + for k in range(1, 13): + q, r = divmod(k, 2) + old_map, old_d = direct_sum([two] * q + [one] * r, OLD) + require(old_d == (17*k + 1)//2, 'old dimension formula') + check_coordinate_pairings(old_map, old_d, k, OLD, zero) + new_map, new_d = direct_sum([new] * k, NEW) + require(new_d == 9*k, 'new dimension formula') + check_coordinate_pairings(new_map, new_d, k, NEW, zero) + check_full_characteristic_two(ports) + controls = [] + controls.append(rejects(lambda: source_ports(raw[:-1] + bytes((raw[-1] ^ 1,))), 'source-byte mutation')) + controls.append(rejects(lambda: check_nine_core(lambda u,v: zero(u,v) and {u,v} != {62,63}), + 'missing zero in short proof')) + controls.append(rejects(lambda: check_nine_core(lambda u,v: u != v and not zero(u,v)), + 'reversed parity convention')) + bad = deepcopy(cert); bad['ub'][0][1] = '1/2' + controls.append(rejects(lambda: check_petersen(bad, zero), 'reversed inequality multiplier')) + bad = deepcopy(cert); bad['ub'].pop() + controls.append(rejects(lambda: check_petersen(bad, zero), 'deleted inequality')) + bad = deepcopy(cert); bad['eq'][-1][1] = '3/2' + controls.append(rejects(lambda: check_petersen(bad, zero), 'altered equality multiplier')) + bad = deepcopy(cert) + row = next(row for row in bad['eq'] if row[0][0] == 'zero') + v = P[row[0][2]] + row[0][1] = 1 << next(j for j,w in enumerate(P) if w != v and not zero(v,w)) + controls.append(rejects(lambda: check_petersen(bad, zero), 'false zero premise')) + bad_map = deepcopy(two[0]); bad_map[63][0] = bad_map[62][0] + controls.append(rejects(lambda: check_coordinate_pairings(bad_map, 17, 2, OLD, zero), + 'forced-zero collision in upper witness')) + bad_map = {v: [c for c in cs if c != 16] for v,cs in two[0].items()} + controls.append(rejects(lambda: check_coordinate_pairings(bad_map, 16, 2, OLD, zero), + 'deleted seventeenth coordinate')) + bad_map = deepcopy(two[0]); bad_map[62][1] = bad_map[62][0] + controls.append(rejects(lambda: check_coordinate_pairings(bad_map, 17, 2, OLD, zero), + 'singular diagonal in upper witness')) + print(json.dumps({'source_sha256': SOURCE_HASH, 'short_proof_axiom_rows': short_rows, + 'petersen_certificate_rows': petersen_rows, + 'original_14_minimum_all_fields': 'ceil(17k/2)', + 'replacement_14_minimum_all_fields': '9k', + 'full_104_lower_all_fields': '9k', + 'full_104_minimum_characteristic_two': '9k', + 'coordinate_block_sizes_executed': list(range(1,13)), + 'negative_controls_rejected': controls}, indent=2)) + print('PASS_P104_SHARP_BLOCK_HALL_DIMENSION') + + +if __name__ == '__main__': + main()