Add exact scalar-shadow row update lemma

research/stream-shadow-row-update/PrintAxioms.lean

@@ -0,0 +1,4 @@
+import StreamShadowRowUpdate
+
+#print axioms StreamShadowRowUpdate.scalRun_append
+#print axioms StreamShadowRowUpdate.S_append_event

research/stream-shadow-row-update/README.md

@@ -0,0 +1,74 @@
+# Exact scalar-shadow row recurrence
+
+**A universal interface lemma; no new multiplication bound or κ is claimed.**
+For any semiring `K`, register type `ι` with decidable equality, label type `Λ`,
+finite event prefix `es`, appended event `e`, and row/column indices `r,j`,
+`S_append_event` gives the exact update to row `r` of the scalar-shadow matrix
+`S (es ++ [e])`. It handles all five `LemmaG.Event` constructors:
+
+| Appended event | Updated scalar-shadow row |
+|---|---|
+| `relabel _ _ _` | unchanged |
+| `add t s q` | row `t` becomes row `t + q · row s` |
+| `scale t q` | row `t` becomes `q · row t` |
+| `copy c s _` | row `c` becomes row `s` |
+| `clear c _` | row `c` becomes zero |
+
+The Lean theorem is universal over every finite prefix and every coefficient in
+`K`; it assumes no field, commutativity, label admissibility, exact recipe,
+finite register count, or selected-word hypothesis. `scalRun_append` proves the
+event-order composition used by the recurrence. The proof reduces each case to
+Lemma G's scalar event semantics and is checked by Lean's kernel.
+
+## Why this interface matters
+
+The hyperplane-ended helper theorem in
+[`hyperplane-end-lean/PROOF.md`](../hyperplane-end-lean/PROOF.md) takes a unit-row
+certificate `hS` as an instance hypothesis. This recurrence makes the exact
+row-by-row update available as a proved Lean interface, so a future source-bound
+word proof can derive `hS` by composing its event trace instead of treating the
+matrix update as an external implementation convention.
+
+This result does **not** instantiate the recurrence on a complete emitted
+helper, prove any particular `hS`, discharge the recipe or footprint hypotheses,
+or change the selected exponent. The complete emitted-word-to-Lean event binding
+and supplier obligations remain separate.
+
+## Reproduce
+
+From this directory, with Lean 4.21.0 and network access for Mathlib's cache:
+
+```sh
+lake exe cache get
+lake build
+lake env lean PrintAxioms.lean
+```
+
+From the repository root, the registered replay and metadata check are:
+
+```sh
+python3 -B scripts/research_package.py --package research/stream-shadow-row-update --check-only
+python3 -B scripts/research_package.py --package research/stream-shadow-row-update
+```
+
+The package uses Mathlib v4.21.0 and the local, source-pinned Lemma G package.
+`SOURCES.json` pins the exact interface and hyperplane-end hypotheses at the
+base commit. No numerical experiment is used as proof evidence.
+
+## Open next questions
+
+Can `S_append_event` derive the unit-row hypothesis for one complete,
+source-pinned emitted helper? This would connect a concrete event transcript to
+the `hS` premise used by the hyperplane-end theorem. First bind the emitted
+events and their ordering to Lean `Event` values, then fold the recurrence and
+prove the resulting row equals the basis row. The binding from serialized
+records to Lean events is the remaining blocker; this package does not attempt
+that bridge.
+
+## Credit
+
+The scalar-shadow semantics and `S` matrix are from Lemma G, PR #484, authored
+by DreamingOfClouds with Claude Opus 5.5 assistance, and retained in the
+source-pinned `e8-lemma-g-lean` package. This contribution adds only the
+left-to-right composition and one-event row recurrence. Prepared by
+1337isnot1337 with OpenAI Codex assistance. Apache-2.0.

research/stream-shadow-row-update/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a",
+  "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"
+    },
+    {
+      "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean",
+      "usage": "input",
+      "git_blob": "e89897190307a6f3fcfb858f8de00cc5a7f49b3e",
+      "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8"
+    },
+    {
+      "path": "research/hyperplane-end-lean/PROOF.md",
+      "usage": "input",
+      "git_blob": "a94a2ac168c088a1282ea411766bc859178620df",
+      "sha256": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9"
+    }
+  ]
+}

research/stream-shadow-row-update/StreamShadowRowUpdate.lean

@@ -0,0 +1,48 @@
+import LemmaG.Stream
+
+namespace StreamShadowRowUpdate
+
+open LemmaG LemmaG.Stream
+
+variable {ι Λ K : Type*} [DecidableEq ι] [Semiring K]
+
+/-- Running a prefix and then a suffix is the same as running the prefix first and
+feeding its state to the suffix. `scalRun` uses the same left-to-right order as an
+emitted event list. -/
+theorem scalRun_append {M : Type*} [AddCommMonoid M] [Module K M]
+    (a b : List (Event ι Λ K)) (x : ι → M) :
+    scalRun (a ++ b) x = scalRun b (scalRun a x) := by
+  induction a generalizing x with
+  | nil => rfl
+  | cons e a ih =>
+      change scalRun (a ++ b) (e.scal x) = scalRun b (scalRun a (e.scal x))
+      exact ih (e.scal x)
+
+/-- Exact recurrence for one row of the scalar-shadow matrix after one appended event.
+
+The five cases match the scalar semantics: relabels are erased, additions replace the
+target row by `row_target + q * row_source`, scales multiply one row, copies replace a
+row by the source row, and clears zero one row. This theorem has no label-admissibility,
+recipe, field, commutativity, or finiteness assumptions. -/
+theorem S_append_event (es : List (Event ι Λ K)) (e : Event ι Λ K) (r j : ι) :
+    S (es ++ [e]) r j =
+      match e with
+      | .relabel _ _ _ => S es r j
+      | .add t s q => if r = t then S es t j + q * S es s j else S es r j
+      | .scale t q => if r = t then q * S es t j else S es r j
+      | .copy c s _ => if r = c then S es s j else S es r j
+      | .clear c _ => if r = c then 0 else S es r j := by
+  simp only [S]
+  rw [scalRun_append]
+  cases e with
+  | relabel t A B =>
+      by_cases h : r = t
+      · subst r
+        simp [scalRun, physRun, Event.scal, Event.phys]
+      · simp [scalRun, physRun, Event.scal, Event.phys, h]
+  | add t s q => simp [scalRun, physRun, Event.scal, Event.phys, Function.update_apply, smul_eq_mul]
+  | scale t q => simp [scalRun, physRun, Event.scal, Event.phys, Function.update_apply, smul_eq_mul]
+  | copy c s F => simp [scalRun, physRun, Event.scal, Event.phys, Function.update_apply]
+  | clear c F => simp [scalRun, physRun, Event.scal, Event.phys, Function.update_apply]
+
+end StreamShadowRowUpdate

research/stream-shadow-row-update/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 6,
+  "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Lean-prove the exact scalar-shadow row recurrence for appending any one of LemmaG.Event.relabel, add, scale, copy, or clear to an arbitrary finite event prefix, over every semiring and without a finite-register assumption.",
+  "scope_change_reason": "The broad formal-interface card is narrowed to the missing event-by-event matrix update that can later derive a concrete helper unit-row certificate. It does not bind any emitted word or close a supplier obligation.",
+  "bottleneck_link": "HyperplaneEnd.hpe_word takes the helper scalar-shadow unit row as hS. A kernel-proved update law exposes the exact recurrence a future source-bound event translation can fold to establish hS.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the universal five-constructor recurrence and axiom-checked Lean build pass. Do not expand this package into an emitted-word binding or selected-supplier claim.",
+  "outcome": "completed",
+  "evidence": "Lean 4.21.0 cold replay passed from a clean package directory with a fresh Mathlib cache: cache acquisition, full Lake build, and axiom probe. scalRun_append depends on no axioms; S_append_event depends only on the repository-allowed propext and Quot.sound. Registered package metadata and base-source pins pass check-only.",
+  "author": "1337isnot1337 with OpenAI Codex",
+  "ai_assistance": "OpenAI Codex assisted with source review, statement design, Lean proof, verifier and documentation. No independent human review is claimed.",
+  "open_questions": [
+    {
+      "question": "Can the recurrence derive the unit-row hypothesis for one complete source-pinned emitted helper?",
+      "why_it_matters": "That would connect the scalar-shadow algebra to the hS premise of the hyperplane-ended helper theorem.",
+      "first_step": "Bind one serialized helper event list to exact Lean Event constructors, then fold S_append_event and prove its final row is the basis row.",
+      "blocked_by": "A source-bound serializer-to-Lean Event mapping for a complete helper is outside this package."
+    }
+  ]
+}

research/stream-shadow-row-update/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e8-lemma-g-lean/LemmaG/Stream.lean",
+    "research/hyperplane-end-lean/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Pinned Lean 4.21.0 and Mathlib v4.21.0 build; no-admission source scan; axiom report for the prefix-composition and five-constructor row-update theorems."
+    }
+  ]
+}

research/stream-shadow-row-update/lake-manifest.json

@@ -0,0 +1,102 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "LemmaG",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../e8-lemma-g-lean",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.21.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.62",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "StreamShadowRowUpdate",
+ "lakeDir": ".lake"}

research/stream-shadow-row-update/lakefile.toml

@@ -0,0 +1,14 @@
+name = "StreamShadowRowUpdate"
+defaultTargets = ["StreamShadowRowUpdate"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.21.0"
+
+[[require]]
+name = "LemmaG"
+path = "../e8-lemma-g-lean"
+
+[[lean_lib]]
+name = "StreamShadowRowUpdate"

research/stream-shadow-row-update/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.21.0