Prove least denominator 12,480 for the A1 zero spectral projector (no κ)

research/a1-zero-projector-denominator/PROOF.md

@@ -0,0 +1,89 @@
+# Proof for the pinned block
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## The finite object
+
+Let `M` be unpaidmoon's pinned 216-by-216 integer matrix for `B=4 A_1` in
+`research/a1-joint-216-charpoly/evidence/matrix.json`. Let `v_i` be the pinned
+signed-orbit basis vectors from that package. Their supports are disjoint and
+their nonzero entries are signs. Consequently the Gram matrix is the positive
+diagonal matrix `D`, with `D_ii = |support(v_i)|`.
+
+The predecessor supplies this historical block and its interpretation. The
+following argument uses the literal pinned matrix; it does not rederive the
+block, the characteristic polynomial or any predecessor kernel certificate.
+
+## A completeness certificate
+
+Put `d=12480`, and take the integer matrix `Q` in PROJECTOR.json. Exact integer
+multiplication verifies `Q^2=dQ` and `MQ=QM=0`. Entrywise comparison verifies
+`DM=M^T D` and `DQ=Q^T D`. Gaussian elimination modulo the prime 1000003 gives
+
+```text
+det(M+Q) = 905182 (mod 1000003).
+```
+
+A zero integer determinant has zero residue in every modulus. Thus `M+Q` is
+invertible over the rationals. These finite identities are the certificate;
+the verifier checks every matrix entry and the modular elimination directly.
+
+Let `P=Q/d`. Idempotence gives `P^2=P`, and `MQ=0` gives
+`image(P) subset kernel(M)`. If `x` lies in `kernel(M)`, then
+
+```text
+(M+Q)(d x-Qx) = d Mx - MQx + d Qx - Q^2 x = 0.
+```
+
+Invertibility implies `Qx=dx`, so `Px=x`. Hence `image(P)=kernel(M)`.
+The weighted self-adjointness of `Q` gives `DP=P^T D`, so this is the unique
+orthogonal projector onto that kernel in the positive inner product defined
+by `D`. Also `PM=0`; since `M` is self-adjoint, its image is the orthogonal
+complement of its kernel. Thus `P` is precisely the zero spectral projector,
+and it commutes with `M` and `A_1`.
+
+The exact trace is 24, hence this idempotent has rank 24. This is a consequence
+of the new projector certificate, not a substituted modular-rank argument.
+The proof does not require the predecessor characteristic polynomial or its
+algebraic-multiplicity count.
+
+One way to discover the matrix is to choose a rational kernel basis `K` and
+form `K (K^T D K)^(-1) K^T D`. The committed certificate is independent of
+that construction procedure: its identities alone prove the result.
+
+## The denominator is sharp
+
+Since `Q` is integral, `dP` is integral. Exact reduction of four specified
+entries gives
+
+```text
+P[10,60] = 9/4160,   P[4,4] = 47/156,
+P[6,6] = 71/260,    P[0,0] = 5/416.
+```
+
+Each fraction is reduced. Any positive integer `e` for which `eP` is integral
+must be divisible by all four denominators. Their least common multiple is
+12480. Therefore the least such `e` is exactly
+`12480 = 2^6 * 3 * 5 * 13`. Independently, the verifier checks that the gcd of
+`d` and all entries of `Q` is one, which proves the same minimality by Bezout.
+No single entry is asserted to have denominator 12480.
+
+## Consequence for exact dyadic operations
+
+A finite linear straight-line program with dyadic rational scalar coefficients
+and dyadic constants has a dyadic rational linear part. This follows by
+induction on additions, subtractions and scalar multiplications. Adding clean
+zero coordinates, or arbitrary dirty coordinates that must be restored, does
+not change this fact about the induced input-output block.
+
+The displayed entries of `P` have unavoidable odd denominator factors 3, 5
+and 13. Therefore such a program cannot implement `P` on the pinned input and
+output coordinates. The same conclusion holds for a polynomial in `A_1` with
+dyadic coefficients, since `A_1=M/4` is a dyadic matrix.
+
+This is a fixed-basis exact obstruction. It is invariant under input and
+output changes of basis whose matrices and inverses are dyadic: if an adapted
+matrix were dyadic, converting back would make `P` dyadic. The statement does
+not grant a free rational basis conversion. It makes no claim about other
+invariant projections, nonlinear operations, approximation, paid odd division,
+physical routing, recursive costs or a multiplication theorem.

research/a1-zero-projector-denominator/README.md

@@ -0,0 +1,114 @@
+# The zero spectral projector needs denominator 12,480
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: exact finite certificate with a scoped arithmetic obstruction.
+For the historical `A_1` joint `(+1,+1)` block pinned by unpaidmoon's
+[PR #6964](https://github.com/CrocSwap/integer-mult-bounds/pull/6964), the
+zero-eigenspace projector has least integral denominator
+
+```text
+P = Q / 12480,    12480 = 2^6 * 3 * 5 * 13.
+```
+
+[PROJECTOR.json](PROJECTOR.json) supplies every entry of the integer matrix
+`Q`. Four reduced entries force the denominator, with indices starting at zero:
+
+```text
+P[10,60] = 9/4160
+P[4,4]   = 47/156
+P[6,6]   = 71/260
+P[0,0]   = 5/416
+lcm(4160,156,260,416) = 12480.
+```
+
+Consequently this particular exact spectral filter cannot be a linear program
+using only dyadic rational coefficients in the pinned basis. In particular,
+no polynomial in `A_1` with dyadic coefficients equals `P`. Its matrix has
+entries outside `Z[1/2]`. This does not exclude another invariant filter,
+a rational implementation with paid odd division, or an approximate filter.
+
+No kappa improvement, supplier admission or selected-frontier change is claimed.
+The selected record at the package base is #7000, with conditional
+`kappa = 363005817/100000000000`. This result concerns a historical centre block.
+
+## Exact evidence
+
+The proof is in [PROOF.md](PROOF.md). The verifier authenticates the predecessor
+matrix and orbit basis, then checks
+
+```text
+M = 4 A_1
+Q^2 = 12480 Q
+M Q = Q M = 0
+D M = M^T D,   D Q = Q^T D
+ det(M+Q) mod 1000003 = 905182 != 0.
+```
+
+`D` is the positive diagonal Gram matrix of the disjoint signed-orbit basis.
+Nonsingularity of `M+Q` proves that the image of `P` is the whole kernel, rather
+than an unspecified part. The identities and weighted symmetry uniquely
+identify its orthogonal projector. Its rank is 24 and `Q` has 4,608 nonzero
+entries, both enumerated by the checker. The characteristic polynomial and
+predecessor nullity packages are not replayed.
+
+The verifier accepts a weighted, nonsymmetric two-dimensional fixture and
+rejects four false certificates: one altered numerator entry, the source
+shifted by the identity, a doubled unreduced fraction, and the zero projector.
+The zero projector satisfies the annihilation and idempotence identities but
+fails completeness, so the determinant check supplies necessary coverage.
+All checks use explicit exceptions and also run under optimized Python.
+
+The full source pins, scope and replay contract are in [SOURCES.json](SOURCES.json),
+[TASK.json](TASK.json) and [VERIFY.json](VERIFY.json). Source-file hashes bind the
+scientific inputs; the package runner also checks metadata and source pins.
+The separate publication preflight checks declared source-history availability.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a1-zero-projector-denominator/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B -O research/a1-zero-projector-denominator/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a1-zero-projector-denominator
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a1-zero-projector-denominator --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. The direct marker is
+`PASS_A1_ZERO_PROJECTOR_DENOMINATOR`. The registered marker is
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Local environment is CPython 3.12.15 on
+macOS arm64, recorded in TASK.json. Lean, Docker, the degree-216 and degree-881
+spectral replays, the selected cold replay and a physical implementation are
+outside this package's checks.
+
+The checker writes nothing. Matrix dimension is at most 216, each JSON input
+is bounded by one MiB, and orbit supports have at most 16 entries among 4,096
+addresses. Python allocates during arithmetic; the finite capacities bound live
+storage instead of claiming allocation-free execution. Functions are below
+60 lines and no recursion or external dependencies are used.
+
+## Related work and credit
+
+unpaidmoon #6964 supplies the exact matrix, the signed-orbit basis and the
+characteristic polynomial. The new result is the explicit projector, its sharp
+arithmetic denominator and the resulting dyadic obstruction. The new certificate
+uses that matrix as its mathematical input and does not independently establish
+its derivation from the historical query.
+
+Related open work #7018, #7064 and #7066 computes kernel dimensions, while #7008
+and #7065 split the same block by normalizer symmetries. They are distinct from
+this projector-denominator question. Their results are credited without replay.
+JoyboyBrian posed the earlier decomposition handoff. Retain the sign-stabilizer
+construction, Ali Romman's #4958/#4720 query and Bell-action work, Krzysztof
+Wojt's #5168 one-slot polynomial, Nick Petalas's #5120 lower bound, and #1719's
+doubled representation. Those results are background rather than new claims here.
+
+## Open next questions
+
+- Price an exact physical filter with odd division and full output restoration.
+  First choose a legal division contract and factor `Q/12480`; native delivery
+  and the complete paid/target invoice are unresolved.
+- Identify whether a different invariant filter needed by a stated centre
+  consumer can be dyadic. Begin with that consumer identity; this package
+  supplies no reason to substitute an arbitrary different projector.

research/a1-zero-projector-denominator/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/a1-joint-216-charpoly/PROOF.md",
+      "usage": "input",
+      "git_blob": "5ec978d4df7a49ec25f020e32fdc96eddf387d51",
+      "sha256": "2b5ba7a83f74188b7dfc0d114747f14be05923418a86b3cfc1540c471a6f988a"
+    },
+    {
+      "path": "research/a1-joint-216-charpoly/README.md",
+      "usage": "input",
+      "git_blob": "7e6de8a547e5080f77f623d9772467fe2a439ae3",
+      "sha256": "d8737c1587a214d8665716f64fcbf54573a4283382f5f2f3ab7e31edd3fd6f66"
+    },
+    {
+      "path": "research/a1-joint-216-charpoly/evidence/basis.json",
+      "usage": "input",
+      "git_blob": "5e524a41ed1c65017b7d902b5445aedd2eb606ff",
+      "sha256": "e198cd71f4100d2629ecc25fb40b135a8c18c7756be8bc80bf24d7b349af418a"
+    },
+    {
+      "path": "research/a1-joint-216-charpoly/evidence/matrix.json",
+      "usage": "input",
+      "git_blob": "23bccaef6f24e6e644bdba81f58e9217787ab16c",
+      "sha256": "44f40ad5a12daf7c8493b42e1e9ddc4ef338b317ee5fdfc6de1b413642ca97aa"
+    }
+  ]
+}

research/a1-zero-projector-denominator/TASK.json

@@ -0,0 +1,125 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Construct the exact zero-eigenspace projector of the pinned historical A_1 joint (+1,+1) 216-dimensional block, determine its least integral denominator, and exclude its realization by dyadic-coefficient linear programs in the pinned basis.",
+  "scope_change_reason": "The decoder/coframe card is narrowed to a new arithmetic question about an exact spectral filter on the historical centre block. PR6964 supplies the matrix and orbit basis but does not construct this projector. This is an algebraic side result rather than a changed current supplier.",
+  "bottleneck_link": "Exact spectral filtering is a possible centre-decoder operation. The odd primes in this projector denominator obstruct a dyadic-only realization of this particular filter. The historical block and fixed basis do not imply a limit for other decoders, new helper inventories or the selected #7000 supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact projector and matching least-denominator certificate. Do not extend to other eigenvalues, joint sign spaces, or a physical supplier.",
+  "outcome": "completed",
+  "evidence": "PROJECTOR.json gives Q and d=12480. verify.py checks Q^2=dQ, MQ=QM=0, positive weighted self-adjointness, and nonsingularity of M+Q modulo 1000003. Four reduced entries have denominator lcm 12480. No predecessor scientific replay is run.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the least odd denominator cost of a physical implementation of this exact filter?",
+      "why_it_matters": "The matrix obstruction requires odd division but does not price it or decide whether a complete decoder can afford it.",
+      "first_step": "Choose one legal odd-division and output-restoration contract, then price a factored realization of Q/12480.",
+      "blocked_by": "No physical caller or complete paid/target invoice is supplied here."
+    },
+    {
+      "question": "Can another exact invariant filter useful to the historical centre decoder be dyadic?",
+      "why_it_matters": "The exclusion concerns the zero spectral projector alone, so changing the filtered invariant subspace might avoid it.",
+      "first_step": "Specify the required consumer identity before testing a different polynomial or invariant decomposition.",
+      "blocked_by": "The consumer must justify which other filter actually replaces a required operation."
+    }
+  ],
+  "claim_type": "exact finite certificate with a scoped arithmetic obstruction",
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571856",
+  "predecessor": {
+    "pr": 6964,
+    "author": "unpaidmoon",
+    "usage": "pinned matrix, signed-orbit basis and the spectral-filter motivation; predecessor polynomial and nullity are not replay targets"
+  },
+  "overlap": {
+    "checked_at": "2026-11-12T18:21:46Z",
+    "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57",
+    "open_pr_records": 760,
+    "discussion_records": 7341,
+    "remote_pagination_complete": true,
+    "local_notes_searched": 225,
+    "head_note_paths": 10178,
+    "limits": "Sparse note coverage is incomplete. Separate Git-tree README searches cover denominator 12480/12,480, spectral/kernel projector and zero spectral filter terms. Merged PR searches cover the number, object and broader projector terminology. No arbitrary diffs or unpublished work are covered.",
+    "nearest_open_prs": [
+      7018,
+      7064,
+      7066,
+      7008,
+      7022,
+      7023,
+      7059,
+      7061,
+      7065,
+      7019,
+      7071,
+      7009,
+      7036,
+      7057,
+      7082,
+      7020,
+      7068,
+      7069,
+      7172
+    ],
+    "novelty": "No matching projector denominator was found. Source PR6964 supplies no other recent contribution from this account in the queried 200-PR account history. The open nullity packages are cited without using their scientific replay as the deliverable."
+  }
+}