Certify a filled three-dimensional mode shadow with 103,333 points (no κ)

research/mode-rank-five-shadow/PROOF.md

@@ -0,0 +1,172 @@
+# One rank-five flat has a filled three-dimensional mode shadow
+
+The proof and finite certificate were produced by Nick Petalas. New work is
+Apache-2.0. This is an exact finite result for one fixed mode matrix.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Statement
+
+Let the rows of the 112-by-8 integer mode matrix in Dillon Amburgey's
+`research/coded-native-caller/NORMALIZERS.json` be `m_0,...,m_111`, indexed
+from zero. Put `L = span_Z {m_i}` and `Z = sum_i [0,1] m_i`.
+Let `F = span_R {m_0,...,m_4}`. These five rows are
+
+```text
+1 1 1 1 0 0 0 0
+1 1 0 0 1 1 0 0
+1 0 1 0 1 0 1 0
+1 0 0 1 0 1 1 0
+1 0 0 1 1 0 0 1
+```
+
+Define the rational quotient map `pi(x) = B x / 2`, with
+
+```text
+B = [-2 0 1  1  1 1 0 0]
+    [-2 1 0  1  1 0 1 0]
+    [ 1 0 0 -1 -1 0 0 1].
+```
+
+**Finite theorem.** `ker(pi) = F`, `pi(L) = Z^3`, and
+
+```text
+pi(Z) intersect Z^3 = { sum_i epsilon_i pi(m_i) : epsilon_i in {0,1} }.
+```
+
+The left-hand side has exactly **103,333** points. Exactly **94,599** are
+strictly interior, and **8,734** are on the boundary. Thus this particular
+three-dimensional shadow has no lattice hole, even on its boundary.
+
+## Quotient and row flat
+
+Exact rational row reduction gives rank five for the five displayed rows
+and rank three for B. Each displayed row is annihilated by B, so F is exactly
+the kernel. Of the 112 rows, exactly 15 are annihilated. Their rank is five.
+They form the closed row flat with span F. A generic functional in F's
+three-dimensional annihilator exposes a face parallel to F, so this is a
+shadow along a codimension-three face in the sense of apoursh's #6829.
+
+The verifier computes every `B m_i`, checks divisibility by two, and sets
+`q_i = pi(m_i)`. Some q_i are the signed coordinate unit vectors. Hence
+`span_Z {q_i} = Z^3`, without any lattice saturation or index assumption.
+
+For enumeration, replace each q_i whose first nonzero coordinate is negative
+by `p_i = -q_i`; leave the others unchanged. Let t be the sum of the q_i
+that were replaced. Then both the zonotope and its subset sums translate
+by the same integer vector:
+
+```text
+sum_i [0,1] q_i = t + sum_i [0,1] p_i,
+{sum_i epsilon_i q_i} = t + {sum_i epsilon_i p_i}.
+```
+
+Consequently filling can be checked for the p_i. This reorientation leaves
+15 zero generators. The 14 distinct nonzero generators and multiplicities
+are emitted in the computed receipt. The exact coordinate bounding box is
+
+```text
+[0,86] x [-1,85] x [-49,5],
+```
+
+which contains 416,295 integer points.
+
+## Complete finite certificate
+
+The verifier uses two different representations of subset sums. First,
+encode a point in that box as
+
+```text
+index(x,y,z) = x + 87(y+1) + 87^2(z+49).
+```
+
+Starting with the bit for the origin, update `S <- S union (S+p_i)` for
+each of the 112 generators. A signed integer bit shift implements this
+update. At every prefix, each genuine subset sum lies in the global box,
+because the sum of coordinatewise negative contributions is a lower bound
+and the sum of positive contributions is an upper bound. Thus no encoded
+shift crosses a coordinate boundary, wraps, or discards a genuine point.
+The final set has 103,333 bits. A separate tuple-set recurrence computes
+all subset sums and agrees with every bit, without integer encoding.
+
+The closed three-dimensional zonotope has a complete facet description
+obtained as follows. For each pair of distinct generator directions, take
+their cross product. Discard zero products, divide by the gcd, and identify
+opposite normals. There are exactly 25 resulting normal pairs. For each
+primitive normal n, the exact support inequalities are
+
+```text
+sum_i min(0,n.p_i) <= n.x <= sum_i max(0,n.p_i).
+```
+
+These inequalities define the zonotope. Indeed, each facet's parallel
+generators span a two-dimensional plane, so two independent generators
+produce its normal in the cross-product list. Conversely every listed
+inequality is valid. A bounded full-dimensional polytope is the
+intersection of its facet half-spaces. No floating-point hull computation
+or predecessor facet census is used here.
+
+For each of the 87-by-55 possible pairs `(y,z)`, intersect these 25
+inequalities to obtain the exact integer x interval. The closed intervals
+contain 103,333 points, each present in the subset bitset. Replacing each
+primitive integral support inequality by its strict version gives 94,599
+interior points, also all present. A separate pointwise scan tests all
+416,295 points against all 25 inequalities and compares every closed
+membership decision with the tuple set. It independently reproduces both
+counts. Their difference is the boundary count.
+
+The receipt is computed at execution time and binds the six package files
+and the subset bitset by SHA256. It is not a handwritten or committed log.
+
+## Controls and implementation bounds
+
+Removing one actually reached interior point creates exactly one detected
+hole in both the closed and interior scans. A small full-rank integer
+zonotope with generators `(1,-3,0),(1,-2,0),(1,0,0),(0,0,1),(0,0,1)` has
+holes; the verifier checks their exact counts rather than assuming every
+zonotope fills. An independent tuple encoding of that example checks signed
+shifts. These are five explicit control predicates, counted in the receipt.
+
+The verifier is nonrecursive and read-only. The source boundary checks eight
+columns, 112 rows, entries in {-1,0,1}, and its pinned SHA256. Geometry accepts
+at most 112 three-coordinate generators, coordinates bounded by eight, and
+a box of at most 500,000 points. Every enumeration is bounded by these
+finite dimensions. No function exceeds 60 physical lines.
+
+Power-of-ten rule 3 deviation applies to Python integers, Fractions, JSON,
+sets and tuples: CPython allocates managed objects during the calculation.
+The scope is this finite verifier. The enforced box capacity bounds each
+reachable set by 500,000 tuples; at most the existing and one shifted set
+are live during an update. The bitset has at most 500,000 bits. File inputs
+are pinned and bounded. Both normal and optimized warning-strict replay
+exercise the same checks, which use explicit exceptions rather than Python
+assertions. Follow-up if the input family grows is to retain explicit
+capacity bounds or switch the tuple cross-check to fixed packed storage.
+Separate compiler/type analysis is not supplied for this standard-library
+Python research script.
+
+## Scope and predecessors
+
+Armin Pourshafeie / apoursh's #6829 poses the codimension-three question
+and proves filling of every facet and ridge shadow. Those results are cited,
+not rechecked. The new calculation begins in a different quotient and proves
+the displayed one-flat statement only. Dillon Amburgey's #4933 supplies M.
+Nick Petalas's #6312 defines the exact-mode rounding radius, and apoursh's
+#6320 reduces radius one to full eight-dimensional lattice filling; #6333
+gives the retained upper bound three halves. Cross products, zonotope support
+functions, exact elimination and subset-sum dynamic programming are classical.
+
+This does not classify rank-five flats, prove filling for every
+three-dimensional shadow, or settle full eight-dimensional filling or R=1.
+No physical rounder, compiler, precision, tape, ownership, stock, supplier
+admission, new kappa, selected-frontier change or complete multiplication
+theorem follows. All five selected framework assumptions remain.
+
+## Open next questions
+
+- Classify rank-five row flats up to the mode matrix's signed code symmetries.
+  Begin by mapping the 15-row flat above into that catalogue. A complete
+  orbit inventory is not supplied here.
+- Test a different rank-five-flat orbit with the same lattice-index and
+  full-membership checks. Larger quotient boxes may need a different exact
+  representation. Filling every such shadow would still leave higher
+  codimensions and full R=1 open.

research/mode-rank-five-shadow/README.md

@@ -0,0 +1,79 @@
+# A filled three-dimensional mode shadow along one rank-five flat
+
+This contribution was produced by Nick Petalas. New work is Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+**Exact finite certificate with a scoped proof; no new kappa.** For the
+112-by-8 mode matrix of Dillon Amburgey's #4933, the row flat generated by
+rows 0 through 4 has a three-dimensional quotient whose entire closed
+zonotope is lattice-filled. Every one of its **103,333** lattice points is
+a subset sum of the projected modes. Exactly **94,599** are interior and
+**8,734** are boundary points. Row numbering starts at zero.
+
+This supplies one explicit case of Open next question 1 in Armin
+Pourshafeie / apoursh's [#6829](https://github.com/CrocSwap/integer-mult-bounds/pull/6829).
+That package establishes facet and ridge filling and leaves three-dimensional
+shadows open. Its scientific verifier is not replayed here.
+
+[PROOF.md](PROOF.md) gives the quotient map, lattice basis, complete exact
+facet description and finite enumeration argument. The new verifier reads
+the pinned original matrix, checks the flat, computes all subset sums twice,
+and compares them with every lattice point in the quotient zonotope.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/mode-rank-five-shadow/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/mode-rank-five-shadow/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mode-rank-five-shadow
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mode-rank-five-shadow --check-source-history
+```
+
+Substitute another CPython 3.12 path on other machines. Expected markers are
+`PASS_MODE_RANK_FIVE_SHADOW`, `PASS_REGISTERED_RESEARCH_PACKAGE`, and
+`PASS_RESEARCH_COMMIT_BYTES`. A sparse checkout needs this package and
+`research/coded-native-caller/NORMALIZERS.json` materialized before replay.
+
+The verifier enumerates a box of 416,295 integer points, 25 facet-normal
+pairs, and all 103,333 distinct subset sums. Independent bitset and tuple-set
+recurrences agree exactly; independent interval and pointwise scans agree
+on closed and interior membership. Five control predicates detect a removed
+interior subset sum and holes in a small counterexample. Receipts are
+generated from the current file hashes and bitset; no receipt is handwritten.
+
+## Limitations
+
+Only one rank-five row flat is covered. There is no all-orbit census,
+universal three-dimensional filling theorem, or proof of R=1. The current
+rounding-radius interval remains 1 to 3/2. Exact-mode rounding itself is an
+abstract interface. No physical rounder or complete multiplication theorem
+is supplied; kappa, selected frontier and the five assumptions are unchanged.
+Native/caller implementation, ownership, compiler, precision/tape and stock
+costs remain open. No predecessor scientific replay, full selected cold
+replay, Lean, Docker or separate type/lint analysis was run. Hosted CI is
+separate from local finite verification.
+
+The `uniform-transfer-audit` card has explicitly changed scope to this
+analytic-recovery side result. Its actual-caller acceptance gate is unmet.
+The source-binding baseline passed and is only metadata orientation.
+
+## Open next questions
+
+- Locate this 15-row flat in a complete signed-symmetry orbit catalogue of
+  rank-five row flats. A complete catalogue is not part of this certificate.
+- Test another orbit using an exact quotient-lattice basis and full lattice
+  membership scan. Larger quotient boxes may need another representation.
+- Connect any eventual full-dimensional filling result to a physical
+  rounder and its complete caller costs. Shadow filling alone is insufficient.
+
+## Credit
+
+Credit Armin Pourshafeie / apoursh #6829 for the open three-dimensional
+question and facet/ridge results, #6320 for the full-dimensional finite
+reduction, and #6333 for R <= 3/2. Dillon Amburgey #4933 supplies the unchanged
+mode matrix. Nick Petalas #6312 supplies the exact-mode radius definition
+and lower bound. Exact elimination, zonotope support functions and subset-sum
+dynamic programming are classical. The new quotient calculation, finite
+certificate, proof and verifier were produced by Nick Petalas.

research/mode-rank-five-shadow/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/coded-native-caller/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    },
+    {
+      "path": "research/mode-fiber-facet-depth/README.md",
+      "usage": "provenance",
+      "git_blob": "68505da8c65b7423a06df844b19cf0c16addb793",
+      "sha256": "42ff56e9ecee6e256991d58e679d86e9bfde50a20e2cfb64deaf2e2500470b84"
+    },
+    {
+      "path": "research/mode-fiber-facet-depth/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "b0cdd56c3cc16415983e5e9bd6f3ddccf9112b73",
+      "sha256": "ee436e8f10f6170123e686d3b96e96cafda40ffb93380ac7284d6d055ce21742"
+    },
+    {
+      "path": "research/mode-fiber-radius-bounds/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "ba8a3da373a2bc9cf7c499681e2f3bd0145b45a8",
+      "sha256": "9793a4418f5e24f3577c166640906260913ebf7da3011559abdf175be3e6e341"
+    }
+  ]
+}

research/mode-rank-five-shadow/TASK.json

@@ -0,0 +1,94 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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"
+    ],
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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": "Exact lattice filling of the three-dimensional shadow along the rank-five flat generated by mode rows 0 through 4.",
+  "scope_change_reason": "The donated task requests original work; this answers one case of apoursh PR6829 Open next question 1 instead of auditing a predecessor or claiming actual-caller assumption discharge.",
+  "bottleneck_link": "Analytic-recovery side result: removes one possible projected lattice-hole obstruction to exact mode-preserving radius-one rounding. No actual caller or physical rounder follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first exact original one-flat filling certificate or a precise hole/handoff.",
+  "outcome": "completed",
+  "evidence": "Exact quotient lattice and rank-five flat; 103333 closed lattice points, 94599 interior and 8734 boundary, all subset sums. Bitset/tuple and interval/pointwise enumerations agree. Five control predicates.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Classify rank-five row-flat orbits and identify the displayed 15-row flat.",
+      "why_it_matters": "One case does not cover every codimension-three shadow.",
+      "first_step": "Apply the retained signed code symmetries to the closed flat.",
+      "blocked_by": "No complete rank-five orbit inventory is supplied."
+    },
+    {
+      "question": "Does another rank-five-flat orbit have a lattice hole?",
+      "why_it_matters": "A missing projected subset sum could obstruct radius-one rounding.",
+      "first_step": "Compute an exact quotient-lattice basis and scan the complete projected box.",
+      "blocked_by": "Larger quotient boxes may require a different finite representation."
+    }
+  ],
+  "environment": {
+    "python": "3.12.15",
+    "requirements": "standard library only"
+  },
+  "claim_type": "Exact finite certificate with a scoped proof for one fixed row flat."
+}