Prove a cost-39 floor for sparse rational E6 corrections (no κ)

research/e6-sparse-correction-floor/PROOF.md

@@ -0,0 +1,126 @@
+# A support obstruction for the fixed E6 correction
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written invoice proof with exact finite corroboration.
+
+## Contract and cited premises
+
+Use Cinna Davis / 1337isnot1337's PR2240 factorization, fixed dense pairing
+B0 and seven-term pricing contract. Write X for its full-column-rank
+36-by-6 coordinate matrix and H for its symmetric basis Gram matrix.
+The original six columns have the cited pairing ranks
+
+```text
+(r_1,r_2,r_3,r_4,r_5,r_6) = (6,7,6,6,6,6).
+```
+
+These ranks are trusted mathematical premises from PR2240, not independently
+recounted or re-certified here. Each nonzero term with pairing rank r has
+fully charged cost max(5,r). The source certificate, exact source head and
+retained bytes are pinned in SOURCES.json. Its model and Theorem C lineage
+credit PR1590 and the retained root-unit contributors.
+
+For nonzero rational a in Q^6 and nonzero rational lambda the correction is
+
+```text
+p_i = X e_i,       q_i = X(H e_i-lambda a_i a),   1<=i<=6,
+p_7 = X a,         q_7 = lambda X a.
+```
+
+Cancellation gives sum_i p_i q_i^T = X H X^T. The factorization and this
+identity are credited to PR2240. A genuine seven-term member has every q_i
+nonzero. X has full column rank, so the p_i, p_7 and q_7 are nonzero.
+
+## The new bound
+
+Let s be the number of nonzero coordinates of a, and let epsilon be one if
+a_2 is nonzero and zero otherwise. For every positive real q, the complete
+seven-term charged moment satisfies
+
+```text
+sum_(i=1)^7 max(5,r_i(new))^q
+ >= (s+1) 5^q + (5-s+epsilon) 6^q + (1-epsilon) 7^q.        (1)
+```
+
+In particular its unit-price charged cost C satisfies
+
+```text
+C >= 42-s-epsilon.                                       (2)
+```
+
+To prove (1), if a_i=0 then q_i=X H e_i and the entire original term,
+including its support and pairing rank, is unchanged. Exactly 5-s+epsilon
+of those fixed terms have rank six and 1-epsilon has rank seven. The s
+changed terms and the extra term each pay at least five. Positive powers
+preserve these inequalities. Summing proves (1); setting q=1 proves (2).
+This argument does not enumerate or bound the rational coefficients.
+
+The bound is sharp for the relaxation that records only the unchanged ranks
+and the five-unit floor of the other terms. Assigning five to every changed
+and extra term attains its right side. This is an abstract invoice witness,
+not a decoder, a simultaneous rank-attainment theorem or a physical program.
+
+## Consequences for the rational two-coordinate family
+
+Every direction supported on at most two coordinates has C>=39. If its
+support excludes coordinate two then a two-coordinate direction has C>=40.
+For the claimed plane a=e_1+t e_2, t rational, the floor is 39 when t!=0
+and 41 when t=0. No minimum decoder cost or attainment of either floor is
+asserted.
+
+The seven-term condition is automatic for these directions. The source
+basis matrix is
+
+```text
+H = [2 0 1 1 1 1
+     0 2 1 1 1 0
+     1 1 2 1 1 1
+     1 1 1 2 1 1
+     1 1 1 1 2 1
+     1 0 1 1 1 2].
+```
+
+Every H e_i has at least four nonzero coordinates. If q_i=0 then full column
+rank of X gives H e_i=lambda a_i a. If a_i=0 this contradicts H e_i!=0;
+otherwise its right side has at most two nonzero coordinates. This is also
+a contradiction. Thus the whole rational two-coordinate family, including
+all nonzero lambda, is covered without excluding untested degeneracies.
+
+Equation (2) also gives necessary support conditions for any genuine member
+to match or improve the original six-term cost 37. Cost at most 37 requires
+s+epsilon>=5, hence at least four nonzero coordinates; if exactly four,
+coordinate two must be included. Cost at most 36 requires at least five,
+again including coordinate two when there are exactly five. These are
+necessary conditions, not constructions or sufficient conditions.
+
+The elementary fixed-term argument is the new step. PR2240 supplies the
+factorization, the six ranks, finite-alphabet screen and tariff. PR2247
+changes the base by elementary shears and is outside this fixed-base result.
+DreamingOfClouds's PR2277 supplies the broader root-code floor 36. It already
+excludes cost 35 for all such root-code decoders. The new support gate is
+stronger for this sparse fixed-base family and does not replace that theorem.
+
+## Finite evidence and limits
+
+The verifier enumerates all 63 nonempty coordinate supports. For each support
+it exhausts charged ranks in {5,6,7} on its changed and extra terms, keeping
+the other ranks fixed. There are exactly 3(4^6-1)=12,285 abstract invoices.
+Every invoice dominates the sorted lower profile coordinatewise, and each
+of the 63 abstract minima attains (2). The bound for arbitrary larger ranks
+follows from the written monotonicity argument, not this finite alphabet.
+
+The new parameter fixtures cover all 15 coordinate pairs, four rational
+ratios outside the earlier ternary pair alphabet and four nonzero rational
+lambda values. These 240 fixtures check coefficient cancellation, unchanged
+terms and absence of zero factors. They do not recompute E6 pairing ranks or
+replay PR2240's published census. Five invalid supports are rejected, and
+explicit ordinary/exceptional/full-support boundaries guard the debit.
+
+This is a fully charged Theorem C invoice obstruction, not a raw-rank floor
+or complete physical supplier bill. Exact minimum cost on the rational plane,
+compatibility of the abstract minimum ranks, dense directions, changed bases,
+native realization, ownership/restoration, routing, precision/tape, stock,
+compiler and outer costs remain open. All five selected framework assumptions
+retain their status. No new kappa, selected-frontier change, supplier admission,
+complete multiplication theorem, independent human or formal proof-kernel
+acceptance is claimed.

research/e6-sparse-correction-floor/README.md

@@ -0,0 +1,119 @@
+# Every sparse two-coordinate E6 correction costs at least 39
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written invoice proof with exact finite corroboration.
+For Cinna Davis / 1337isnot1337's fixed PR2240 one-extra rank-one E6
+factorization and its fully charged Theorem C tariff, every nonzero rational
+correction direction supported on at most two coordinates costs at least 39,
+for every nonzero rational lambda. A two-coordinate direction that excludes
+coordinate two costs at least 40. Attainment is unclaimed.
+
+The [proof](PROOF.md) gives the support-sensitive moment bound, valid for every
+positive power q and every genuine seven-term member:
+
+```text
+sum charged_rank^q >= (s+1) 5^q + (5-s+epsilon) 6^q + (1-epsilon) 7^q,
+C >= 42-s-epsilon,
+s = support size of a,   epsilon = 1 if a_2 is nonzero, otherwise 0.
+```
+
+This strengthens PR2277's general root-code floor 36 on this sparse family.
+To match the original six-term cost 37, a genuine seven-term correction must
+touch at least four coordinates, including coordinate two when it touches exactly four. To reach
+36 requires at least five, including coordinate two when exactly five.
+These are new necessary support gates, not sufficient conditions or decoders.
+
+The lower profile is sharp in the abstract relaxation that retains only fixed
+term ranks and the five-unit charge floor. No E6 decoder is claimed to attain
+that abstract profile. The exact minimum on the rational two-parameter plane
+remains open.
+
+## Evidence and reproduction
+
+The standalone verifier enumerates every nonempty coordinate support and all
+12,285 declared abstract invoices. Each of the 63 support minima equals the
+new formula. It also checks 240 new rational coefficient fixtures across all
+coordinate pairs, five invalid supports and the ordinary, exceptional and
+full-support boundaries. It imports no predecessor executable and does not
+replay the predecessor's census or recompute its six published pairing ranks.
+Four scientific source mutations and one source-byte corruption were also
+rejected locally in both normal and optimized modes. Every run generates a
+receipt hashing all six package files and its pinned
+source certificate. No receipt is handwritten or committed.
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -X dev -W error -B research/e6-sparse-correction-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -X dev -W error -B research/e6-sparse-correction-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e6-sparse-correction-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e6-sparse-correction-floor --check-source-history
+```
+
+Another CPython 3.12 installation can replace the absolute interpreter path.
+The direct marker is PASS_E6_SPARSE_CORRECTION_FLOOR. Normal and optimized
+commands are read-only. A standalone export must retain the declared source
+certificate at its repository-relative path; direct replay then needs no Git.
+The metadata and committed-byte commands need repository history.
+
+## Sources and scope
+
+Cinna Davis / 1337isnot1337's [PR2240](https://github.com/CrocSwap/integer-mult-bounds/pull/2240),
+head c8a2b37056e766715c457f56e2dd8172f5bdbccd, supplies the fixed
+factorization, dense pairing, ranks (6,7,6,6,6,6), tariff and finite-alphabet
+screen. Those mathematical inputs are cited, not audited or independently
+re-certified. Its PR1590/root-unit lineage retains credit. PR2247 changes the
+base by shears. DreamingOfClouds's PR2277 supplies the broader root-code floor
+36, already excluding cost 35. The new gate is stronger on this sparse fixed
+base, and leaves those results intact.
+
+Scientific base is canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a,
+priorities revision 8, selected PR6030. [SOURCES.json](SOURCES.json) binds the
+source certificate as a live input and the source question as provenance.
+[TASK.json](TASK.json) records the change from the complex-rank-shape-decoder
+card to this scoped obstruction. Its supplier acceptance gate is not claimed.
+The current selected metadata control passed; its scientific replay was not run.
+
+The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371202)
+identifies the E6 target and its narrowed scope.
+Live open/account PRs, active Discussions, reservations, main/merged rational
+and support-sensitive searches were checked. The overlap snapshot covered
+522 open PRs and 6,534 Discussion records; omitted sparse notes, unpublished
+work and arbitrary historical diffs remain limits. No global novelty claim is
+made.
+
+No raw-rank bound, exact decoder minimum, physical supplier, new kappa,
+selected-frontier change or complete multiplication theorem is claimed.
+Native realization, ownership/restoration, routing, precision/tape, stock,
+compiler and outer costs remain separate. All five selected framework
+assumptions remain. Selected cold replay, Lean, Docker, independent human and
+formal proof-kernel review were not run or claimed.
+
+## Engineering bounds
+
+All loops have fixed finite bounds: 63 supports, at most 3^7 invoice choices,
+seven ranks, six coordinates and 240 rational fixtures. There is no recursion,
+dynamic code evaluation or external executable import. Each function is under
+60 lines and explicit invariant checks survive optimized execution.
+
+Power-of-Ten rule 3 has a managed-runtime deviation. Python integers, Fractions
+and temporary lists allocate during arithmetic. The fixed domains bound live
+records to one seven-rank invoice or six-by-six coefficient matrix, plus the
+source certificate, capped at 64 KiB. Any future general-input interface needs
+a new resource bound. Warning-strict normal/optimized runs, AST inspection,
+source corruption and scientific mutation controls are the applicable checks.
+No repository-wide analyzer configuration changes are needed for this package.
+
+## Open next questions
+
+1. Determine whether a genuine fixed-base correction attains the support-only
+   floor at support four or five. Start by checking simultaneous pairing-rank
+   compatibility at an explicit rational direction. The abstract invoice does
+   not supply that compatibility or a decoder.
+2. Determine the exact minimum on a=e_1+t e_2. Start with the support-change
+   arrangement in rational t and lambda. The present floor 39 is not claimed
+   attained; a universal two-parameter classification is unrun.
+3. Identify a changed base or a complete physical consumer that makes a lower
+   algebraic invoice useful. Start with its full paid contract. Frames,
+   restoration and native/outer costs are unresolved.

research/e6-sparse-correction-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/e6-one-extra-frame-seed4dd9/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "bdd765ed8b25a2c16343d6829b3bbdfd0668f5fc",
+      "sha256": "8fb24266bef48d57bee29573404b04c7b3eb996a733db02fa57538a1ce3dd0ae"
+    },
+    {
+      "path": "research/e6-one-extra-frame-seed4dd9/README.md",
+      "usage": "provenance",
+      "git_blob": "73270b0a515fcfbe6736695c7da271ac0e5305ca",
+      "sha256": "fd2c4645df6218549c81eaf07f159084f1b5e1df2c85e0b60cb5cd74c76f2d64"
+    }
+  ]
+}

research/e6-sparse-correction-floor/TASK.json

@@ -0,0 +1,93 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "A support-sensitive charged-moment obstruction for the fixed PR2240 rank-one E6 correction; every rational direction supported on at most two coordinates costs at least 39.",
+  "scope_change_reason": "Take an original sparse rational subfamily of PR2240, removing its finite direction alphabet on the claimed plane. Stop at the first new support obstruction; no supplier construction, predecessor audit or parameter sweep.",
+  "bottleneck_link": "Scoped decoder side result: reject sparse rational corrections before a larger direction search. This does not satisfy the card supplier acceptance gate or move the selected frontier.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified support obstruction. Leave exact decoder attainment and the rational parameter arrangement open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py: 63 support sets, 12285 abstract invoices, 240 new rational fixtures, 5 invalid supports and exact boundary controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a genuine fixed-base correction attain the support-only floor at support four or five?",
+      "why_it_matters": "Tests whether the new necessary invoice gate has compatible rank realizations.",
+      "first_step": "Check simultaneous pairing ranks for one explicit rational direction.",
+      "blocked_by": "The abstract minimum does not provide a compatible E6 decoder."
+    },
+    {
+      "question": "What is the exact minimum on a=e_1+t e_2?",
+      "why_it_matters": "Would sharpen the rational-plane floor to an exact decoder tariff.",
+      "first_step": "Classify the exact support-change arrangement in rational t and lambda.",
+      "blocked_by": "The two-parameter arrangement is unrun and attainment of 39 is unclaimed."
+    },
+    {
+      "question": "Can a changed base or physical caller use a lower decoder invoice?",
+      "why_it_matters": "Connects an algebraic bill to multiplication savings.",
+      "first_step": "State and charge the full native/frame/restoration/outer contract.",
+      "blocked_by": "No complete physical consumer or supplier mapping is supplied."
+    }
+  ],
+  "source_question": {
+    "pr": 2240,
+    "author": "1337isnot1337",
+    "head": "c8a2b37056e766715c457f56e2dd8172f5bdbccd"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371202"
+}