Price an exact three-term Gram-class design on A_3 (no kappa)

research/gram-class-a3-three-term-design/PROOF.md

@@ -0,0 +1,101 @@
+# Proof note: an exact three-term Gram-class design on A_3
+
+Model, quoted from DreamingOfClouds' `research/p104-duality-ceiling-flag-note`
+(Theorem O, section 2, and the A_2 toy, section 4). Let `V = {x in Q^(n+1) :
+sum_i x_i = 0}` and `Pi = I - J/(n+1)` the orthogonal projector onto V. The A_n
+lines are the pairs `(i,j)`, `i < j`; the line `(i,j)` is orthogonal to `x` iff
+`x_i = x_j`. The even-inner-product mask of the line set is `N = I`, so for
+`u, w in V` the price of a term is
+
+```text
+rho(u,w) = rank_F2 N[S_u, T_w] = |Sep(u) cap Sep(w)|,
+Sep(x) = {(i,j) : x_i != x_j}.
+```
+
+A Gram-class design is a finite family `(u_k, w_k)` in `V x V` with
+`sum_k u_k w_k^T = Pi`; its cost is `sum_k rho(u_k, w_k)`. This package fixes
+n = 3: four coordinates, six lines, `Pi_4 = I - J/4`. Labels are [P] written
+proof, [C] exact computation in `verify.py`.
+
+## 1. The written design [P+C]
+
+Set
+
+```text
+u_1 = (0, 0, 1, -1)      w_1 = (-1/2,  1/2,  1/2, -1/2)
+u_2 = (0, 1, -1, 0)      w_2 = ( 1/2,  1/2, -1/2, -1/2)
+u_3 = (1, -1, 1, -1)     w_3 = ( 3/4, -1/4, -1/4, -1/4)
+```
+
+Every coordinate vector has coordinate sum zero, so `u_k, w_k in V`, and
+`sum_k u_k w_k^T = Pi_4` holds identically over the rationals [C]. The three
+prices are 3, 3 and 2 [C]:
+
+| k | Sep(u_k) | Sep(w_k) | intersection | price |
+|---|---|---|---|---|
+| 1 | 5 pairs | 4 pairs | `(0,2),(0,3),(1,2),(1,3)` | 3 |
+| 2 | 5 pairs | 4 pairs | `(0,2),(0,3),(1,2),(1,3)` | 3 |
+| 3 | 4 pairs | 3 pairs | `(0,1),(0,3)` | 2 |
+
+Total cost 8. (The check recomputes the separations from the vectors; the table
+is descriptive.)
+
+## 2. The natural dual-basis design costs 9 [P+C]
+
+Let `u_k = e_k - e_4` for `k = 1,2,3` and let `w_k` be the dual basis of V
+with respect to the dot product, `w_k = e_k - (1/4) 1`. Then `u_k . w_l =
+delta_kl` and `sum_k u_k w_k^T` is the orthogonal projector of V = col(U), so
+the design is exact [C].
+
+Price: `u_k` has entry 1 at k, -1 at 4 and 0 elsewhere, so `Sep(u_k)` is the
+set of pairs meeting `{k,4}`, of size `2n-1 = 5`. `w_k` has entry `3/4` at k and
+`-1/4` at the other three coordinates, so `Sep(w_k)` is the set of pairs meeting
+`k`, of size `n = 3`. The pairs meeting both `k` and `{4}` are exactly the pairs
+meeting `k`, so `rho(u_k,w_k) = 3` and the total cost is `3 * 3 = 9`. The same
+count gives `n^2` for general n. Hence the written design of section 1 improves
+the dual-basis design inside the same model by one unit.
+
+## 3. Every design has at least three terms [P]
+
+`Pi_4` has rank 3, and each term `u_k w_k^T` has rank at most 1. So a Gram-class
+design needs at least three terms. No lower bound on the cost beyond
+`cost >= number of terms >= 3` is claimed.
+
+## 4. The declared finite family [C]
+
+Take the primitive integer vectors in `[-3,3]^4` with coordinate sum zero and
+positive first nonzero entry, and keep the lexicographically first vector of
+each equality pattern. There are 14 patterns; the list is fixed by the check
+(`candidate_vectors`). Enumerate all ordered triples, solve `Pi_4 = U W^T` for
+`W` exactly (the solution is unique when `U` has full rank), and price the
+result. Of the `14^3 = 2744` triples, 1812 have full-rank `U` and an exact
+solution; every one of the 1812 has cost at least 8, and the written design of
+section 1 is one of the minimisers [C].
+
+Because the family keeps one representative per equality pattern, this is not a
+search over all rational carriers. A design with different carriers in the same
+pattern can have a different price, so the enumeration does not prove that 8 is
+the Gram-class minimum.
+
+## 5. Rejection controls [C]
+
+The check requires that (i) adding 1/2 to one entry of `w_1` destroys the
+projector identity, (ii) replacing `u_1` by the zero vector destroys it, and
+(iii) the three `u_k` of the written design are linearly independent. It also
+requires the dual-basis design to be exact at cost 9 and the A_2 control below
+to be exact at cost 4, so a broken cost or identity check fails loudly.
+
+## 6. A_2 control [C]
+
+`u_1 = (0,1,-1)`, `w_1 = (1,0,-1)`, `u_2 = (1,-2,1)`, `w_2 = (2/3,-1/3,-1/3)`
+give `sum_k u_k w_k^T = Pi_3` with prices 3 and 1, total 4. This reproduces the
+A_2 Gram value reported by the predecessor's section 4; it is a control for this
+package's price code and is not claimed as new.
+
+## Scope
+
+Nothing here is a lower bound over all Gram-class designs, a statement about
+A_n for n >= 4, a kappa change, a physical word, or a supplier admission. The
+exact A_3 minimum remains open. The model, definitions and A_2 value are the
+predecessor's; this package adds the explicit A_3 design, the dual-basis price
+comparison and the bounded enumeration.

research/gram-class-a3-three-term-design/README.md

@@ -0,0 +1,99 @@
+# An exact three-term Gram-class design on the A_3 line system
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+DreamingOfClouds' [P104 duality and Gram-floor note](../../research/p104-duality-ceiling-flag-note/README.md)
+defines a Gram-class price model on line systems and shows at A_2 that the
+naive transfer "Gram price at least the identity-decoder price" is false: the
+Gram value there is 4 (section 4 of [THEOREM.md](../../research/p104-duality-ceiling-flag-note/THEOREM.md)).
+That note states A_4 and every n >= 3 as outside its scope. This package adds
+the next explicit data point.
+
+**Result.** On the A_3 line system (four coordinates, six lines, mask N = I)
+there is an exact three-term Gram-class design
+
+```text
+u_1 = (0, 0, 1, -1)        w_1 = (-1/2,  1/2,  1/2, -1/2)
+u_2 = (0, 1, -1, 0)        w_2 = ( 1/2,  1/2, -1/2, -1/2)
+u_3 = (1, -1, 1, -1)       w_3 = ( 3/4, -1/4, -1/4, -1/4)
+```
+
+with `sum_k u_k w_k^T = Pi_4 = I - J/4` over the rationals and term prices
+**3, 3, 2**, for a total price **8**. The natural dual-basis design of the same
+shape, `u_k = e_k - e_4` with `w_k = e_k - (1/4) 1`, is exact and costs
+**3 + 3 + 3 = 9**, so the written design is strictly cheaper inside the same
+model.
+
+The declared finite family of three-term designs whose carriers are the 14
+canonical representatives of the equality patterns on four coordinates (1812
+full-rank triples) has minimum price **8**, attained by the written design. This
+is a bounded enumeration, not a lower bound over all designs.
+
+Claim type: exact finite certificate (a written design with exact rational
+identity and prices) plus a bounded exhaustive enumeration of a declared finite
+family. **Not** claimed: the exact minimum over all Gram-class designs, any
+lower bound beyond the trivial three terms forced by rank, a new kappa, or a
+supplier admission.
+
+## Why the price rule is the predecessor's
+
+For the A_n line system the even-inner-product mask is `N = I`, so the F2
+mask-rank price of a term collapses to the number of lines on which both
+carriers are non-constant. See section 4 of the predecessor's `THEOREM.md`,
+which fixes this rule and the A_2 example; this package uses that rule only and
+does not re-check the predecessor's proofs. The A_2 value 4 is reproduced here
+as a control, not claimed as new.
+
+## Reproduction
+
+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/gram-class-a3-three-term-design/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/gram-class-a3-three-term-design/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gram-class-a3-three-term-design
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gram-class-a3-three-term-design --check-source-history
+```
+
+The verifier checks the written identity over the rationals, the three term
+prices, the dual-basis comparison, the A_2 control, the 1812-design enumeration
+and three rejection controls. It prints a JSON receipt bound to the package
+file hashes.
+
+## Limitations
+
+The enumeration is over one canonical representative per equality pattern, not
+over all rational carriers. The exact Gram-class minimum on A_3 is therefore
+open; 8 is an upper bound. The model is the scalar Gram price model with the
+F2 mask-rank rule and says nothing about a physical word, caller, compiler,
+native implementation, precision or restoration. No kappa changes.
+
+## Open next questions
+
+1. What is the exact Gram-class minimum on A_3? A lower-bound technique must
+   handle arbitrary rational carriers, not equality patterns. Start with the
+   four-term case, where the W factor has a one-parameter freedom
+   `W = W_0 + q r^T`; a useful first step is an exhaustive price-multiset case
+   analysis for totals below 8. Blocked by: no continuous lower-bound argument
+   is known for this cost.
+2. Is the A_n Gram-class cost `n^2` for every n, or does the A_3 value 8
+   (against the dual-basis 9) start a systematic `n^2 - 1` family? Start by
+   generalising the written pattern to n >= 4 and pricing it. Blocked by: the
+   general pattern is not constructed.
+3. Does the A_2 gap (Gram 4 against identity decoder 3) persist for some
+   n >= 3, and at which n does a Gram design match the identity decoder? Start
+   with n = 3 and the identity decoder cost 4. Blocked by: question 1.
+
+## Related open work
+
+No open PR is known to study the A_n Gram-class cost for n >= 3. The
+predecessor's package is merged with its own A_4 note left open; this package
+does not audit it.
+
+## Credit
+
+The model, the A_2 value 4 and the F2 mask-rank price rule are
+DreamingOfClouds' (`research/p104-duality-ceiling-flag-note`). The A_2 control
+reproduces their number. The explicit A_3 design, the dual-basis price
+comparison and the bounded enumeration are new. Independent human or formal
+review is unclaimed.

research/gram-class-a3-three-term-design/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/p104-duality-ceiling-flag-note/THEOREM.md",
+      "usage": "provenance",
+      "git_blob": "90d1e224b6a4183a2d0004e3d11af8da4d5e5433",
+      "sha256": "720b9b803d07e5217f5ca6b5511ec2727a74413034773ccab587cf20777a67dc"
+    },
+    {
+      "path": "research/p104-duality-ceiling-flag-note/README.md",
+      "usage": "provenance",
+      "git_blob": "d5fe91d99174118343bd23651690dd301c8e991a",
+      "sha256": "79f37525b4e765eb2c1a685fcf7aba0494c59f783b9ab3fd507800e03c3060bf"
+    }
+  ]
+}

research/gram-class-a3-three-term-design/TASK.json

@@ -0,0 +1,86 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the 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": "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.",
+    "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": [
+      "productive helper",
+      "target refinement",
+      "5599",
+      "5614"
+    ],
+    "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": "Explicit exact three-term Gram-class design on the A_3 line system of the p104-duality-ceiling-flag-note Gram model, its price 8 against the natural dual-basis design price 9, and a bounded enumeration of the 1812 three-term designs over the 14 canonical equality-pattern representatives (minimum 8).",
+  "scope_change_reason": "The card asks for a changed helper inventory with a complete signed bill. This package answers the small grammatical sub-question that the cited Gram model leaves open at A_3: the predecessor note states A_4 and every n >= 3 as outside its scope. It supplies an explicit design and a price comparison in that model, not a supplier, caller or kappa claim.",
+  "bottleneck_link": "Side result: it tests the F2 mask-rank price rule used for the P104 Gram-class floors on the next line system after the A_2 counterexample. It does not move the binding complex or BIT budget.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one exact design and one declared finite enumeration; no lower bound over all carriers, no physical word, no kappa.",
+  "outcome": "partial",
+  "evidence": "README.md and PROOF.md give the model, the identity and the price count. verify.py checks the rational identity, prices 3/3/2, the dual-basis cost 9, the A_2 control 4, all 1812 enumerated designs and three rejection controls; it prints a hash-bound receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact Gram-class minimum on A_3?",
+      "why_it_matters": "8 is only an upper bound; the exact value decides whether the A_2 gap widens at the next line system.",
+      "first_step": "Run the price-multiset case analysis for totals below 8, beginning with the four-term designs where W = W_0 + q r^T has one free direction.",
+      "blocked_by": "No continuous lower-bound argument is known for this cost; equality patterns do not determine prices."
+    },
+    {
+      "question": "Is the A_n Gram-class cost n^2 for every n, or does A_3 start an n^2 - 1 family?",
+      "why_it_matters": "A general formula would settle the A_n side of the Gram-class model rather than one case.",
+      "first_step": "Generalise the written three-term pattern to n >= 4 and price it; compare with the dual-basis n^2.",
+      "blocked_by": "The general pattern is not constructed."
+    },
+    {
+      "question": "Does the A_2 gap (Gram 4 against identity decoder 3) persist for some n >= 3?",
+      "why_it_matters": "This decides whether the A_2 toy is an anomaly or the start of a systematic failure of the naive transfer.",
+      "first_step": "Compare the identity decoder cost n+1 with the best explicit Gram design at n = 3 and n = 4.",
+      "blocked_by": "Depends on the exact A_3 minimum above."
+    }
+  ]
+}

research/gram-class-a3-three-term-design/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Exact rational A_3 design identity and prices, dual-basis cost 9, A_2 control 4, 1812-design enumeration, rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "The same exact checks under optimized Python with assertions active."
+    }
+  ]
+}