Certify the screened P104 source-chart shortcut misses the debt-free …

research/p104-source-chart-shortcut/PROOF.md

@@ -0,0 +1,85 @@
+# Screened source chart after one Gram undo
+
+## Question
+
+Discussion #1166 comment 19035513 asks for one caller that fuses the physical
+source-normalization factor with a full-output interface and a favorable bill.
+The same handoff says a screened one-row Gram-undo shortcut still returns
+`F81 T^{-1} x` on the physical source, and that the missing rank-one factor
+costs 10816. This note proves that screening statement and the debt-free gate
+arithmetic. It does not construct the fused caller.
+
+## Local FULL is not F81
+
+Let `F81 = F_2^9 ⊗ F_2^9`, dimension 81. For a nonzero row vector `r` and a
+nonzero column vector `c`,
+
+- `E_row(r) = r ⊗ F_2^9` has dimension 9,
+- `E_col(c) = F_2^9 ⊗ c` has dimension 9,
+- `E_row(r) ∩ E_col(c) = span{r ⊗ c}` has dimension 1,
+- `E_row(r) + E_col(c)` has dimension 17,
+- the codimension of that span in `F81` is 64.
+
+The verifier checks all `511 × 511` nonzero pairs. Distinct nonzero `r` give
+distinct row charts. A zero vector is not a 9-dimensional chart. Completing
+one local row chart and one local column chart therefore leaves 64 dimensions
+of the common chart unpaid. Local FULL is not global `F81`.
+
+## The prepared entrance keeps `T^{-1}`
+
+Use the prepared cut from PR #3978. Write `A_r` and `A_c` for the two Gram
+factors, `K = T^{-1}`, and `F` for the common chart. The raw product and the
+physical source read are
+
+```text
+M = [[I - A_c A_r, -A_c], [A_r, I]],
+source = F * (M (K x, y))_1.
+```
+
+Polynomials are noncommutative. No relation `F K = K F` is used. Direct
+expansion gives the source monomials
+
+```text
++ F K x - F A_c A_r K x.
+```
+
+Every source monomial contains `K`. Setting `A_r = 0` (row Gram undo) or
+`A_c = 0` (column Gram undo) leaves exactly `F K x`. Replacing the entrance
+`(K x, y)` by `(x, y)` leaves `F x` instead. The Gram undo does not create
+the chart defect, and it does not remove it. The physical source after either
+one-axis undo is `F K x = F81 T^{-1} x`, not `F81 x`.
+
+## Debt-free gate
+
+The published conditional inventory in that same cut is `m = 81`,
+`W = 36608`, `N = 104^2 = 10816`, 208 calls, bare channel mass 2368 and
+persistent progress cap 2312. Those integers retie as
+
+```text
+81 W = 2965248,
+81 W - N - 208*2312 = 2473536,
+208*2368 + 2473536 = 2966080,
+excess = 832.
+```
+
+For a changed local profile with debt `d = mass - progress`, the necessary
+gate stated there is `C < N - 208 d`. At `d = 0` the strict allowance is
+`C < 10816`. The predecessor tariff charges one rank-one child for the chart
+`K` on each of the `N` data positions, cost `10816`. That cost equals the
+allowance, so the strict gate fails. The screened excess moves from `-N` to
+`0`, and the bill equals capacity `81 W` before helper, phase, owner, routing,
+tape or precision charges. Any further positive charge makes the excess
+positive.
+
+The inherited positive-debt route already fails by 832 before this factor.
+The debt-free calculation is the most favorable specialization of the same
+gate for this particular shortcut. It is not a universal P104 barrier, and it
+does not price the three-layer joint word (cost 32448 in PR #3978).
+
+## What would escape the obstruction
+
+An entrance that is already `(x, y)` rather than `(K x, y)` has source `F x`
+after the row undo, so this chart charge is not forced by the Gram undo alone.
+A fused caller can still change the entrance, the chart family, the debt, or
+the progress binding. Those changes need their own bill. Equality at `81 W`
+is already a failed strict gate for the screened shortcut.

research/p104-source-chart-shortcut/README.md

@@ -0,0 +1,62 @@
+# Screened P104 source chart after one Gram undo
+
+**Negative result for one shortcut. No new κ.** Selected conditional κ stays
+`0.001672660197076918`.
+
+## Scope and evidence
+
+Card `p104-side-correction`, scope **refined**. Discussion #1166 comment
+19035513 asks for a caller that fuses the physical source-normalization
+factor with a full-output interface and a favorable complete bill. This
+package does not build that caller. It certifies the screened shortcut named
+in that handoff.
+
+On `F81 = F_2^9 ⊗ F_2^9`, every nonzero row chart `r ⊗ F_2^9` and column chart
+`F_2^9 ⊗ c` meet in one line and span 17 dimensions. The codimension in `F81`
+is 64, over all `511 × 511` nonzero pairs. Local FULL is not global `F81`.
+
+On the prepared entrance `(T^{-1} x, y)` of the PR #3978 joint cut, deleting
+either Gram factor leaves the physical source equal to `F T^{-1} x`. The
+rank-one chart tariff on all `N = 104^2 = 10816` data positions equals the
+debt-free allowance `C < 10816`. The screened bill equals capacity `81 W =
+2965248` before any further nonnegative charge, so the strict gate fails.
+
+The proof is in [PROOF.md](PROOF.md). Exact integers are in [RESULT.json](RESULT.json).
+The inherited positive-debt excess 832 is retied only as a transcription check
+of the published `#3978` gate. PR #3978's head is not an ancestor of canonical
+main, so its files are cited rather than pinned as live inputs.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/p104-source-chart-shortcut
+```
+
+The chart census checks 261121 pairs and takes roughly twenty seconds on
+CPython 3.12. One registered command. No native replay, Lean, or Docker run.
+
+## Open next questions
+
+A fused caller that changes the entrance from `(T^{-1} x, y)` to a chart
+already cleared, or that changes the debt and progress binding, is not ruled
+out by equality at `81 W`. The first step is one literal producer whose source
+bank is `F x` at the same cut, with owners, dirty returns and a bill strictly
+under `81 W` after every nonnegative charge. It is blocked until that
+entrance and those charges are specified. Applying `T` as `N` extra rank-one
+children on this shortcut does not open a margin.
+
+## Credit
+
+The prepared cut, the gate `C < N - 208 d`, and the tariff that charges each
+`K = T^{-1}` as one rank-one child are PR #3978 (`48e2e44d8785be8204d8c4b719850332f4f9abe0`,
+`research/p104-joint-compensation`) by Chris R / Clear1nsight. The fusion
+question is discussion comment 19035513, from the same handoff as PRs #3981,
+#3979, #3984 and #3978. Retained lineage: Rohan Arun / #1972, Chafik
+Boukhalfa / #1991, Adam Gall / #1940, and the E8, native and compiler sources
+named there.
+
+New chart census, noncommutative source expansion and debt-free comparison
+are by unpaidmoon with Grok assistance in Cursor. Apache-2.0. No human or
+proof-assistant review is claimed. The selected frontier is unchanged.

research/p104-source-chart-shortcut/RESULT.json

@@ -0,0 +1,81 @@
+{
+  "charts": {
+    "field": 2,
+    "factor_dimension": 9,
+    "f81_dimension": 81,
+    "nonzero_row_charts": 511,
+    "pairs_checked": 261121,
+    "row_dimension": 9,
+    "column_dimension": 9,
+    "intersection_dimension": 1,
+    "span_dimension": 17,
+    "codimension_in_f81": 64
+  },
+  "identity": {
+    "full_source": [
+      {
+        "coeff": -1,
+        "atoms": [
+          "F",
+          "Ac",
+          "Ar",
+          "K",
+          "x"
+        ]
+      },
+      {
+        "coeff": 1,
+        "atoms": [
+          "F",
+          "K",
+          "x"
+        ]
+      }
+    ],
+    "row_undo_source": [
+      {
+        "coeff": 1,
+        "atoms": [
+          "F",
+          "K",
+          "x"
+        ]
+      }
+    ],
+    "column_undo_source": [
+      {
+        "coeff": 1,
+        "atoms": [
+          "F",
+          "K",
+          "x"
+        ]
+      }
+    ],
+    "row_undo_if_entrance_drops_K": [
+      {
+        "coeff": 1,
+        "atoms": [
+          "F",
+          "x"
+        ]
+      }
+    ]
+  },
+  "gate": {
+    "N": 10816,
+    "m": 81,
+    "W": 36608,
+    "calls": 208,
+    "capacity_81W": 2965248,
+    "inherited_positive_debt_excess": 832,
+    "debt_free_allowance": 10816,
+    "rank_one_chart_cost": 10816,
+    "strict_gate_passes": false,
+    "screened_excess": 0,
+    "screened_bill": 2965248
+  },
+  "checks": 3,
+  "controls": 5,
+  "kappa_claim": null
+}

research/p104-source-chart-shortcut/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/p104-source-chart-shortcut/TASK.json

@@ -0,0 +1,88 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/p104-native-channel/README.md",
+      "research/p104-native-channel/PROOF.md",
+      "docs/research/community-efficient1000-review.md",
+      "research/p104-joint-unit-flags/README.md"
+    ],
+    "methods": [
+      "Construct one side-correction word at an explicit chronological cut with the needed frames still available.",
+      "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget."
+    ],
+    "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.",
+    "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.",
+    "allowed_variations": [
+      "One correction factorization, one chronological cut, or one explicit hosting obstruction.",
+      "A changed correction schedule with an updated full bill and native frame contract."
+    ],
+    "scope_change_triggers": [
+      "Recompiling the already certified low-rank channel without closing a new obligation.",
+      "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.",
+      "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.",
+      "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful."
+    ],
+    "overlap_terms": [
+      "P104",
+      "I-G/2",
+      "side correction",
+      "native channel",
+      "1972",
+      "1991",
+      "2586",
+      "endpoint transport",
+      "physical dual",
+      "relay composition",
+      "2981",
+      "joint unit flags",
+      "acquisition delivery",
+      "static nesting"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.",
+        "evidence": "research/p104-joint-unit-flags/README.md",
+        "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.",
+        "status": "author-checked",
+        "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Certify that a one-axis Gram undo on the prepared P104 entrance leaves F T^{-1} x, and that the N rank-one chart tariff misses the debt-free strict gate.",
+  "scope_change_reason": "The card asks whether one chronological correction has an affordable complete bill. Discussion #1166 comment 19035513 narrows the next decision to fusing the physical source-normalization factor with a full-output interface. This package prices the screened one-axis shortcut named there and stops when that bill meets capacity. It does not construct the fused caller or repeat the PR #3978 three-layer word.",
+  "bottleneck_link": "A source-chart factor that consumes the entire debt-free allowance cannot be omitted from a P104 correction bill. The shortcut fails before it can reduce the binding complex side.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop if the screened chart tariff meets or exceeds the debt-free allowance. Do not expand into a fused native caller on this entrance.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md; RESULT.json; verify.py census of all 511x511 nonzero charts and the noncommutative source expansion.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Grok assistance in Cursor for the package, the finite chart census and the polynomial expansion. No human or proof-assistant review claimed.",
+  "open_questions": [
+    {
+      "question": "Does one literal producer whose source bank is already F x, rather than F T^{-1} x, have a complete owner and dirty-return bill strictly under 81W?",
+      "why_it_matters": "Equality at capacity kills only the screened shortcut that keeps the prepared entrance (T^{-1} x, y). A changed entrance can still be favorable.",
+      "first_step": "Pin one chronological source bank that equals F x at the PR #3978 cut, list its owners and dirty returns, and price every nonnegative charge against 81W = 2965248.",
+      "blocked_by": "No such entrance is specified. Paying N extra rank-one children for T on the present shortcut adds cost without creating a margin."
+    }
+  ]
+}

research/p104-source-chart-shortcut/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All 511x511 nonzero F2 chart pairs, noncommutative Gram-undo source identity, debt-free gate equality, and five mutants."
+    }
+  ]
+}