Formalize the selected BIT split-residual retractions and conjugation interface

research/lean-split-residual/README.md

@@ -0,0 +1,140 @@
+# Kernel-checked split residual interface for selected BIT
+
+Jose Manuel's [PR2195](https://github.com/CrocSwap/integer-mult-bounds/pull/2195)
+proves the selected BIT local-ring integration conditionally on completed
+callees. Section 1 supplies an explicit split-rank factorization instead of
+inferring rank from trace modulo the prime. This package kernel-checks that
+algebraic implication and its conjugation behavior. The mathematical
+factorization retains PR2195 credit; the contribution is the formal boundary,
+not a new supplier or exponent.
+
+## Exact proposition
+
+Let A and M be additive commutative groups, represented by Lean's IntModule
+class. Let B:A->M, V:M->A and C:M->M preserve zero, addition and negation.
+Assume V(B(a))=a for every a. Put P=BV and define
+
+    D(x,y) = (x-Px+P(Cy), C(Px)+y-C(P(Cy))),
+    F(z) = D(z)-z,
+    U(a) = (-B(a), C(B(a))),
+    W(x,y) = V(x)-V(C(y)),
+    L(x,y) = -V(x),     R(a) = (B(a),0).
+
+SplitResidual.lean proves F=UW, LU=id and WR=id. It also proves that the
+image of F is exactly the image of U, and U is injective. Every residual
+image element therefore has a unique A coordinate. P is idempotent.
+With the additional hypothesis C(C(x))=x, D is involutory.
+
+For an invertible additive change of coordinates T, the formalized
+residual-conjugation identity is
+
+    T D T^-1 - id = T (D-id) T^-1.
+
+Transformed factors TU and WT^-1 have retractions LT^-1 and TR. This
+includes weight/chart changes once their additive bijections are supplied.
+No orthogonality or transpose-as-inverse assumption is used. The factorization
+and retractions do not require C^2=id; only D-involution uses that premise.
+No field, characteristic, trace or diagonalizability hypothesis enters the proof.
+
+## Formal/source correspondence
+
+| Lean roots | Exact meaning and assumptions |
+|---|---|
+| map_sub, factorization | Distribute the explicit additive maps through the residual |
+| left_inverse, right_inverse | The displayed retractions, using VB=id |
+| projection_idempotent | P=BV is idempotent |
+| image_iff, lifted_injective | Residual image is a uniquely coordinatized copy of A |
+| involution | D^2=id, additionally using C^2=id |
+| conjugate_factorization, conjugate_left_inverse, conjugate_right_inverse | Factorization and retractions survive an explicit two-sided bijection |
+| conjugate_residual | Actual conjugated operation minus identity equals conjugated residual, requiring subtraction preservation |
+| integer_example, integer_split_example | Concrete signed-swap instance over integers |
+
+For the source matrices take A=R^r and M=R^m over R=Z/q^w, B,V from the
+split image/kernel basis, and C the reversal. Source section 1 states VB=I
+and F=[-B;CB][V,-VC]. The formal formula is precisely this block formula
+evaluated on a pair, not a renamed conclusion supplied as a hypothesis.
+
+**Remaining external obligations:** construction and authentication of concrete
+B,V,C; their module instances and scalar linearity; the determinant-unit lift
+from residue-field bases; and a formal dimension/rank theorem. The kernel
+proves retractions and image correspondence, not a library assertion
+rank(F)=r. Mathematically, R-linear B,V,C and A=R^r identify the residual
+image with that free module. Finite fixtures corroborate this specialization
+without binding every selected frame in Lean.
+
+The selected word, profile, completed callees, physical hosting, row allocation,
+tape/precision and outer analytic transfer remain separate. Their assumptions
+are unchanged.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+    python3.12 scripts/research_package.py --package research/lean-split-residual
+    python3.12 -I -O -B research/lean-split-residual/verify.py --lean /absolute/path/to/lean
+
+Use Lean 4.34.1. The explicit --lean command recompiles all source in a fresh
+temporary directory with warnings treated as errors, then queries all fourteen
+roots and rejects axioms outside propext, Classical.choice and Quot.sound.
+It never accepts a saved compiler log as evidence. Four material theorem
+mutations must fail compilation. A genuinely compiled declaration depending
+on an injected axiom must be rejected by the audit.
+
+The registered Python hook runs finite fixtures and export controls.
+**It does not run Lean automatically.** The explicit live command was run
+during development on Windows with Lean 4.34.1 and CPython 3.12.14.
+RESULT.json binds the Lean source SHA-256, also reported by live verification.
+
+Default verification is read-only; --write explicitly replaces RESULT.json.
+Git-free exports need this package and the declared PROOF.md input at their
+repository-relative paths. The generic runner additionally audits historical
+task/source provenance.
+
+## Evidence and controls
+
+The 252 exact modular matrix cases cover m=1..6, every positive r<=m,
+three basis charts, primes 3/5 and widths 1/2. They check VB=I, P^2=P,
+F=UW, LU=I, WR=I, D^2=I, residue ranks and conjugated identities.
+**42 cases have positive rank but zero trace modulo the prime.**
+Unit-pivot inversion and separate residue-field elimination use exact integers.
+
+Five controls cover a missing lift sign, absent retraction premise,
+transpose-as-inverse, absent C-involution premise, and the rank-zero boundary.
+The last is a positive identity boundary, not a rejected counterexample.
+The four live Lean mutations change/remove the lift sign, VB hypothesis,
+right section and C^2 hypothesis. Git-free CLI tests reject source and
+Lean-byte corruption and Boolean/float receipt substitutions, and verify
+read-only success. All Python checks remain active under -O.
+
+The source's 636 frames and 531 residuals are not rerun here. These small-ring
+controls do not replace its geometry checks. No selected cold replay, hosted
+CI, human review, Mathlib matrix theorem or full multiplication theorem is claimed.
+
+## Provenance and overlap
+
+Scientific base 21ec98bfd2e9f27810a8718d95d9b5d19a5df7d7, priority 5;
+picker nonce dba52022fd62ead90880b092efd7d755. The prescribed binding baseline
+passed. SOURCES.json pins the exact retained source proof, catalogue and
+selected record. Original PR2195 head:
+3a1cf78a1ba6322129e42d80c50d21765524d612, Jose Manuel (jmbarrancoml).
+
+The card was narrowed to this boundary after reading the already formal HPE
+wrapper/label proofs. Local Lean and merged notes, open PRs and targeted
+REST queries showed no exact existing kernel treatment. TASK.json records
+coverage limits, including the stale Discussion snapshot; no search proves
+novelty or exhausts diffs. Claim: PR2195 comment 6199233287.
+
+Retain PR2195's credits to alephnan PR1627, eumemic PR490/source527,
+DreamingOfClouds PR589 and the selected construction lineage. The small live
+axiom-audit pattern follows our PR2618 verifier; no new audit framework is
+claimed. Prepared for ywz65 with substantial OpenAI Codex assistance.
+Apache-2.0.
+
+## Open next questions
+
+1. Bind one actual selected rank-divisible-by-prime frame to the kernel.
+   Begin with finite-ring B,V,C literals and VB=I; concrete representation
+   and authenticated translation remain missing.
+2. Connect the image correspondence to a free-module dimension API and
+   formalize the determinant-unit basis lift. The rank-library bridge
+   remains external to the present proof.

research/lean-split-residual/RESULT.json

@@ -0,0 +1,8 @@
+{
+  "status": "PASS_SPLIT_RESIDUAL_CONTROLS",
+  "formal_sha256": "bb1beefee02cdf17004df49ffa75fe043e9057b896e21b9074b28e26b0d60177",
+  "ring_cases": 252,
+  "positive_trace_zero_cases": 42,
+  "conjugated_cases": 252,
+  "controls": 5
+}

research/lean-split-residual/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "21ec98bfd2e9f27810a8718d95d9b5d19a5df7d7",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "889b95d936746df124872133ae1e7cc339adcb92",
+      "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6"
+    },
+    {
+      "path": "research/selected-bit-local-ring-sweeps/PROOF.md",
+      "usage": "input",
+      "git_blob": "4330de85dd9862ed15d84ab917887d249753df99",
+      "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7"
+    }
+  ]
+}

research/lean-split-residual/SplitResidual.lean

@@ -0,0 +1,119 @@
+import Std
+set_option maxHeartbeats 4000000
+namespace SplitResidual
+open Lean.Grind
+variable {A M : Type} [IntModule A] [IntModule M]
+
+structure AddMap (X Y : Type) [IntModule X] [IntModule Y] where
+  apply : X → Y
+  zero : apply 0 = 0
+  add : ∀ x y, apply (x+y) = apply x + apply y
+  neg : ∀ x, apply (-x) = -apply x
+
+theorem map_sub (f : AddMap A M) (x y : A) :
+    f.apply (x-y) = f.apply x - f.apply y := by
+  simp only [AddCommGroup.sub_eq_add_neg, f.add, f.neg]
+
+def proj (B : AddMap A M) (V : AddMap M A) (x : M) := B.apply (V.apply x)
+def lifted (B : AddMap A M) (C : AddMap M M) (a : A) : M × M :=
+  (-B.apply a, C.apply (B.apply a))
+def lowered (V : AddMap M A) (C : AddMap M M) (z : M × M) : A :=
+  V.apply z.1 - V.apply (C.apply z.2)
+def undoLift (V : AddMap M A) (z : M × M) : A := -V.apply z.1
+def embed (B : AddMap A M) (a : A) : M × M := (B.apply a, 0)
+def d (B : AddMap A M) (V : AddMap M A) (C : AddMap M M) (z : M × M) : M × M :=
+  (z.1 - proj B V z.1 + proj B V (C.apply z.2),
+   C.apply (proj B V z.1) + z.2 - C.apply (proj B V (C.apply z.2)))
+def residual (B : AddMap A M) (V : AddMap M A) (C : AddMap M M) (z : M × M) : M × M :=
+  ((d B V C z).1-z.1, (d B V C z).2-z.2)
+
+theorem factorization (B : AddMap A M) (V : AddMap M A) (C : AddMap M M) (z : M × M) :
+    residual B V C z = lifted B C (lowered V C z) := by
+  apply Prod.ext
+  · simp only [residual,d,proj,lifted,lowered,map_sub]
+    grind
+  · simp only [residual,d,proj,lifted,lowered,map_sub]
+    grind
+
+theorem left_inverse (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (a : A) :
+    undoLift V (lifted B C a) = a := by
+  simp only [undoLift,lifted,V.neg,hVB]
+  grind
+
+theorem right_inverse (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (a : A) :
+    lowered V C (embed B a) = a := by
+  simp only [lowered,embed,C.zero,V.zero,hVB]
+  grind
+
+theorem projection_idempotent (B : AddMap A M) (V : AddMap M A)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (x : M) :
+    proj B V (proj B V x) = proj B V x := by
+  simp only [proj,hVB]
+
+theorem image_iff (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (z : M × M) :
+    (∃ x, residual B V C x = z) ↔ (∃ a, lifted B C a = z) := by
+  constructor
+  · rintro ⟨x,hx⟩
+    exact ⟨lowered V C x, (factorization B V C x).symm.trans hx⟩
+  · rintro ⟨a,ha⟩
+    refine ⟨embed B a, ?_⟩
+    rw [factorization,right_inverse B V C hVB,ha]
+
+theorem lifted_injective (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) {a b : A}
+    (h : lifted B C a = lifted B C b) : a = b := by
+  have h' := congrArg (undoLift V) h
+  simpa only [left_inverse B V C hVB] using h'
+theorem involution (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a)
+    (hCC : ∀ x, C.apply (C.apply x) = x) (z : M × M) :
+    d B V C (d B V C z) = z := by
+  apply Prod.ext <;>
+    simp only [d,proj,map_sub,B.add,V.add,C.add,hVB,hCC] <;> grind
+
+structure Bijection (X : Type) where
+  forward : X → X
+  backward : X → X
+  back_forward : ∀ x, backward (forward x) = x
+  forward_back : ∀ x, forward (backward x) = x
+
+theorem conjugate_factorization {X Y : Type} (F : X → X) (U : Y → X)
+    (W : X → Y) (h : ∀ x, F x = U (W x)) (T : Bijection X) (x : X) :
+    T.forward (F (T.backward x)) = T.forward (U (W (T.backward x))) := by
+  rw [h]
+
+theorem conjugate_left_inverse {X Y : Type} (U : Y → X) (L : X → Y)
+    (h : ∀ y, L (U y) = y) (T : Bijection X) (y : Y) :
+    L (T.backward (T.forward (U y))) = y := by
+  rw [T.back_forward,h]
+
+theorem conjugate_right_inverse {X Y : Type} (W : X → Y) (R : Y → X)
+    (h : ∀ y, W (R y) = y) (T : Bijection X) (y : Y) :
+    W (T.backward (T.forward (R y))) = y := by
+  rw [T.back_forward,h]
+
+theorem conjugate_residual {X : Type} [IntModule X] (F : X → X)
+    (T : Bijection X) (hsub : ∀ x y, T.forward (x-y) = T.forward x - T.forward y)
+    (x : X) :
+    T.forward (F (T.backward x)) - x =
+      T.forward (F (T.backward x) - T.backward x) := by
+  rw [hsub,T.forward_back]
+
+def intIdentity : AddMap Int Int := ⟨id, rfl, by intros; rfl, by intros; rfl⟩
+def intNegative : AddMap Int Int := ⟨fun x => -x, by decide,
+  by intros; grind, by intros; rfl⟩
+
+theorem integer_example (x y : Int) :
+    d intIdentity intIdentity intNegative (x,y) = (-y,-x) := by
+  apply Prod.ext <;> simp only [d,proj,intIdentity,intNegative,id] <;> grind
+
+theorem integer_split_example (a : Int) :
+    undoLift intIdentity (lifted intIdentity intNegative a) = a ∧
+    lowered intIdentity intNegative (embed intIdentity a) = a := by
+  constructor
+  · exact left_inverse intIdentity intIdentity intNegative (fun _ => rfl) a
+  · exact right_inverse intIdentity intIdentity intNegative (fun _ => rfl) a
+end SplitResidual

research/lean-split-residual/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 5,
+  "base_commit": "21ec98bfd2e9f27810a8718d95d9b5d19a5df7d7",
+  "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": "Kernel-check PR2195 section1's split residual factorization, explicit retractions and image correspondence, involution, and additive conjugation invariance.",
+  "scope_change_reason": "HPE wrappers already have proofs; the newer selected BIT local-ring argument states this split residual bridge only in prose and finite checks. The factorization remains credited, not a new mathematical theorem.",
+  "bottleneck_link": "Makes the ring-safe width argument inspectable without trace-as-rank, retaining concrete free-basis construction and supplier cost as external obligations.",
+  "budget_minutes": 60,
+  "stop_rule": "Formalize this factorization interface, run live kernel/axiom/mutation controls and exact ring fixtures, then stop.",
+  "outcome": "completed",
+  "evidence": "SplitResidual.lean, README.md, RESULT.json, verify.py --lean live audit and test_cli.py Git-free controls.",
+  "author": "ywz65",
+  "ai_assistance": "Substantial OpenAI Codex assistance in formalization, testing, source and overlap analysis, and writing.",
+  "open_questions": [
+    {
+      "question": "Can selected finite image/kernel bases become kernel-checked instances of these retractions?",
+      "why_it_matters": "The abstract proof does not authenticate or construct the selected 636 frame bases.",
+      "first_step": "Bind one rank-divisible-by-prime frame's B,V,C and verify VB=I in a concrete finite-ring module.",
+      "blocked_by": "A concrete representation and source-to-kernel translation."
+    },
+    {
+      "question": "Can the free-module rank conclusion and lifted local-ring basis construction be formalized?",
+      "why_it_matters": "This proves retractions and image correspondence, not a library dimension theorem.",
+      "first_step": "Connect lifted_injective and image_iff to a free-module dimension API.",
+      "blocked_by": "A compatible algebra library and formal invertibility of the chosen image/kernel basis."
+    }
+  ],
+  "nonce": "dba52022fd62ead90880b092efd7d755",
+  "source_credit": {
+    "pr": 2195,
+    "head": "3a1cf78a1ba6322129e42d80c50d21765524d612",
+    "author": "Jose Manuel (jmbarrancoml)",
+    "path": "research/selected-bit-local-ring-sweeps/PROOF.md",
+    "section": "1"
+  },
+  "overlap": {
+    "open_prs": "767 records, complete snapshot 2026-10-15T18:06:42Z",
+    "discussions": "1239 records, complete snapshot 2026-10-15T15:22:22Z; stale at submission",
+    "additional": "Local Lean/source/merged-note search and targeted REST 2195/Lean, split-rank/Lean and residual-factorization/Lean queries; no exhaustive code-diff search."
+  },
+  "upstream_checkpoint": {
+    "commit": "ab4fcd39c74effa88d464ed1d80ec832f6020e51",
+    "guidance": "unchanged; fast-forwarded before publication; scientific pins21ec98 retained"
+  }
+}