From b59f9c29bedfb3e2e227f63afb5f630e73a3cd6a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:12:25 +0000 Subject: [PATCH] feat(research): prove sharp sunflower downset inertia --- research/sunflower-downset-inertia/README.md | 266 +++++++++++++++++ .../sunflower-downset-inertia/SOURCES.json | 30 ++ research/sunflower-downset-inertia/TASK.json | 109 +++++++ .../sunflower-downset-inertia/VERIFY.json | 32 ++ research/sunflower-downset-inertia/verify.py | 278 ++++++++++++++++++ 5 files changed, 715 insertions(+) create mode 100644 research/sunflower-downset-inertia/README.md create mode 100644 research/sunflower-downset-inertia/SOURCES.json create mode 100644 research/sunflower-downset-inertia/TASK.json create mode 100644 research/sunflower-downset-inertia/VERIFY.json create mode 100644 research/sunflower-downset-inertia/verify.py diff --git a/research/sunflower-downset-inertia/README.md b/research/sunflower-downset-inertia/README.md new file mode 100644 index 0000000000..1e89b8c8ac --- /dev/null +++ b/research/sunflower-downset-inertia/README.md @@ -0,0 +1,266 @@ +# Sharp integer inertia certificates for sunflower downsets + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: **scoped mathematical proof with exact finite corroboration**. +Every downset generated by a finite sunflower of maximal sets has a +nonsingular, symmetric, nonnegative integer matrix supported on disjoint +pairs whose number of positive eigenvalues equals its largest star size. +The construction also gives the exact determinant. The new case has three +or more maximal sets. It resolves the disjoint-petal first case left in +Nick Petalas's [#5247](https://github.com/CrocSwap/integer-mult-bounds/pull/5247). + +This proves the sunflower subclass of Ellis, Filmus and Friedgut's +[spectral Conjecture I, section 4](https://arxiv.org/html/2609.28404v1#S4), +recorded as C070 in David Ganz's +[atlas #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849). +The general downset conjecture remains open here. Global literature +priority, independent human review and formal proof-kernel review are +unclaimed. No new kappa or selected-frontier change is claimed. + +## Statement and construction + +Let C,A_0,...,A_(r-1) be pairwise disjoint finite sets, with + +```text +r >= 3, a_0 >= a_1 >= ... >= a_(r-1) >= 1, a_i = |A_i|, c = |C|, +D = union over i of 2^(C union A_i), +L = 1 + sum_i (2^a_i - 1), N = 2^c L. +``` + +These are precisely the downsets whose three or more maximal sets form a +sunflower. One or two maximal sets are covered by the cited predecessor. +Choose injections phi_i:A_i -> A_0 for i>=1, and let phi_0 be the identity. +The injections define weights only. They do not identify actual ground +elements from different petals. + +First take c=0. List every subset of A_0, then the nonempty subsets of +each other petal. This lists D once. Define a symmetric base matrix K. +Within one petal, use ordinary disjointness entries. Between subsets S,T +from different petals, put k=|phi_i(S) intersect phi_j(T)| and use + +```text + k = 0 k >= 1 +one petal is A_0: 1 2^k - 1 +neither is A_0: 1 2^(k+1) - 3. +``` + +Every cross-petal pair is disjoint in the actual ground set. All displayed +weights are positive integers. Within a petal, the only nonzero diagonal +entry is at the empty set, and it is 1. + +For general c, write a set uniquely as R union U, with R subset C and U +a base label, and set + +```text +M((R,U),(R',V)) = 1[R intersect R' is empty] K(U,V). +``` + +Then M is nonnegative, integral, symmetric and zero whenever its two +indexing sets intersect. Let s denote the largest star size. The formulas +are + +```text +s = 2^(a_0-1) if c=0; s = N/2 if c>=1, +e = 2^c sum_(i=1)^(r-1) (2^(a_i-1)-1), +inertia(M) = (s, N-s, 0), +det(M) = (-1)^(N-s) 3^e. +``` + +Thus the optimal number of nonnegative eigenvalues is exactly s, even +when the competing matrices may have arbitrary real supported entries. + +## Proof + +The Boolean zeta congruence and the dominant-to-one-petal block below are +the credited ingredients of #5247. The new step chooses all the other +cross blocks simultaneously and cancels every off-diagonal Schur block. +The argument is written in full to specify that new construction; no +predecessor executable is imported or replayed. + +For the cube on a set A, put + +```text +Z_A(S,T) = 1[T subset S], +J_A(T,T) = (-1)^|T|, +D_A(S,T) = 1[S intersect T is empty]. +``` + +In an inclusion-compatible order Z_A is unit lower triangular, and +`D_A = Z_A J_A Z_A^T`, since the entry is the alternating subset sum +over S intersect T. For each i>=1, let Z_i' and J_i' be the restrictions +to nonempty subsets of A_i, and put u_i(T)=(-1)^(|T|+1). Then + +```text +Z_i' u_i = 1, +D_A_i[nonempty,nonempty] = Z_i' (J_i' + u_i u_i^T) Z_i'^T. +``` + +Let e_0 be the empty-subset coordinate of the full A_0 cube. Define E_i +with columns indexed by nonempty T subset A_i. Its column is the standard +coordinate vector at phi_i(T) when |T| is even, and zero when |T| is odd. +Injectivity gives + +```text +J_A_0 E_i = E_i, e_0^T E_i = 0, +E_i^T E_i = diag(1[|T| is positive and even]). +``` + +Set H_i=e_0 u_i^T+2E_i. Under congruence by +`Z=diag(Z_A_0,Z_1',...,Z_(r-1)')`, K has the blocks + +```text +B_00 = J_A_0, +B_0i = H_i, +B_ii = J_i' + u_i u_i^T, +B_ij = u_i u_j^T + 4 E_i^T E_j for distinct i,j >= 1, +K = Z B Z^T. +``` + +To check the explicit weights, Z_A_0 E_i Z_i'^T counts nonempty even +subsets of S intersect phi_i(T). The analogous cross expression +`Z_i' E_i^T E_j Z_j'^T` counts nonempty even subsets of +phi_i(S) intersect phi_j(T). If this intersection has size k, the count +is zero at k=0 and `2^(k-1)-1` at k>=1. Adding the all-ones term and +multiplying that count by 2 or 4 gives exactly the two weight formulas. + +Eliminate B_00. It is its own inverse. For every i,j>=1, + +```text +H_i^T J_A_0 H_j = u_i u_j^T + 4 E_i^T E_j. +``` + +Therefore all off-diagonal Schur blocks vanish, and diagonal block i is + +```text +J_i' - 4 E_i^T E_i + = diag(-1 on odd subsets, -3 on nonempty even subsets). +``` + +This is negative definite, independently of how many petals there are or +how their injected images overlap in A_0. Sylvester's law of inertia +gives exactly `2^(a_0-1)` positive eigenvalues. Every other eigenvalue is +negative. The zeta and Schur congruence factors have determinant one. +There are `sum_(i>=1)(2^(a_i-1)-1)` entries -3, which proves the base +determinant's absolute value and its sign from the negative eigenvalues. + +For c>=1, `M=D_C tensor K`. The invertible symmetric D_C has equally +many positive and negative eigenvalues, by its zeta congruence. Hence +M has N/2 of each sign. Also |det D_C|=1, so +`|det M|=|det K|^(2^c)`. This proves both general formulas. + +When c=0, an element of A_i belongs to exactly `2^(a_i-1)` sets. When +c>=1, an element of C belongs to N/2 sets. A petal element belongs to +`2^c 2^(a_i-1)<=N/2` sets because L>=2^a_i. These counts give s above. + +Finally a star of size s indexes a zero principal block in every real +symmetric disjointness-supported matrix. Its quadratic form vanishes on +that s-dimensional coordinate subspace. If there were fewer than s +nonnegative eigenvalues, the negative eigenspace would have dimension +greater than N-s and intersect this subspace nontrivially. That would +contradict negative definiteness. This proves the asserted optimality. + +## First new example and finite evidence + +For three disjoint two-element facets, N=10 and s=2. The construction has +inertia `(2,8,0)` and determinant 9. Its weights between the full facets +are 3,3,5. Keeping the two dominant cross weights 3 but changing the last +weight to 1 gives inertia `(3,7,0)` and determinant -7. Changing that last +weight to 3 retains sharp inertia but changes the determinant to 5. This +control distinguishes exact Schur cancellation from mere sharp inertia. +Weakening the coupling coefficient 2 to 1 gives `(2,6,2)`, with four +nonnegative eigenvalues, so zero eigenvalues must be counted. + +The standalone standard-library verifier enumerates all 50 nonincreasing +positive petal-size/core tuples with r>=3 and +`c+sum_i a_i<=7`. Matrices have order at most 64. It builds actual disjoint +ground-set labels, checks all 23,333 support entries and the largest stars, +and independently computes exact inertia and determinant by rational +symmetric elimination with both one- and two-dimensional pivots. It also +checks the integer zeta congruence and all 785 leaf Schur entries across +these cases. Thirteen named controls include the new example, changed +weights, null-eigenvalue counting, zero-diagonal pivots and invalid inputs. +No two-facet predecessor cases are replayed. + +The universal result rests on the written proof. These finite checks +corroborate the construction and test its failure modes. JSON stdout is +generated from the actual checks and binds all five package files by +SHA256. No receipt is handwritten or committed. The verifier writes no +files and does not fetch or import predecessor sources. + +From the repository root, any CPython 3.12 may replace this local path: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/sunflower-downset-inertia/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/sunflower-downset-inertia/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sunflower-downset-inertia +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sunflower-downset-inertia --check-source-history +``` + +Expected scientific marker: `PASS_SUNFLOWER_DOWNSET_INERTIA`. The last +command checks publication bytes and source history after committing. + +## Implementation bounds and limitations + +Every loop has a finite bound from seven ground coordinates, seven petals, +matrix order 64 or the fixed five-file inventory. The parameter iterator +examines at most 1,716 tuples for each of five petal counts; only 50 pass +the stated domain. Symmetric elimination removes at least one coordinate +per iteration and uses at most 64 iterations. No recursive calls, dynamic +code evaluation, subprocesses or external runtime dependencies occur. +All functions fit within sixty physical lines. Explicit exception checks +remain active under optimization. + +Power-of-Ten rule 3 has a managed-runtime deviation in verify.py: CPython +allocates lists and exact integers/rationals during execution. Fixed input +and matrix capacities bound live work; there are no external parameters or +unbounded streams. A future parameterized checker must enforce size and +bit-length budgets before lifting these capacities. Rule 9 has six fixed +local rejection callbacks, used immediately and retaining no state. Their +only targets are the literal-matrix validator and the label validator. +Warning-strict normal and optimized execution and AST inspection supply +available diagnostics; a standalone linter is not installed in this +interpreter. No shared build configuration is changed. + +General overlapping-facet downsets, a weighted-Hoffman certificate, +physical preparation, recursive callers, precision, stock and supplier +admission remain outside scope. Lean, Docker and the selected cold replay +were not run. This is not a complete multiplication theorem. + +## Credit and overlap + +David Ganz's #2849 supplies atlas C070. Ellis, Filmus and Friedgut supply +the spectral conjecture. Nick Petalas's #5247 supplies the two-facet +construction, the Boolean-zeta/one-petal Schur argument and the explicit +three-facet first question. Classical zeta inversion and Sylvester's law +retain their credit. The new step is the simultaneous leaf cross-block +construction, its all-petal cancellation and the resulting determinant. +Predecessor files and credit lines are unchanged. + +Canonical base is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority +revision 8. The selected-baseline binding control passed. TASK.json marks +the formal-interface card as changed to this algebraic certificate side +result; no caller-bound formalization is asserted. The +[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214425) +records the domain and method. + +Live open/account PRs, active Discussions, recent handoffs, local +reservations, canonical-main README terms and merged topic searches were +checked. The overlap cache covered 416 open PRs and 5,309 Discussion +records at 10:01-10:02 UTC on October 27. Sparse local coverage was only +209 of 7,845 HEAD note paths; separate main README searches supplement it. +No open PR on this sunflower inertia quantity appeared. These bounded +searches do not cover unpublished work or establish literature priority. + +## Open next questions + +1. Can three maximal sets with different nonempty pairwise intersections + admit a sharp integer certificate? Start with facets {1,2}, {2,3} and + {1,3}. Cross-facet pairs may now intersect, so freely prescribing all + Schur-cancelling entries may violate the support restriction. This is + the first obstruction to extending the present sunflower proof. +2. Can a smaller weight alphabet give a uniform sharp certificate for + arbitrary sunflowers? The three-two-element-petal control has a sharp + alternative determinant 5. Start by classifying its allowed cross + weights. Exact cancellation and minimum entry size are different + objectives; no general minimum-weight claim is made here. diff --git a/research/sunflower-downset-inertia/SOURCES.json b/research/sunflower-downset-inertia/SOURCES.json new file mode 100644 index 0000000000..b17bb7f3ce --- /dev/null +++ b/research/sunflower-downset-inertia/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/two-facet-downset-inertia/README.md", + "usage": "provenance", + "git_blob": "1a447b60814df51d32a2c63ea52848f9bfc91243", + "sha256": "9c047eafb8dfcb621e795af8bcbb8f7a9971856be5a0fa5eefccd0da997bb983" + }, + { + "path": "research/pure-math-atlas-400/volumes/03-combinatorics.md", + "usage": "provenance", + "git_blob": "63ecb48e31e8f15c06c6c9813cfb8092870605d8", + "sha256": "b80927e2a5d68e22d3c0687a9ec8267a11b5a1c4a68b06c3f80b8164c2c66b2c" + } + ] +} diff --git a/research/sunflower-downset-inertia/TASK.json b/research/sunflower-downset-inertia/TASK.json new file mode 100644 index 0000000000..02b4074ace --- /dev/null +++ b/research/sunflower-downset-inertia/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove sharp nonnegative integer inertia certificates and exact determinants for every downset generated by three or more sunflower facets.", + "scope_change_reason": "The formal-interface card asks for a selected-caller formalization. This is an original algebraic side result on atlas C070 and the explicit three-disjoint-facet question of merged PR5247, with no supplier or proof-kernel claim.", + "bottleneck_link": "Algebraic certificate side result: enlarges the explicitly certified class in the repository mathematical atlas. No selected supplier cost or kappa improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified sunflower construction; package it and leave general overlapping facets and smaller weight alphabets open.", + "outcome": "completed", + "evidence": "README.md universal simultaneous Schur proof; verify.py exact enumeration of 50 sunflower tuples, 23333 supported-matrix entries, 785 leaf Schur entries and 13 named controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can three maximal sets with distinct nonempty pairwise intersections admit a sharp integer inertia certificate?", + "why_it_matters": "Would move beyond sunflower facets toward the general spectral conjecture.", + "first_step": "Study facets {1,2}, {2,3} and {1,3}, imposing every intersecting-pair zero before choosing Schur cross entries.", + "blocked_by": "Arbitrary cross-block prescriptions can violate disjointness support once the exclusive petals overlap." + }, + { + "question": "Can a smaller weight alphabet yield a sharp certificate for arbitrary sunflowers?", + "why_it_matters": "The new cancellation construction attains optimal inertia but does not optimize entry magnitudes.", + "first_step": "Classify allowed cross weights in the three-disjoint-two-element-facet fixture, whose pairwise-weight control has determinant 5.", + "blocked_by": "Sharp inertia alone does not require the exact Schur cancellation used for the determinant formula." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214425", + "upstream_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at": "2026-10-27T10:09:34.962044+00:00", + "reservation": "formal-interface-lemma-sunflower-downset-sharp-inertia.lock", + "overlap_limits": "416 open PRs and 5309 Discussion records, sparse local inventory 209 of 7845 HEAD notes; targeted main README and merged PR searches supplement sparse coverage." + } +} diff --git a/research/sunflower-downset-inertia/VERIFY.json b/research/sunflower-downset-inertia/VERIFY.json new file mode 100644 index 0000000000..0f90383628 --- /dev/null +++ b/research/sunflower-downset-inertia/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 50 new sunflower tuples through seven ground elements; literal support/stars, exact rational inertia/determinants, zeta congruences and 785 simultaneous Schur entries; 13 named controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical exact checks under optimization; explicit exception contracts remain enabled." + } + ] +} diff --git a/research/sunflower-downset-inertia/verify.py b/research/sunflower-downset-inertia/verify.py new file mode 100644 index 0000000000..3ca65c2fa0 --- /dev/null +++ b/research/sunflower-downset-inertia/verify.py @@ -0,0 +1,278 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the sunflower inertia construction. + +Produced by Nick Petalas. Apache-2.0. +The all-size theorem is the written proof in README.md. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations_with_replacement +import json +from pathlib import Path +import platform + + +MAX_GROUND = 7 +MAX_ORDER = 64 +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def labels_and_ground(sizes, core): + require(isinstance(core, int) and 0 <= core <= MAX_GROUND, "invalid core") + require(3 <= len(sizes) <= MAX_GROUND, "at least three petals required") + require(all(isinstance(a, int) and a >= 1 for a in sizes), "invalid petal") + require(tuple(sorted(sizes, reverse=True)) == sizes, "petals must be sorted") + require(sum(sizes) + core <= MAX_GROUND, "ground capacity exceeded") + base = [(0, s) for s in range(1 << sizes[0])] + for i, a in enumerate(sizes[1:], 1): + base.extend((i, s) for s in range(1, 1 << a)) + offsets = [core + sum(sizes[:i]) for i in range(len(sizes))] + labels = [(r, i, s) for r in range(1 << core) for i, s in base] + ground = [r | (s << offsets[i]) for r, i, s in labels] + require(len(labels) <= MAX_ORDER, "matrix capacity exceeded") + require(len(set(ground)) == len(ground), "ground labels must be distinct") + return labels, ground + + +def entry(x, y, leaf_mode="cancel", coefficient=2): + r, i, s = x + t, j, u = y + if r & t: + return 0 + if i == j: + return int(s & u == 0) + k = (s & u).bit_count() + even = 0 if k == 0 else (1 << (k - 1)) - 1 + if i == 0 or j == 0: + return 1 + coefficient * even + if leaf_mode == "cancel": + return 1 + coefficient**2 * even + if leaf_mode == "pairwise": + return 1 + coefficient * even + require(leaf_mode == "unweighted", "unknown leaf mode") + return 1 + + +def literal_matrix(labels, leaf_mode="cancel", coefficient=2): + return [[entry(x, y, leaf_mode, coefficient) for y in labels] for x in labels] + + +def transpose(matrix): + return [list(row) for row in zip(*matrix, strict=True)] + + +def multiply(left, right): + require(len(left[0]) == len(right), "matrix product shape mismatch") + require(max(len(left), len(right), len(right[0])) <= MAX_ORDER, "product capacity") + out = [[0] * len(right[0]) for _ in left] + for i, row in enumerate(left): + for k, value in enumerate(row): + if value: + for j, other in enumerate(right[k]): + out[i][j] += value * other + return out + + +def permute_first(matrix, position): + matrix[0], matrix[position] = matrix[position], matrix[0] + for row in matrix: + row[0], row[position] = row[position], row[0] + + +def inertia_determinant(matrix): + """Symmetric elimination, including zero-diagonal 2-by-2 pivots.""" + n = len(matrix) + require(1 <= n <= MAX_ORDER, "invalid matrix order") + require(all(len(row) == n for row in matrix), "matrix must be square") + require(matrix == transpose(matrix), "matrix must be symmetric") + work = [[Fraction(x) for x in row] for row in matrix] + positive = negative = zero = 0 + determinant = Fraction(1) + for _ in range(n): + if not work: + break + diagonal = next((i for i in range(len(work)) if work[i][i]), None) + if diagonal is not None: + permute_first(work, diagonal) + pivot = work[0][0] + positive += pivot > 0 + negative += pivot < 0 + determinant *= pivot + work = [[work[i][j] - work[i][0] * work[0][j] / pivot + for j in range(1, len(work))] for i in range(1, len(work))] + continue + pair = next(((i, j) for i in range(len(work)) + for j in range(i + 1, len(work)) if work[i][j]), None) + if pair is None: + zero += len(work) + determinant = Fraction(0) + work = [] + break + i, j = pair + permute_first(work, i) + # j>i, so the first swap leaves the second pivot index j unchanged. + work[1], work[j] = work[j], work[1] + for row in work: + row[1], row[j] = row[j], row[1] + pivot = work[0][1] + positive += 1 + negative += 1 + determinant *= -pivot**2 + work = [[work[i][j] - (work[i][0] * work[1][j] + + work[i][1] * work[0][j]) / pivot + for j in range(2, len(work))] for i in range(2, len(work))] + require(not work and positive + negative + zero == n, "elimination incomplete") + return (positive, negative, zero), determinant + + +def expected(sizes, core): + base_order = 1 + sum((1 << a) - 1 for a in sizes) + n = (1 << core) * base_order + star = n // 2 if core else 1 << (sizes[0] - 1) + exponent = (1 << core) * sum((1 << (a - 1)) - 1 for a in sizes[1:]) + return (star, n - star, 0), (-1)**(n - star) * 3**exponent + + +def transformed_blocks(sizes): + """Build B independently in the zeta basis, before Schur elimination.""" + labels, _ = labels_and_ground(sizes, 0) + n = len(labels) + zeta = [[int(i == j and t & s == t) + for _, j, t in labels] for _, i, s in labels] + reduced = [[0] * n for _ in range(n)] + for x, (_, i, s) in enumerate(labels): + for y, (_, j, t) in enumerate(labels): + if i == j == 0: + reduced[x][y] = (-1)**s.bit_count() if s == t else 0 + elif i == j: + reduced[x][y] = ((-1)**s.bit_count() if s == t else 0) + reduced[x][y] += (-1)**(s.bit_count() + t.bit_count()) + elif i == 0: + reduced[x][y] = ((-1)**(t.bit_count() + 1) if s == 0 else 0) + reduced[x][y] += 2 * int(s == t and t.bit_count() % 2 == 0) + elif j == 0: + reduced[x][y] = ((-1)**(s.bit_count() + 1) if t == 0 else 0) + reduced[x][y] += 2 * int(s == t and s.bit_count() % 2 == 0) + else: + reduced[x][y] = (-1)**(s.bit_count() + t.bit_count()) + reduced[x][y] += 4 * int(s == t and s.bit_count() % 2 == 0) + return zeta, reduced + + +def check_schur(sizes, reduced): + a = sizes[0] + cut = 1 << a + labels, _ = labels_and_ground(sizes, 0) + count = 0 + for i in range(cut, len(reduced)): + for j in range(cut, len(reduced)): + correction = sum(reduced[i][k] * (-1)**k.bit_count() * reduced[k][j] + for k in range(cut)) + target = (-1 if labels[i][2].bit_count() % 2 else -3) if i == j else 0 + require(reduced[i][j] - correction == target, "Schur cancellation") + count += 1 + return count + + +def check_case(sizes, core): + labels, ground = labels_and_ground(sizes, core) + matrix = literal_matrix(labels) + support = 0 + for i, x in enumerate(ground): + for j, y in enumerate(ground): + require(type(matrix[i][j]) is int and matrix[i][j] >= 0, "integer positivity") + require(not (x & y) or matrix[i][j] == 0, "disjointness support") + support += 1 + stars = [sum(bool(mask & (1 << bit)) for mask in ground) + for bit in range(sum(sizes) + core)] + wanted, determinant = expected(sizes, core) + require(max(stars) == wanted[0], "literal largest star") + actual, det = inertia_determinant(matrix) + require((actual, det) == (wanted, determinant), "literal inertia or determinant") + zeta, reduced = transformed_blocks(sizes) + base_labels, _ = labels_and_ground(sizes, 0) + base = literal_matrix(base_labels) + require(multiply(multiply(zeta, reduced), transpose(zeta)) == base, "zeta congruence") + schur = check_schur(sizes, reduced) + return {"petals": list(sizes), "core": core, "order": len(labels), + "inertia": list(actual), "determinant": str(det), + "support_entries": support, "schur_entries": schur} + + +def rejected(call, message): + try: + call() + except ValueError: + return + raise ValueError("control accepted: " + message) + + +def controls(): + labels, _ = labels_and_ground((2, 2, 2), 0) + target = ((2, 8, 0), Fraction(9)) + require(inertia_determinant(literal_matrix(labels)) == target, "first new fixture") + passed = ["first_new_fixture"] + failures = {} + for mode in ("pairwise", "unweighted"): + result = inertia_determinant(literal_matrix(labels, mode)) + require(result != target, "missing cancellation must change the certificate") + failures[mode] = {"inertia": list(result[0]), "determinant": str(result[1])} + passed.append(mode) + weak = inertia_determinant(literal_matrix(labels, coefficient=1)) + require(weak[0][2] > 0, "weak coupling must leave null directions") + failures["weak_coupling"] = {"inertia": list(weak[0]), "determinant": str(weak[1])} + passed.append("weak_coupling") + require(inertia_determinant([[0, 2], [2, 0]]) == ((1, 1, 0), -4), "2x2 pivot") + passed.append("zero_diagonal_pivot") + require(inertia_determinant([[0, 0], [0, 0]]) == ((0, 0, 2), 0), "zeros count") + passed.append("zero_eigenvalues") + rejected(lambda: inertia_determinant([[1, 2], [0, 1]]), "asymmetry") + passed.append("asymmetry") + rejected(lambda: labels_and_ground((2, 2), 0), "previous two-facet domain") + passed.append("previous_domain_excluded") + rejected(lambda: labels_and_ground((1, 2, 1), 0), "unsorted petals") + passed.append("unsorted_petals") + rejected(lambda: labels_and_ground((2, 1, 0), 0), "empty petal") + passed.append("empty_petal") + rejected(lambda: labels_and_ground((3, 3, 2), 0), "capacity") + passed.append("ground_capacity") + rejected(lambda: labels_and_ground((1, 1, 1), -1), "negative core") + passed.append("negative_core") + require(expected((2, 2, 2), 0)[0][0] < 4, "sum of petal stars is not largest star") + passed.append("largest_star_not_star_sum") + return {"count": len(passed), "passed": passed, "distinguishing_fixtures": failures} + + +def parameter_cases(): + cases = [] + for petals in range(3, MAX_GROUND + 1): + for ascending in combinations_with_replacement(range(1, MAX_GROUND + 1), petals): + sizes = tuple(reversed(ascending)) + total = sum(sizes) + if total <= MAX_GROUND: + for core in range(MAX_GROUND - total + 1): + cases.append((sizes, core)) + require(len(cases) <= 256, "parameter inventory capacity") + return cases + + +def main(): + cases = [check_case(sizes, core) for sizes, core in parameter_cases()] + result = {"status": "PASS_SUNFLOWER_DOWNSET_INERTIA", + "claim_type": "scoped proof with exact finite corroboration", + "no_new_kappa": True, "python": platform.python_version(), + "cases": cases, "case_count": len(cases), "controls": controls()} + folder = Path(__file__).resolve().parent + result["sha256"] = {name: sha256((folder / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()