Formalize the overcomplete rank and one-extra coupling interface

research/overcomplete-rank-interface/Coupling.lean

@@ -0,0 +1,164 @@
+import Mathlib.LinearAlgebra.Matrix.Rank
+import Mathlib.LinearAlgebra.FiniteDimensional.Basic
+
+/-
+SPDX-License-Identifier: Apache-2.0
+The rank conclusions of DreamingOfClouds's Lemma OC (PR2277), formalized
+for ywz65 with OpenAI Codex assistance. No geometric cost theorem is claimed.
+-/
+open Matrix Module
+set_option linter.unusedSectionVars false
+
+namespace OvercompleteRank
+variable {K T M : Type*} [Field K] [Fintype T] [Fintype M]
+  [DecidableEq T] [DecidableEq M]
+
+theorem cross_idempotent (X Y : Matrix T M K) (h : X * Y.transpose = 1) :
+    (Y.transpose * X) * (Y.transpose * X) = Y.transpose * X := by
+  calc
+    _ = Y.transpose * (X * Y.transpose) * X := by simp only [Matrix.mul_assoc]
+    _ = _ := by rw [h, Matrix.mul_one]
+
+theorem factor_rank (X Y : Matrix T M K) (h : X * Y.transpose = 1) :
+    X.rank = Fintype.card T := by
+  apply le_antisymm
+  · rw [← Matrix.rank_transpose]
+    exact Matrix.rank_le_card_width _
+  · have hh := Matrix.rank_mul_le_left X Y.transpose
+    simpa only [h, Matrix.rank_one] using hh
+
+theorem cross_rank (X Y : Matrix T M K) (h : X * Y.transpose = 1) :
+    (Y.transpose * X).rank = Fintype.card T := by
+  have hX := factor_rank X Y h
+  have hx : X * (Y.transpose * X) = X := by rw [← Matrix.mul_assoc, h, Matrix.one_mul]
+  apply le_antisymm
+  · simpa only [hX] using Matrix.rank_mul_le_right Y.transpose X
+  · have hh := Matrix.rank_mul_le_right X (Y.transpose * X)
+    simpa only [hx, hX] using hh
+
+theorem rank_add_le (A B : Matrix M M K) : (A + B).rank ≤ A.rank + B.rank := by
+  rw [Matrix.rank, Matrix.mulVecLin_add]
+  exact (Submodule.finrank_mono (LinearMap.range_add_le A.mulVecLin B.mulVecLin)).trans
+    (Submodule.finrank_add_le_finrank_add_finrank _ _)
+
+theorem complement_rank (X Y : Matrix T M K) (h : X * Y.transpose = 1) :
+    (1 - Y.transpose * X).rank = Fintype.card M - Fintype.card T := by
+  have hc := cross_rank X Y h
+  have hz : (Y.transpose * X) * (1 - Y.transpose * X) = 0 := by
+    rw [Matrix.mul_sub, Matrix.mul_one, cross_idempotent X Y h, sub_self]
+  have hu := Matrix.rank_add_rank_le_card_of_mul_eq_zero hz
+  have hl := rank_add_le (Y.transpose * X) (1 - Y.transpose * X)
+  have hs : Y.transpose * X + (1 - Y.transpose * X) = 1 := by abel
+  rw [hs, Matrix.rank_one, hc] at hl
+  rw [hc] at hu
+  omega
+
+theorem one_extra_rank (X Y : Matrix T M K) (h : X * Y.transpose = 1)
+    (hm : Fintype.card M = Fintype.card T + 1) :
+    (1 - Y.transpose * X).rank = 1 := by
+  rw [complement_rank X Y h, hm]
+  omega
+
+theorem rank_one_factorization (A : Matrix M M K) (hr : A.rank = 1) :
+    ∃ a b : M → K, A = Matrix.vecMulVec a b ∧ a ≠ 0 ∧ b ≠ 0 := by
+  classical
+  have hn : A ≠ 0 := by
+    intro hz
+    rw [hz, Matrix.rank_zero] at hr
+    omega
+  have hex : ∃ j, A.col j ≠ 0 := by
+    by_contra h
+    push Not at h
+    apply hn
+    ext i j
+    exact congrFun (h j) i
+  obtain ⟨j, hj⟩ := hex
+  let S := Submodule.span K (Set.range A.col)
+  have hs : Module.finrank K S = 1 := by
+    simpa only [Matrix.rank_eq_finrank_span_cols] using hr
+  have hm (k : M) : A.col k ∈ S := Submodule.subset_span ⟨k, rfl⟩
+  let a : S := ⟨A.col j, hm j⟩
+  have ha : a ≠ 0 := by
+    intro h
+    apply hj
+    exact congrArg Subtype.val h
+  have hc (k : M) : ∃ c : K, c • a = (⟨A.col k, hm k⟩ : S) :=
+    exists_smul_eq_of_finrank_eq_one hs ha _
+  choose b hb using hc
+  have hf : A = Matrix.vecMulVec (A.col j) b := by
+    ext i k
+    have hi := congrFun (congrArg Subtype.val (hb k)) i
+    simpa only [a, Submodule.coe_smul, Pi.smul_apply, smul_eq_mul,
+      Matrix.col_apply, Matrix.vecMulVec_apply, mul_comm] using hi.symm
+  refine ⟨A.col j, b, hf, hj, ?_⟩
+  intro hz
+  apply hn
+  rw [hf, hz]
+  ext i k
+  simp
+
+theorem complement_idempotent (X Y : Matrix T M K) (h : X * Y.transpose = 1) :
+    (1 - Y.transpose * X) * (1 - Y.transpose * X) = 1 - Y.transpose * X := by
+  simp only [Matrix.sub_mul, Matrix.mul_sub, Matrix.one_mul,
+    Matrix.mul_one, cross_idempotent X Y h]
+  abel
+
+theorem outer_idempotent_normalized (a b : M → K) (ha : a ≠ 0) (hb : b ≠ 0)
+    (h : Matrix.vecMulVec a b * Matrix.vecMulVec a b = Matrix.vecMulVec a b) :
+    dotProduct b a = 1 := by
+  classical
+  have hai : ∃ i, a i ≠ 0 := by
+    by_contra hh
+    push Not at hh
+    exact ha (funext hh)
+  have hbj : ∃ j, b j ≠ 0 := by
+    by_contra hh
+    push Not at hh
+    exact hb (funext hh)
+  obtain ⟨i, hi⟩ := hai
+  obtain ⟨j, hj⟩ := hbj
+  rw [Matrix.vecMulVec_mul_vecMulVec] at h
+  have he := congrArg (fun A : Matrix M M K => A i j) h
+  simp only [Matrix.vecMulVec_apply, Pi.smul_apply, smul_eq_mul] at he
+  apply mul_right_cancel₀ (mul_ne_zero hi hj)
+  calc
+    dotProduct b a * (a i * b j) = a i * (dotProduct b a * b j) := by ring
+    _ = a i * b j := he
+    _ = 1 * (a i * b j) := by ring
+
+theorem one_extra_factorization (X Y : Matrix T M K) (h : X * Y.transpose = 1)
+    (hm : Fintype.card M = Fintype.card T + 1) :
+    ∃ a b : M → K, 1 - Y.transpose * X = Matrix.vecMulVec a b ∧
+      dotProduct b a = 1 := by
+  obtain ⟨a, b, hf, ha, hb⟩ := rank_one_factorization _ (one_extra_rank X Y h hm)
+  refine ⟨a, b, hf, outer_idempotent_normalized a b ha hb ?_⟩
+  rw [← hf]
+  exact complement_idempotent X Y h
+
+theorem one_extra_entries (X Y : Matrix T M K) (h : X * Y.transpose = 1)
+    (hm : Fintype.card M = Fintype.card T + 1) :
+    ∃ a b : M → K, dotProduct b a = 1 ∧
+      (∀ i j, i ≠ j → (Y.transpose * X) i j = -(a i * b j)) ∧
+      (∀ i, (Y.transpose * X) i i = 1 - a i * b i) := by
+  obtain ⟨a, b, hf, hn⟩ := one_extra_factorization X Y h hm
+  refine ⟨a, b, hn, ?_, ?_⟩
+  · intro i j hij
+    have he := congrArg (fun A : Matrix M M K => A i j) hf
+    simp only [Matrix.sub_apply, Matrix.one_apply_ne hij,
+      Matrix.vecMulVec_apply, zero_sub] at he
+    exact neg_eq_iff_eq_neg.mp he
+  · intro i
+    have he := congrArg (fun A : Matrix M M K => A i i) hf
+    simp only [Matrix.sub_apply, Matrix.one_apply_eq, Matrix.vecMulVec_apply] at he
+    calc
+      (Y.transpose * X) i i = 1 - (1 - (Y.transpose * X) i i) := by abel
+      _ = 1 - a i * b i := by rw [he]
+
+#print axioms factor_rank
+#print axioms cross_rank
+#print axioms complement_rank
+#print axioms rank_one_factorization
+#print axioms one_extra_factorization
+#print axioms one_extra_entries
+
+end OvercompleteRank

research/overcomplete-rank-interface/DEPENDENCY.json

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2277",
+  "head": "ca7f99921f03398d303bba90245d3ee2e38e95c3",
+  "author": "DreamingOfClouds",
+  "files": [
+    {
+      "path": "research/overcomplete-and-realisation-floors/README.md",
+      "retained": "vendor/pr2277/README.md",
+      "git_blob": "02660b10d4f48cd39db3416def50cd944aef4ac9",
+      "sha256": "1a11f33a8d358479cae0f39018fa9ebd3d439790cd1872de91d109fd4d23a088"
+    },
+    {
+      "path": "research/overcomplete-and-realisation-floors/lean/Overcomplete.lean",
+      "retained": "vendor/pr2277/lean/Overcomplete.lean",
+      "git_blob": "58d9d97a9228d60edcef18a635f949a3a3713118",
+      "sha256": "06ed7a0c208e328bfdbc34609ed851085dd8832ee9b38e8e5b5790dfae96f0cd"
+    },
+    {
+      "path": "research/overcomplete-and-realisation-floors/lean/lake-manifest.json",
+      "retained": "vendor/pr2277/lean/lake-manifest.json",
+      "git_blob": "94973914f6f3e54695bab1ab1583b1caa5ec0c7e",
+      "sha256": "1f62920310807cf74bb08e834265e7e2281eac76650ea6026cdc676e516652b7"
+    },
+    {
+      "path": "research/overcomplete-and-realisation-floors/lean/lakefile.toml",
+      "retained": "vendor/pr2277/lean/lakefile.toml",
+      "git_blob": "ae1ee720f16f50dfc43bc9620201e9e31fb9c537",
+      "sha256": "6d1584fba35d26bb56eb4b4e756b41caa4299d544b69bc937dc00fd8bc8791b1"
+    },
+    {
+      "path": "research/overcomplete-and-realisation-floors/lean/lean-toolchain",
+      "retained": "vendor/pr2277/lean/lean-toolchain",
+      "git_blob": "fd85b262bf1c734663aa8292b0101f672168788f",
+      "sha256": "62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef"
+    }
+  ]
+}

research/overcomplete-rank-interface/FORMAL-RESULT.json

@@ -0,0 +1,27 @@
+{
+  "schema_version": 1,
+  "status": "kernel-checked",
+  "source_sha256": "afb7bc4da2c9cc1e9ec42172dfa54b003cfd78bb18500f9c30686c3993e47ec0",
+  "lean_version": "4.33.0-rc1",
+  "lean_commit": "62eed1db4d67327ec8120be05f1a1b0847d74561",
+  "mathlib_commit": "55b7917b472489c7c56a0fa6393af05cfd536599",
+  "audited_roots": [
+    "factor_rank",
+    "cross_rank",
+    "complement_rank",
+    "rank_one_factorization",
+    "one_extra_factorization",
+    "one_extra_entries"
+  ],
+  "allowed_axioms": [
+    "propext",
+    "Classical.choice",
+    "Quot.sound"
+  ],
+  "rejected_contract_mutants": [
+    "cross rank replaced by ambient size",
+    "exactness replaced by zero product",
+    "two extra columns called rank one",
+    "normalization changed to zero"
+  ]
+}

research/overcomplete-rank-interface/README.md

@@ -0,0 +1,130 @@
+# Kernel-checked rank interface for overcomplete coupling
+
+PR2277's Lemma OC already proves in prose that an exact factorization
+`X Yᵀ = I_T` makes `K = Yᵀ X` a rank-T idempotent, with complement rank
+`m−T`. Its shipped Lean file formalizes idempotency, traces and the square
+case, and explicitly leaves the rank statements and one-extra consequence
+as written proofs. This package completes those **forward formal obligations**.
+It does not claim a new mathematical rank theorem or a new decoder cost floor.
+
+`Coupling.lean` proves, over **every field**, for arbitrary finite index types:
+
+* `rank X = rank K = T`;
+* `rank(I_m−K) = m−T`;
+* if `m=T+1`, there are vectors `a,b` with `I_m−K = a bᵀ` and `bᵀa=1`;
+* consequently `K_ij = −a_i b_j` for `i≠j`, and `K_ii=1−a_i b_i`.
+
+The size difference is a natural-number difference. Exactness itself forces
+`T≤m`. Empty finite types are allowed by the general theorems; the one-extra
+premise forces the complement to be nonzero. No positivity, characteristic
+zero, symmetry, root-system classification, finite search or rank conclusion
+is assumed in a theorem hypothesis.
+
+## Proof structure
+
+The product `XYᵀ=I` and the matrix rank inequalities force `rank X=T`.
+Next `XK=X` gives the lower bound for `rank K`, while `K=YᵀX` gives the upper
+bound. This avoids using trace to infer rank: over F2, the three-dimensional
+identity has trace one and rank three.
+
+Idempotency gives `K(I−K)=0`, so their ranks sum to at most m. The matrix
+rank subadditivity inequality and `K+(I−K)=I` give the reverse inequality.
+Natural-number arithmetic then gives the stated complement rank.
+
+For a rank-one matrix, the proof chooses a nonzero actual column. Its column
+space has dimension one, so every column is a scalar multiple of that column.
+This yields an outer product with two nonzero factors. Applying idempotency
+to a nonzero entry and cancelling that entry proves `bᵀa=1`. The two entry
+formulas follow directly from `I−K=a bᵀ`.
+
+The proof reuses the elementary idempotency calculation from the credited
+source, and Mathlib's established rank and finite-dimensional APIs. Six final
+roots are printed with `#print axioms`; each depends only on `propext`,
+`Classical.choice` and `Quot.sound`. There is no `sorry`, custom axiom,
+native-decision axiom or finite fixture assumed by a theorem.
+
+## Reproduce the formal result
+
+The predecessor pins Lean **4.33.0-rc1**, commit
+`62eed1db4d67327ec8120be05f1a1b0847d74561`, and Mathlib commit
+`55b7917b472489c7c56a0fa6393af05cfd536599`. `TOOLCHAIN.json` also records
+the dependency-manifest hash and the official Windows release archive's
+SHA256, checked before the local run. Install that Lean release in a local
+directory, then prepare a separate Mathlib checkout:
+
+```sh
+git clone https://github.com/leanprover-community/mathlib4.git /path/to/mathlib4
+git -C /path/to/mathlib4 checkout 55b7917b472489c7c56a0fa6393af05cfd536599
+# With the pinned Lean bin directory on PATH, in /path/to/mathlib4:
+lake exe cache get Mathlib.LinearAlgebra.Matrix.Rank Mathlib.LinearAlgebra.FiniteDimensional.Basic
+# Back in this repository:
+python3.12 -I -B research/overcomplete-rank-interface/leancheck.py \
+  --mathlib-root /path/to/mathlib4 --lean-bin /path/to/pinned-lean/bin
+```
+
+The checker verifies compiler version/commit, Mathlib HEAD, tracked source
+cleanliness and the exact dependency manifest. It compiles a temporary copy
+without writing generated files into this package or changing Mathlib.
+It audits all six roots and rejects four altered contracts: ambient size
+instead of T, zero product instead of exactness, two extra columns instead
+of one, and normalization zero instead of one. A missing toolchain is an
+error, not a skipped formal pass. `--out NEW.json` writes a new recomputed
+receipt and refuses an existing path. Normal replay compares the retained
+`FORMAL-RESULT.json`.
+
+As with a standard Mathlib build, the compiler and imported library artifacts
+are trusted dependencies. The checker is not a hermetic rebuild or an audit
+of the entire Mathlib library. No hosted CI formal run is claimed.
+
+## Separate finite and export evidence
+
+```sh
+python3.12 -I -B scripts/research_package.py --package research/overcomplete-rank-interface
+```
+
+This registered Python replay is intentionally **separate from Lean**. It
+authenticates the retained predecessor and formal-source receipt, then checks
+448 exact factorization fixtures over Q, F2, F3 and F5, with T from one to four
+and zero through three extra columns. The 112 one-extra cases independently
+recover an outer product from a pivot and check its normalization and entries.
+Four semantic controls include trace-one/rank-three in F2, failed exactness,
+the two-extra boundary and a nonsymmetric idempotent positive control.
+Git-free optimized export checks exercise read-only replay, predecessor and
+formal-source corruption rejection, and refusal to overwrite a receipt.
+These finite checks illustrate and test the interface; they do not prove its
+universal quantifiers or rerun the source's root-code tables.
+
+## Provenance, binding and decision
+
+The exact source is DreamingOfClouds's
+[PR2277](https://github.com/CrocSwap/integer-mult-bounds/pull/2277), head
+`ca7f99921f03398d303bba90245d3ee2e38e95c3`, README section 4 (Lemma OC and
+consequence b). `DEPENDENCY.json` records Git blob IDs and SHA256 hashes for
+the unchanged README, original Lean file and three environment files. The
+notation is direct: source X,Y and cross matrix `YᵀX` have the same matrix
+dimensions and orientation in this package. The formal theorem requires
+exactly the source's `XYᵀ=I`; no source geometric calculation is imported.
+All source credit is retained. This package's new proof and replay code were
+prepared for ywz65 with substantial OpenAI Codex assistance, Apache-2.0.
+
+The task picker selected the P104 card, nonce
+`ad89b619e94d237299b77316f1d1a534`; the baseline orientation passed. Adjacent
+ceiling domain defects were handed to a single separate repair. This scope
+instead closes an expressly unformalized decoder-coupling obligation.
+`TASK.json` records the change. Main provenance is pinned to `1884c509`;
+pending source provenance is pinned independently to the PR head above.
+
+The decision is **finish this bounded formal audit**. It constructs no new
+physical family. Native access, copy/hosting, restoration, precision and
+consumer costs are not evaluated and remain unknown for any proposed use;
+they are not assigned zero. No new supplier, kappa bound or all-size integer
+multiplication result follows. The converse, prescribed-direction criterion,
+geometric floor tables and source SAT claims are outside this proof.
+
+## Open next questions
+
+Formalize the converse of Lemma OC by cancelling the full-rank rectangular
+factors, then its prescribed-direction criterion. Those are separate written
+obligations in the source. A later root-code application must also bind its
+finite geometric tables and cost model to the exact formal hypotheses; the
+present generic algebra theorem supplies no such table or physical bridge.

research/overcomplete-rank-interface/RESULT.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "exact_fixtures": 448,
+  "one_extra_fixtures": 112,
+  "fields": [
+    "Q",
+    "F2",
+    "F3",
+    "F5"
+  ],
+  "dimensions": [
+    1,
+    2,
+    3,
+    4
+  ],
+  "excess_columns": [
+    0,
+    1,
+    2,
+    3
+  ],
+  "semantic_controls": 4,
+  "scope": "finite checks and retained formal receipt; Lean replay is separate"
+}