diff --git a/.github/workflows/p104-affine-complement-lean.yml b/.github/workflows/p104-affine-complement-lean.yml
new file mode 100644
index 0000000000..136ac06cd3
--- /dev/null
+++ b/.github/workflows/p104-affine-complement-lean.yml
@@ -0,0 +1,44 @@
+name: P104 affine complement Lean
+on:
+  pull_request:
+    paths:
+      - 'research/p104-affine-complement-lean/**'
+      - 'formal/lean/lean-toolchain'
+      - 'formal/lean/lakefile.toml'
+      - 'formal/lean/lake-manifest.json'
+      - '.github/workflows/p104-affine-complement-lean.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'research/p104-affine-complement-lean/**'
+      - 'formal/lean/lean-toolchain'
+      - 'formal/lean/lakefile.toml'
+      - 'formal/lean/lake-manifest.json'
+      - '.github/workflows/p104-affine-complement-lean.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  formal:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.12'
+      - name: Checksum-pinned official Lean
+        shell: bash
+        run: |
+          curl --fail --location --retry 3 https://github.com/leanprover/lean4/releases/download/v4.21.0/lean-4.21.0-linux.tar.zst -o "$RUNNER_TEMP/p104-lean.tar.zst"
+          echo "455c6df09d5bd54d2a51b137939c47e2dda816d512ac789c4b3642c9bf98bde8  $RUNNER_TEMP/p104-lean.tar.zst" | sha256sum --check
+          tar --zstd -xf "$RUNNER_TEMP/p104-lean.tar.zst" -C "$RUNNER_TEMP"
+          echo "$RUNNER_TEMP/lean-4.21.0-linux/bin" >> "$GITHUB_PATH"
+      - name: Provision pinned Mathlib modules
+        working-directory: formal/lean
+        run: lake exe cache get Mathlib.LinearAlgebra.Dual.Lemmas Mathlib.Algebra.Field.ZMod Mathlib.Data.Finset.Card
+      - name: Fresh kernel proof and rejecting controls
+        run: python -I -O -Werror -B research/p104-affine-complement-lean/check_lean.py
+      - run: git diff --exit-code
diff --git a/research/p104-affine-complement-lean/AffineComplement.lean b/research/p104-affine-complement-lean/AffineComplement.lean
new file mode 100644
index 0000000000..542a200673
--- /dev/null
+++ b/research/p104-affine-complement-lean/AffineComplement.lean
@@ -0,0 +1,126 @@
+import Mathlib.LinearAlgebra.Dual.Lemmas
+import Mathlib.Algebra.Field.ZMod
+import Mathlib.Data.Finset.Card
+import Lean
+
+set_option autoImplicit false
+
+/-! The geometric lemma in PR2920, without any circuit or cost assertion. -/
+namespace P104AffineComplement
+
+abbrev F₂ := ZMod 2
+
+variable {V : Type*} [AddCommGroup V] [Module F₂ V]
+
+/-- On the odd section, the two kernel tests are complementary. -/
+theorem complementary_tests (f q : V →ₗ[F₂] F₂) (x : V) (hx : q x = 1) :
+    ((f + q) x = 0 ↔ f x ≠ 0) := by
+  have htwo : ∀ a : F₂, a = 0 ∨ a = 1 := by decide
+  have htwo_one : (1 : F₂) + 1 = 0 := by decide
+  rcases htwo (f x) with h | h <;> simp [LinearMap.add_apply, hx, h, htwo_one]
+
+/-- The odd demand set is covered, without overlap, by the two kernels. -/
+theorem kernel_partition (D : Set V) (f q : V →ₗ[F₂] F₂)
+    (hodd : ∀ x ∈ D, q x = 1) :
+    D ∩ (LinearMap.ker f : Set V) ∪ D ∩ (LinearMap.ker (f + q) : Set V) = D ∧
+    Disjoint (D ∩ (LinearMap.ker f : Set V))
+      (D ∩ (LinearMap.ker (f + q) : Set V)) := by
+  constructor
+  · ext x
+    simp only [Set.mem_union, Set.mem_inter_iff, LinearMap.mem_ker]
+    constructor
+    · rintro (⟨hx, _⟩ | ⟨hx, _⟩) <;> exact hx
+    · intro hx
+      by_cases hf : f x = 0
+      · exact Or.inl ⟨hx, hf⟩
+      · exact Or.inr ⟨hx, (complementary_tests f q x (hodd x hx)).mpr hf⟩
+  · rw [Set.disjoint_left]
+    intro x hx hy
+    exact ((complementary_tests f q x (hodd x hx.1)).mp hy.2) hx.2
+
+/-- A split demand set forces both linear forms to be nonzero. -/
+theorem split_forms_nonzero (D : Set V) (f q : V →ₗ[F₂] F₂)
+    (hodd : ∀ x ∈ D, q x = 1)
+    (hin : ∃ x ∈ D, f x = 0) (hout : ∃ x ∈ D, f x ≠ 0) :
+    f ≠ 0 ∧ f + q ≠ 0 := by
+  rcases hin with ⟨x, hx, hfx⟩
+  rcases hout with ⟨y, _, hfy⟩
+  constructor
+  · intro hf
+    exact hfy (by simp [hf])
+  · intro hfq
+    have hz : (f + q) x = 0 := by simp [hfq]
+    have ho : (f + q) x = 1 := by simp [LinearMap.add_apply, hfx, hodd x hx]
+    exact zero_ne_one (hz.symm.trans ho)
+
+/-- Every nonzero binary linear functional has a codimension-one kernel. -/
+theorem kernel_codimension_one [FiniteDimensional F₂ V]
+    (f : V →ₗ[F₂] F₂) (hf : f ≠ 0) :
+    Module.finrank F₂ (LinearMap.ker f) + 1 = Module.finrank F₂ V := by
+  exact Module.Dual.finrank_ker_add_one_of_ne_zero hf
+
+/-- In dimension eight, any nontrivial odd-section split gives two 7-planes. -/
+theorem eight_dimensional_cover [FiniteDimensional F₂ V]
+    (hdim : Module.finrank F₂ V = 8) (D : Set V) (f q : V →ₗ[F₂] F₂)
+    (hodd : ∀ x ∈ D, q x = 1)
+    (hin : ∃ x ∈ D, f x = 0) (hout : ∃ x ∈ D, f x ≠ 0) :
+    Module.finrank F₂ (LinearMap.ker f) = 7 ∧
+    Module.finrank F₂ (LinearMap.ker (f + q)) = 7 ∧
+    D ∩ (LinearMap.ker f : Set V) ∪ D ∩ (LinearMap.ker (f + q) : Set V) = D ∧
+    Disjoint (D ∩ (LinearMap.ker f : Set V))
+      (D ∩ (LinearMap.ker (f + q) : Set V)) := by
+  have hn := split_forms_nonzero D f q hodd hin hout
+  have h₁ := kernel_codimension_one f hn.1
+  have h₂ := kernel_codimension_one (f + q) hn.2
+  have hp := kernel_partition D f q hodd
+  exact ⟨by omega, by omega, hp.1, hp.2⟩
+
+/-- Finite demand counts partition exactly; no maximality assumption is needed. -/
+theorem finite_partition_counts (D : Finset V) (f q : V →ₗ[F₂] F₂)
+    (hodd : ∀ x ∈ D, q x = 1) :
+    (D.filter (fun x => f x = 0)).card +
+      (D.filter (fun x => (f + q) x = 0)).card = D.card := by
+  classical
+  have he : D.filter (fun x => (f + q) x = 0) = D.filter (fun x => ¬ f x = 0) := by
+    apply Finset.filter_congr
+    intro x hx
+    exact complementary_tests f q x (hodd x hx)
+  rw [he]
+  exact Finset.filter_card_add_filter_neg_card_eq_card _
+
+/-- Omitting the odd-section premise permits overlapping kernel membership. -/
+theorem even_point_counterexample :
+    ∃ x : F₂, (LinearMap.id : F₂ →ₗ[F₂] F₂) x = 0 ∧
+      ((LinearMap.id : F₂ →ₗ[F₂] F₂) + (LinearMap.id : F₂ →ₗ[F₂] F₂)) x = 0 := by
+  exact ⟨0, by simp, by simp⟩
+
+/-- Omitting nontriviality permits a full-dimensional first kernel. -/
+theorem zero_form_counterexample :
+    ∃ D : Set F₂, ∃ f q : F₂ →ₗ[F₂] F₂,
+      (∀ x ∈ D, q x = 1) ∧ LinearMap.ker f = ⊤ := by
+  exact ⟨{1}, 0, LinearMap.id, by simp, by simp⟩
+
+end P104AffineComplement
+
+/- Dependency audit adapted from research/cyclic-schur-lean/Audit.lean,
+   prepared for Ali Romman. It checks every theorem in this namespace. -/
+open Lean Elab Command in
+def auditP104AffineComplement : CommandElabM Unit := do
+  let env ← getEnv
+  let mut count := 0
+  for (name, _) in env.constants do
+    if (`P104AffineComplement).isPrefixOf name then
+      if getOriginalConstKind? env name == some .axiom then
+        throwError "Package axiom: {name}"
+      if getOriginalConstKind? env name == some .thm then
+        count := count + 1
+        let axioms ← collectAxioms name
+        for axiomName in axioms do
+          unless #[`propext, `Classical.choice, `Quot.sound].contains axiomName do
+            throwError "Forbidden axiom in {name}: {axiomName}"
+        logInfo m!"AXIOMS {name}: {axioms.toList}"
+  unless count == 13 do
+    throwError "Expected eight statements and five generated proofs, got {count}"
+  logInfo "PASS_P104_AFFINE_COMPLEMENT_LEAN statements=8 declarations=13 standard_axioms_only"
+
+run_cmd auditP104AffineComplement
diff --git a/research/p104-affine-complement-lean/README.md b/research/p104-affine-complement-lean/README.md
new file mode 100644
index 0000000000..1911bde285
--- /dev/null
+++ b/research/p104-affine-complement-lean/README.md
@@ -0,0 +1,158 @@
+# P104 affine-complement lemma in Lean
+
+Lean checks the geometric implication used in Nick Petalas's
+[PR2920](https://github.com/CrocSwap/integer-mult-bounds/pull/2920), exact head
+`b9ea9def949f9d71d59e21294d0e6cfbe0692a73`. This is independent proof coverage
+of an existing lemma, not a new endpoint bound, correction circuit or kappa.
+
+Let V be a binary vector space, D a demand set and f,q linear functionals.
+Assume q(x)=1 for every x in D. Then
+
+```text
+D intersect ker(f) and D intersect ker(f+q)
+are disjoint and their union is D.
+```
+
+If f vanishes on some demand and does not vanish on another, both f and f+q
+are nonzero. In finite dimension their kernels have codimension one.
+For dimension eight they are genuine dimension-seven subspaces. For a finite
+D, the two intersection cardinalities sum exactly to |D|. Choosing a
+maximizing f is unnecessary for the partition theorem; maximality only
+identifies PR2920's first cardinality as its previously computed b.
+
+## Formal statements and finite binding
+
+[AffineComplement.lean](AffineComplement.lean) contains eight named statements:
+
+- `complementary_tests`, the pointwise binary identity;
+- `kernel_partition`, disjoint coverage for arbitrary sets;
+- `split_forms_nonzero`, the two nontrivial linear functionals;
+- `kernel_codimension_one`, using Mathlib's existing dual-space lemma;
+- `eight_dimensional_cover`, the dimension-eight specialization;
+- `finite_partition_counts`, the finite cardinality identity;
+- `even_point_counterexample`, overlap without the odd-section premise;
+- `zero_form_counterexample`, a full kernel without a nontrivial split.
+
+The embedded audit checks every theorem in the package namespace, including
+five compiler-generated proof helpers. All thirteen declarations use only
+`propext`, `Quot.sound` and `Classical.choice`. It rejects package axioms,
+`sorryAx` and any other axiom dependency. The proofs use kernel reduction,
+not `native_decide` or an external proof oracle.
+
+[verify.py](verify.py) separately reconstructs the 104 arrival and 104 departure
+residual sets from the frozen PR1972/1991 word and ordered root fixture. It
+checks their rank eight, endpoint containment, odd functional, nontrivial
+split, two 128-point kernels and disjoint exact demand coverage. Each orientation
+has 4,656 residual demands. The combined census is:
+
+| Demand size | First part | Second part | Endpoints |
+| ---: | ---: | ---: | ---: |
+| 36 | 24 | 12 | 24 |
+| 44 | 28 | 16 | 48 |
+| 45 | 30 | 15 | 16 |
+| 46 | 29 | 17 | 48 |
+| 47 | 30 | 17 | 48 |
+| 48 | 30 | 18 | 24 |
+
+The binary integer encoding represents vectors by nine bits, functionals by
+bit parity, and functional addition by XOR. Restricting to each endpoint
+hyperplane gives the eight-dimensional space in the Lean theorem. This
+encoding and the source-to-residual reconstruction are an explicit mathematical
+correspondence, **not a Lean proof of the Python extractor**. The finite checker
+is a separately implemented corroboration, not new mathematical coverage by
+itself. [RESULT.json](RESULT.json) binds its complete census and witness digest.
+The price optimization in PR2920 is not formalized or rerun here.
+
+## Reproduce
+
+Finite premises and their three behavioral test groups, Python 3.12+:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/p104-affine-complement-lean
+```
+
+This opt-in replay is Git-free after metadata checking and needs no Lean.
+It does **not** check the formal proof. Its tests cover a positive fixture,
+missing odd/nontriviality premises, source and typed receipt corruption, and
+optimized source-export execution.
+
+For the proof, provision the repository's existing pinned environment once:
+
+```sh
+cd formal/lean
+lake exe cache get Mathlib.LinearAlgebra.Dual.Lemmas Mathlib.Algebra.Field.ZMod Mathlib.Data.Finset.Card
+cd ../..
+python3.12 -I -O -Werror -B research/p104-affine-complement-lean/check_lean.py
+```
+
+The checker requires official Lean 4.21.0 at compiler commit
+`6741444a63eec253a7eae7a83f1beb3de015023d`, Mathlib
+`308445d7985027f538e281e18df29ca16ede2ba3`, and all transitive Git pins from
+`formal/lean/lake-manifest.json`. It authenticates the environment configuration,
+checks dependency checkout heads, discards inherited Lean search paths, and
+compiles a fresh temporary proof copy. It writes no proof objects into the
+package and downloads nothing. `--formal-root PATH` can reuse another checkout
+with exactly the same configuration and dependencies. Compiled library caches
+and the official compiler remain trusted; the checker does not rebuild Mathlib.
+
+Five controls must reject: the wrong complement predicate, dimension eight
+instead of seven, an incomplete proof, an injected custom axiom and a missing
+audit command. The last control isolates the required success-marker guard.
+Expected final marker:
+
+```text
+PASS_P104_AFFINE_FORMAL_CONTROLS rejected=5
+```
+
+The dedicated [workflow](../../.github/workflows/p104-affine-complement-lean.yml)
+provisions the pinned Lean/Mathlib environment and runs these formal checks.
+Hosted execution is separate from local evidence. Local Linux x86_64 runs of
+both checkers and all controls passed with CPython 3.12.15. Ruff and
+warning-as-error Python compilation passed. No independent human review is claimed.
+
+## Scope, credit and open next questions
+
+Task `p104-side-correction` is **changed** to a formal-audit side result because
+live PR2920 already supplied the separate endpoint geometry and price analysis.
+Base main is `90a72fb3739bfe4e8b8148a8f3dd7de876cfb022`, priority revision 5.
+[Task metadata](TASK.json) records source heads, the chooser nonce, canonical
+claim and stopping rule. [SOURCES.json](SOURCES.json) pins every live input.
+Frozen predecessors and the selected frontier remain unchanged.
+
+Credit Nick Petalas/PR2920/2909/2896 for the geometric lemma and residual-count
+analysis; Hiroki Kumazaki/PR2889/2353 for endpoint spans and the monotone
+contract; Arham Tahir/PR2675/2682 for the cost-relaxation context; ywz65/PR2614
+for later-readable source handling; Sagar Thakrar's mixer handoff; and Philippe
+Van Velzen's relay work. Retain Rohan Arun/PR1972, Chafik Boukhalfa/PR1991,
+Adam Gall/PR1940, Josie Elliston/PR1071, Ali Romman/PR1125 and the geometry/native
+lineage. The dependency-audit pattern is adapted from Ali Romman's
+`research/cyclic-schur-lean/Audit.lean`; Mathlib supplies rank-nullity facts.
+Nick Petalas. Apache-2.0. Substantial AI assistance is disclosed in TASK.json.
+
+### Open next questions
+
+The remaining question is PR2920's joint flag/acquisition handoff. Can an
+affordable complete helper collection actually acquire and deliver the required
+coefficients in chronological order and restore arbitrary dirty state? First
+specify one actual joint dependency assignment and respect the existing mixer,
+endpoint and cut bounds. Separate endpoint covers do not supply such a program.
+Its physical owners, routing, idle work, precision, all-size lifting and entire
+consumer bill are still missing. This package finishes a proof audit and stops;
+it neither admits a supplier nor justifies a construction campaign.
+
+## Engineering limits
+
+Build the Lever shaped the rerunnable proof and mutation checker. Prove It Works
+required kernel checking, actual source premises and rejecting controls. New
+Python functions are below 60 lines. Loop domains are fixed by 4,058 events,
+208 endpoints, 512 vectors, 48 demands per endpoint, at most sixteen dependency
+pins and five proof mutants. Lean invocations have 90-second timeouts.
+
+Power of Ten deviations: Python's managed allocations are bounded by those
+finite domains and 2 MB input-file limits; no fixed-capacity runtime is claimed.
+Importlib in the tests loads exactly the package's own verifier. Lean tactics,
+Mathlib and the namespace dependency audit use trusted metaprogramming; the
+resulting proof terms are kernel-checked and the audit's failure paths are
+exercised. Replacing those runtime mechanisms would require a separate checker,
+not changes to frozen sources. No full selected cold replay, native P104 replay,
+rounding/circuit semantics or multiplication theorem is checked.
diff --git a/research/p104-affine-complement-lean/RESULT.json b/research/p104-affine-complement-lean/RESULT.json
new file mode 100644
index 0000000000..bbd44104da
--- /dev/null
+++ b/research/p104-affine-complement-lean/RESULT.json
@@ -0,0 +1,43 @@
+{
+  "census": [
+    [
+      36,
+      24,
+      12,
+      24
+    ],
+    [
+      44,
+      28,
+      16,
+      48
+    ],
+    [
+      45,
+      30,
+      15,
+      16
+    ],
+    [
+      46,
+      29,
+      17,
+      48
+    ],
+    [
+      47,
+      30,
+      17,
+      48
+    ],
+    [
+      48,
+      30,
+      18,
+      24
+    ]
+  ],
+  "covers_sha256": "fb9767bc2de82facb08887ba4a28b0e43cc41937c38be72f4601ce6f85c5d02b",
+  "endpoints": 208,
+  "residuals_per_orientation": 4656
+}
diff --git a/research/p104-affine-complement-lean/SOURCES.json b/research/p104-affine-complement-lean/SOURCES.json
new file mode 100644
index 0000000000..74787ed2b0
--- /dev/null
+++ b/research/p104-affine-complement-lean/SOURCES.json
@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "90a72fb3739bfe4e8b8148a8f3dd7de876cfb022",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "889b95d936746df124872133ae1e7cc339adcb92",
+      "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json",
+      "usage": "input",
+      "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706",
+      "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/P104-FIXTURE.json",
+      "usage": "input",
+      "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9",
+      "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4"
+    },
+    {
+      "path": "formal/lean/lake-manifest.json",
+      "usage": "input",
+      "git_blob": "36433bd6697cc16c39ff03acf97431386cb0f2c2",
+      "sha256": "702bd5bcfbf4a4739bea2e1cba72b471e8f0680520c67547f5daf3d0f26b6ddf"
+    },
+    {
+      "path": "formal/lean/lakefile.toml",
+      "usage": "input",
+      "git_blob": "b6abf04c93acf5ec745aa06aa1b503575b454186",
+      "sha256": "e5b1a6ff207cdd5e64b04ebfd944274d0ccde896f415bb578deb6090b4175ed5"
+    },
+    {
+      "path": "formal/lean/lean-toolchain",
+      "usage": "input",
+      "git_blob": "980709bbbae28702ec58c368b84fdf6638093c63",
+      "sha256": "d24fed434d3b13adfaab57724a0a7f270ea8bf1c818b5ae5cf25cbce24dd685c"
+    },
+    {
+      "path": "research/cyclic-schur-lean/Audit.lean",
+      "usage": "provenance",
+      "git_blob": "8158ecfe822f619f6f6ebdabeef48eca4fa175c9",
+      "sha256": "8c21b111cccab46b1980d937090838e1a3d76e83f767fce8cc9793e9494af462"
+    }
+  ]
+}
diff --git a/research/p104-affine-complement-lean/TASK.json b/research/p104-affine-complement-lean/TASK.json
new file mode 100644
index 0000000000..49a8e0e133
--- /dev/null
+++ b/research/p104-affine-complement-lean/TASK.json
@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 5,
+  "base_commit": "90a72fb3739bfe4e8b8148a8f3dd7de876cfb022",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Which unresolved physical correction, endpoint transport or hosting obligation in a pinned P104 follow-up can be closed or decisively rejected?",
+    "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"
+    ],
+    "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 P104 row in research-family-status.md and its exact pending source heads before choosing a task. #1991 is the reviewed channel; #2586 is a pending physical dual with explicit added transport costs, not an admitted supplier.",
+      "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": "Check live claims, pin the chosen follow-up and reproduce only the evidence needed for one unresolved obligation. Compare its complete correction/transport/hosting invoice with the target budget; test legal chronological access. Do not rebuild #1991 or assume #2586 has solved global admission.",
+    "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."
+    ],
+    "overlap_terms": [
+      "P104",
+      "I-G/2",
+      "side correction",
+      "native channel",
+      "1972",
+      "1991",
+      "2586",
+      "endpoint transport",
+      "physical dual",
+      "relay composition"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independent Lean formalization of PR2920's affine-complement implication and source-bound checking of its 208 endpoint hypotheses, not construction or cost optimization.",
+  "scope_change_reason": "Live overlap showed that endpoint counts, separate subspace-union attainment and two-history pricing were already supplied by PR2896/2909/2920. This side result adds kernel-checked universal proof coverage rather than reconstructing that work.",
+  "bottleneck_link": "The geometric lemma supports the P104 endpoint relaxation. It supplies no joint acquisition/restoration program and resolves none of the unknown complete supplier costs.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish one scoped formal lemma, check its finite premises and rejecting controls, then stop. No dependent construction campaign or family expansion.",
+  "outcome": "completed",
+  "evidence": "AffineComplement.lean proves eight named statements and audits all thirteen theorem declarations including generated helpers. check_lean.py checks the official pinned Lean/Mathlib environment and five rejecting proof controls. verify.py reconstructs all 208 endpoint hypotheses from immutable inputs; RESULT.json and three behavioral test groups record the finite check.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Substantial AI assistance in proof drafting, implementation, verification and prose. No independent human review or separate-agent review is claimed.",
+  "selection_nonce": "1b0a1ad9767cfd7601144c60f137d6af",
+  "milestone": "scoped formal audit",
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18971688",
+  "predecessors": [
+    {"pr": 2920, "head": "b9ea9def949f9d71d59e21294d0e6cfbe0692a73", "author": "Nick Petalas", "contribution": "affine-complement lemma and separate endpoint/price analysis"},
+    {"pr": 2909, "head": "4f394cfd3244b336e59b7adaded883277b66b637", "author": "Nick Petalas", "contribution": "endpoint-saturated count relaxation"},
+    {"pr": 2896, "head": "d33e8066de4d3e3b8230f2b3635d7bdcd80155ad", "author": "Nick Petalas", "contribution": "residual demand sets and endpoint support capacities"}
+  ],
+  "environment": "Linux x86_64; CPython 3.12.15; official Lean 4.21.0 commit 6741444a63eec253a7eae7a83f1beb3de015023d; Mathlib 308445d7985027f538e281e18df29ca16ede2ba3 and transitive pins in formal/lean/lake-manifest.json.",
+  "family_decision": "Audit complete, stop. Physical acquisition, coefficients, chronology, restoration, native realization, owners/routing/idle, precision and all-size costs remain unknown. No supplier admission or selected frontier change.",
+  "freshness": {
+    "upstream_commit": "a7482490b4ca256db67d767a33fa6f7553060807",
+    "priority_revision": 5,
+    "checked_at_utc": "2026-10-16T11:22:08Z",
+    "relevant_changes": "None in guidance, selected record, declared inputs, formal environment or replay runner. Scientific pins remain at starting main.",
+    "overlap": "496 open PRs, 2119 closed PR bodies and 1597 Discussion records, complete pagination and no warnings. No focused formalization match; arbitrary diffs and unpublished work remain outside coverage. PR2920 head unchanged."
+  },
+  "validation": [
+    "CPython 3.12.15 registered replay and three behavioral test groups passed.",
+    "CPython 3.12.15 optimized formal runner passed with eight statements, thirteen audited declarations and five rejecting controls in the pinned official Lean/Mathlib environment.",
+    "Ruff check and warning-as-error Python source compilation passed.",
+    "CPython 3.13.5 research-workflow suite ran 144 tests successfully with five skips. Expected deliberate-failure fixture tracebacks are present in its output.",
+    "No independent subagent tool was available; proof/interface and runner/failure-path self-reviews were performed separately. No independent human review, full selected replay or hosted-CI success is claimed."
+  ],
+  "open_questions": [
+    {
+      "question": "Can any affordable complete helper collection realize both endpoint flag assignments with actual source acquisition and dirty restoration?",
+      "why_it_matters": "Separate kernel partitions and optimistic prices do not establish a complete P104 correction.",
+      "first_step": "Follow PR2920's canonical handoff and specify one actual joint flag/dependency assignment before native synthesis; preserve existing lifetime and cut lower bounds.",
+      "blocked_by": "No joint chronological coefficient/restoration program or complete physical consumer bill is provided. This formalization does not justify another construction round."
+    }
+  ]
+}
diff --git a/research/p104-affine-complement-lean/VERIFY.json b/research/p104-affine-complement-lean/VERIFY.json
new file mode 100644
index 0000000000..ca65545bfe
--- /dev/null
+++ b/research/p104-affine-complement-lean/VERIFY.json
@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-native-channel/inputs/LOWRANK-WITNESS.json",
+    "research/p104-native-channel/inputs/P104-FIXTURE.json",
+    "formal/lean/lake-manifest.json",
+    "formal/lean/lakefile.toml",
+    "formal/lean/lean-toolchain"
+  ],
+  "commands": [
+    {
+      "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/verify.py"],
+      "timeout_seconds": 60,
+      "checks": "Source authentication and all 208 finite endpoint hypotheses; NOT the Lean proof"
+    },
+    {
+      "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/test_verify.py"],
+      "timeout_seconds": 60,
+      "checks": "Finite positive fixture, weakened hypotheses, typed receipt and source faults, Git-free replay"
+    }
+  ]
+}
diff --git a/research/p104-affine-complement-lean/check_lean.py b/research/p104-affine-complement-lean/check_lean.py
new file mode 100644
index 0000000000..cbd774cea0
--- /dev/null
+++ b/research/p104-affine-complement-lean/check_lean.py
@@ -0,0 +1,114 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Kernel-check the proof and deliberately invalid variants in temporary storage."""
+
+import argparse
+import hashlib
+import json
+import os
+import shutil
+import subprocess
+import tempfile
+from pathlib import Path
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+MARKER = 'PASS_P104_AFFINE_COMPLEMENT_LEAN statements=8 declarations=13 standard_axioms_only'
+LEAN_COMMIT = '6741444a63eec253a7eae7a83f1beb3de015023d'
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def run(argv, formal_root, timeout=90):
+    env = os.environ.copy()
+    for key in ('LEAN_PATH', 'LEAN_SYSROOT', 'LEAN_SRC_PATH'):
+        env.pop(key, None)
+    return subprocess.run(argv, check=False, cwd=formal_root, env=env, text=True,
+                          stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=timeout)
+
+
+def check_environment(lake, formal_root):
+    sources = json.loads((PACKAGE / 'SOURCES.json').read_text())['files']
+    require(len(sources) <= 16, 'source pin count bound')
+    formal_pins = [row for row in sources if row['path'].startswith('formal/lean/')]
+    require(len(formal_pins) == 3, 'three formal environment pins')
+    for row in formal_pins:
+        data = (formal_root / Path(row['path']).name).read_bytes()
+        require(hashlib.sha256(data).hexdigest() == row['sha256'], 'formal environment hash')
+    for flag, expected in [('--short-version', '4.21.0'), ('--githash', LEAN_COMMIT)]:
+        result = run([lake, 'env', 'lean', flag], formal_root, 30)
+        require(result.returncode == 0 and result.stdout.strip() == expected,
+                'official Lean 4.21.0 required: ' + result.stdout)
+    pinned = json.loads((ROOT / 'formal/lean/lake-manifest.json').read_text())
+    actual = json.loads((formal_root / 'lake-manifest.json').read_text())
+    require(actual == pinned, 'pinned Mathlib environment manifest')
+    require(len(pinned['packages']) <= 16, 'dependency count bound')
+    for dep in pinned['packages']:
+        folder = formal_root / '.lake/packages' / dep['name']
+        result = run(['git', '-C', str(folder), 'rev-parse', 'HEAD'], formal_root, 10)
+        require(result.returncode == 0 and result.stdout.strip() == dep['rev'],
+                'wrong or unavailable dependency: ' + dep['name'])
+
+
+def replace_once(source, old, new):
+    require(source.count(old) == 1, 'unique control anchor')
+    return source.replace(old, new, 1)
+
+
+def controls(source):
+    yield ('wrong_complement', replace_once(source,
+           '((f + q) x = 0 ↔ f x ≠ 0)', '((f + q) x = 0 ↔ f x = 0)'), 'unsolved goals')
+    yield ('wrong_dimension', replace_once(source,
+           'Module.finrank F₂ (LinearMap.ker f) = 7 ∧',
+           'Module.finrank F₂ (LinearMap.ker f) = 8 ∧'), 'omega could not prove')
+    start = source.index('  have htwo :')
+    end = source.index('\n/-- The odd demand', start)
+    yield ('incomplete_proof', source[:start] + '  sorry\n' + source[end:], "uses 'sorry'")
+    fake = source[:start] + '  exact False.elim P104AffineComplement.injected\n' + source[end:]
+    fake = replace_once(fake, 'namespace P104AffineComplement',
+                        'namespace P104AffineComplement\naxiom injected : False')
+    yield ('custom_axiom', fake, 'axiom in P104AffineComplement.')
+    yield ('missing_audit', replace_once(source, 'run_cmd auditP104AffineComplement', ''), None)
+
+
+def check(lake, formal_root):
+    check_environment(lake, formal_root)
+    source = (PACKAGE / 'AffineComplement.lean').read_text()
+    with tempfile.TemporaryDirectory(prefix='p104-affine-lean-') as tmp:
+        path = Path(tmp) / 'AffineComplement.lean'
+        path.write_text(source)
+        command = [lake, 'env', 'lean', '-j1', '-DwarningAsError=true']
+        positive = run(command + [str(path)], formal_root)
+        require(positive.returncode == 0 and MARKER in positive.stdout, positive.stdout)
+        print(positive.stdout, end='')
+        count = 0
+        for name, mutated, diagnostic in controls(source):
+            path.write_text(mutated)
+            result = run(command + [str(path)], formal_root)
+            if diagnostic is None:
+                require(result.returncode == 0 and MARKER not in result.stdout,
+                        'missing-audit control did not isolate marker check')
+            else:
+                require(result.returncode != 0 and diagnostic in result.stdout,
+                        'control did not reject for expected reason: ' + name + '\n' + result.stdout)
+            print('REJECTED_' + name)
+            count += 1
+        require(count == 5, 'five proof controls')
+    print('PASS_P104_AFFINE_FORMAL_CONTROLS rejected=5')
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--lake', default='lake')
+    parser.add_argument('--formal-root', type=Path, default=ROOT / 'formal/lean')
+    args = parser.parse_args()
+    lake = shutil.which(args.lake)
+    require(lake is not None, 'lake unavailable; provision the pinned environment')
+    check(lake, args.formal_root.resolve())
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/p104-affine-complement-lean/test_verify.py b/research/p104-affine-complement-lean/test_verify.py
new file mode 100644
index 0000000000..0c953b7fda
--- /dev/null
+++ b/research/p104-affine-complement-lean/test_verify.py
@@ -0,0 +1,67 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Behavioral controls for finite premises; formal controls are in check_lean.py."""
+
+import importlib.util
+import json
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+from pathlib import Path
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+spec = importlib.util.spec_from_file_location('affine_premises', PACKAGE / 'verify.py')
+verify = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(verify)
+
+
+class PremiseTests(unittest.TestCase):
+    def test_source_bound_result(self):
+        self.assertEqual(verify.calculate(), verify.load(PACKAGE / 'RESULT.json'))
+
+    def test_necessary_hypotheses(self):
+        # An eight-dimensional odd section in the low eight bits.
+        points = {v for v in range(256) if v & 1}
+        points = set(sorted(points)[:47]) | {129}
+        self.assertEqual(verify.rank(points), 8)
+        first, second = verify.check_cover(points, 256, 1, 2)
+        self.assertEqual(first + second, 48)
+        for q, f, error in [(0, 2, 'form bounds'), (2, 2, 'odd-section'),
+                            (1, 256, 'nontrivial split')]:
+            with self.assertRaisesRegex(ValueError, error):
+                verify.check_cover(points, 256, q, f)
+        with self.assertRaisesRegex(ValueError, 'duplicate JSON'):
+            json.loads('{"a": 1, "a": 2}', object_pairs_hook=verify.unique)
+
+    def test_git_free_and_corruptions(self):
+        with tempfile.TemporaryDirectory(prefix='p104-affine-test-') as tmp:
+            root = Path(tmp)
+            package = root / 'research' / PACKAGE.name
+            shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns('__pycache__', '.lake'))
+            for row in verify.load(PACKAGE / 'SOURCES.json')['files']:
+                if row['usage'] == 'input':
+                    path = root / row['path']
+                    path.parent.mkdir(parents=True, exist_ok=True)
+                    shutil.copyfile(ROOT / row['path'], path)
+            command = [sys.executable, '-I', '-O', '-Werror', '-B', str(package / 'verify.py')]
+            result = subprocess.run(command, check=False, capture_output=True, text=True, timeout=60)
+            self.assertEqual(result.returncode, 0, result.stderr)
+            self.assertIn('PASS_P104_AFFINE_PREMISES', result.stdout)
+            receipt = verify.load(package / 'RESULT.json')
+            receipt['endpoints'] = True
+            (package / 'RESULT.json').write_text(json.dumps(receipt))
+            result = subprocess.run(command, check=False, capture_output=True, text=True, timeout=60)
+            self.assertNotEqual(result.returncode, 0)
+            self.assertIn('typed receipt', result.stderr)
+            source = root / verify.INPUT / 'LOWRANK-WITNESS.json'
+            source.write_bytes(source.read_bytes() + b' ')
+            result = subprocess.run(command, check=False, capture_output=True, text=True, timeout=60)
+            self.assertNotEqual(result.returncode, 0)
+            self.assertIn('source hash', result.stderr)
+
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/research/p104-affine-complement-lean/verify.py b/research/p104-affine-complement-lean/verify.py
new file mode 100644
index 0000000000..132024e0fc
--- /dev/null
+++ b/research/p104-affine-complement-lean/verify.py
@@ -0,0 +1,183 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Reconstruct the finite P104 hypotheses of the separate Lean geometry lemma."""
+
+import argparse
+import hashlib
+import json
+from collections import Counter
+from itertools import combinations, product
+from pathlib import Path
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+INPUT = 'research/p104-native-channel/inputs/'
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def unique(pairs):
+    result = dict(pairs)
+    require(len(result) == len(pairs), 'duplicate JSON key')
+    return result
+
+
+def load(path):
+    require(path.stat().st_size <= 2_000_000, 'JSON size bound')
+    return json.loads(path.read_bytes(), object_pairs_hook=unique)
+
+
+def inputs():
+    manifest = load(PACKAGE / 'SOURCES.json')
+    rows = [row for row in manifest['files'] if row['usage'] == 'input']
+    require({row['path'] for row in rows} ==
+            {INPUT + 'LOWRANK-WITNESS.json', INPUT + 'P104-FIXTURE.json',
+             'formal/lean/lake-manifest.json', 'formal/lean/lakefile.toml',
+             'formal/lean/lean-toolchain'}, 'input paths')
+    require(len(rows) == 5, 'five input pins')
+    result = {}
+    for row in rows:
+        path = ROOT / row['path']
+        require(path.stat().st_size <= 2_000_000, 'source size bound')
+        data = path.read_bytes()
+        require(hashlib.sha256(data).hexdigest() == row['sha256'], 'source hash')
+        if row['path'].startswith(INPUT):
+            result[path.name] = json.loads(data, object_pairs_hook=unique)
+    return result['LOWRANK-WITNESS.json'], result['P104-FIXTURE.json']
+
+
+def span(basis):
+    require(len(basis) <= 9, 'basis size bound')
+    result = {0}
+    for value in basis:
+        require(type(value) is int and 0 < value < 512 and value not in result,
+                'independent binary basis')
+        result |= {value ^ old for old in tuple(result)}
+    return frozenset(result)
+
+
+def parity(a, b):
+    return (a & b).bit_count() % 2
+
+
+def rank(points):
+    require(len(points) <= 48 and all(type(v) is int and 0 < v < 512 for v in points),
+            'point count and bit-width bounds')
+    basis = [0] * 9
+    for point in points:
+        for bit in range(8, -1, -1):
+            if point & (1 << bit):
+                if basis[bit]:
+                    point ^= basis[bit]
+                else:
+                    basis[bit] = point
+                    break
+    return sum(bool(v) for v in basis)
+
+
+def geometry(witness, fixture):
+    roots = set()
+    for i, j in combinations(range(8), 2):
+        for sign in (-1, 1):
+            row = [0] * 8
+            row[i], row[j] = 2, 2 * sign
+            roots.add(tuple(row))
+    roots |= {(1, *s) for s in product((-1, 1), repeat=7) if s.count(-1) % 2 == 0}
+    puncture = fixture['section4_explicit_P104']
+    ports = sorted(roots - {tuple(v) for v in puncture['F0'] + puncture['C']})
+    require(len(roots) == 120 and len(ports) == 104, 'ordered P104 ports')
+    paths = {f'{k}{i}': [span(witness['initial_frames'][f'{k}{i}'])]
+             for k in 'XY' for i in range(104)}
+    require(len(witness['program']) == 4058, 'frozen event count')
+    for event in witness['program']:
+        if event[0] == 'transport' and event[1] in paths:
+            _, name, before, after, jump = event
+            require(paths[name][-1] == span(before) < span(after), 'monotone data path')
+            require(jump == len(after) - len(before), 'rank-gap binding')
+            paths[name].append(span(after))
+    for name in paths:
+        require(paths[name][-1] == span(witness['final_frames'][name]), 'final frame')
+    x, y = [paths[f'X{i}'] for i in range(104)], [paths[f'Y{i}'] for i in range(104)]
+    require(all(len(p[0]) == 2 and len(p[-1]) == 512 for p in x), 'source endpoints')
+    require(all(p[0] == {0} and len(p[-1]) == 256 for p in y), 'target endpoints')
+    labels = [next(iter(p[0] - {0})) for p in x]
+    normals = []
+    for p in y:
+        dual = [n for n in range(1, 512) if all(parity(n, v) == 0 for v in p[-1])]
+        require(len(dual) == 1, 'unique target normal')
+        normals.append(dual[0])
+    require(len(set(labels)) == len(set(normals)) == 104, 'distinct endpoints')
+    return ports, x, y, labels, normals
+
+
+def residuals(geo):
+    ports, x, y, labels, normals = geo
+    arrival, departure = [set() for _ in ports], [set() for _ in ports]
+    count = 0
+    for t in range(104):
+        for s in range(104):
+            gram = sum(a * b for a, b in zip(ports[t], ports[s], strict=True))
+            require((labels[s] in y[t][-1]) == (gram % 8 == 4), 'Gram/frame binding')
+            if gram == 8 * int(t == s):
+                continue
+            count += 1
+            require(y[t][-1] not in x[s] and x[s][0] not in y[t], 'no endpoint bypass')
+            if not any(labels[s] in frame for frame in y[t][:-1]):
+                arrival[t].add(labels[s])
+            if not any(len(frame) > 2 and frame <= y[t][-1] for frame in x[s]):
+                departure[s].add(normals[t])
+    require(count == 4992, 'correction demand count')
+    return [('arrival', arrival, normals), ('departure', departure, labels)]
+
+
+def check_cover(points, normal, q, f):
+    require(0 < normal < 512 and 0 < q < 512 and 0 < f < 512, 'form bounds')
+    require(len(points) <= 48 and rank(points) == 8, 'spanning demand set')
+    require(all(parity(v, normal) == 0 and parity(v, q) == 1 for v in points),
+            'endpoint and odd-section hypotheses')
+    endpoint = {v for v in range(512) if parity(v, normal) == 0}
+    left = {v for v in endpoint if parity(v, f) == 0}
+    right = {v for v in endpoint if parity(v, f ^ q) == 0}
+    require(0 < len(points & left) < len(points), 'nontrivial split')
+    require(len(left) == len(right) == 128, 'dimension-seven kernels')
+    require(not points & left & right and points <= left | right, 'exact disjoint cover')
+    return len(points & left), len(points & right)
+
+
+def calculate():
+    witness, fixture = inputs()
+    geo = geometry(witness, fixture)
+    covers, census = [], Counter()
+    for direction, rows, normals in residuals(geo):
+        require(sum(map(len, rows)) == 4656, 'residual total per orientation')
+        for i, (points, normal) in enumerate(zip(rows, normals, strict=True)):
+            odd = [q for q in range(1, 512) if all(parity(v, q) == 1 for v in points)]
+            require(bool(odd), 'odd section exists')
+            f = max((f for f in range(1, 512) if f != normal),
+                    key=lambda f: sum(parity(v, f) == 0 for v in points))
+            left, right = check_cover(points, normal, odd[0], f)
+            census[len(points), left, right] += 1
+            covers.append([direction, i, normal, odd[0], f, left, right])
+    require(len(covers) == 208, 'all endpoint hypotheses checked')
+    return {'endpoints': 208, 'residuals_per_orientation': 4656,
+            'census': [list(key) + [value] for key, value in sorted(census.items())],
+            'covers_sha256': hashlib.sha256(json.dumps(covers).encode()).hexdigest()}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--emit', action='store_true')
+    args = parser.parse_args()
+    result = calculate()
+    if not args.emit:
+        require(json.dumps(result, sort_keys=True) ==
+                json.dumps(load(PACKAGE / 'RESULT.json'), sort_keys=True), 'typed receipt')
+    print(json.dumps(result, sort_keys=True, indent=2))
+    print('PASS_P104_AFFINE_PREMISES endpoints=208 no_circuit_or_cost_claim')
+
+
+if __name__ == '__main__':
+    main()