From 41f977bd4c2090d8bb159c77257ac307a4bf5c00 Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 10:37:31 -0700 Subject: [PATCH] Formalize overcomplete rank and one-extra coupling --- .../overcomplete-rank-interface/Coupling.lean | 164 +++++++++++++++ .../DEPENDENCY.json | 38 ++++ .../FORMAL-RESULT.json | 27 +++ .../overcomplete-rank-interface/README.md | 130 ++++++++++++ .../overcomplete-rank-interface/RESULT.json | 25 +++ .../overcomplete-rank-interface/SOURCES.json | 24 +++ .../overcomplete-rank-interface/TASK.json | 73 +++++++ .../TOOLCHAIN.json | 9 + .../overcomplete-rank-interface/VERIFY.json | 29 +++ .../exportchecks.py | 51 +++++ .../overcomplete-rank-interface/leancheck.py | 105 ++++++++++ .../vendor/pr2277/README.md | 190 ++++++++++++++++++ .../vendor/pr2277/lean/Overcomplete.lean | 46 +++++ .../vendor/pr2277/lean/lake-manifest.json | 117 +++++++++++ .../vendor/pr2277/lean/lakefile.toml | 9 + .../vendor/pr2277/lean/lean-toolchain | 1 + .../overcomplete-rank-interface/verify.py | 131 ++++++++++++ 17 files changed, 1169 insertions(+) create mode 100644 research/overcomplete-rank-interface/Coupling.lean create mode 100644 research/overcomplete-rank-interface/DEPENDENCY.json create mode 100644 research/overcomplete-rank-interface/FORMAL-RESULT.json create mode 100644 research/overcomplete-rank-interface/README.md create mode 100644 research/overcomplete-rank-interface/RESULT.json create mode 100644 research/overcomplete-rank-interface/SOURCES.json create mode 100644 research/overcomplete-rank-interface/TASK.json create mode 100644 research/overcomplete-rank-interface/TOOLCHAIN.json create mode 100644 research/overcomplete-rank-interface/VERIFY.json create mode 100644 research/overcomplete-rank-interface/exportchecks.py create mode 100644 research/overcomplete-rank-interface/leancheck.py create mode 100644 research/overcomplete-rank-interface/vendor/pr2277/README.md create mode 100644 research/overcomplete-rank-interface/vendor/pr2277/lean/Overcomplete.lean create mode 100644 research/overcomplete-rank-interface/vendor/pr2277/lean/lake-manifest.json create mode 100644 research/overcomplete-rank-interface/vendor/pr2277/lean/lakefile.toml create mode 100644 research/overcomplete-rank-interface/vendor/pr2277/lean/lean-toolchain create mode 100644 research/overcomplete-rank-interface/verify.py diff --git a/research/overcomplete-rank-interface/Coupling.lean b/research/overcomplete-rank-interface/Coupling.lean new file mode 100644 index 0000000000..f701a4340b --- /dev/null +++ b/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 diff --git a/research/overcomplete-rank-interface/DEPENDENCY.json b/research/overcomplete-rank-interface/DEPENDENCY.json new file mode 100644 index 0000000000..aaa2842d10 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/overcomplete-rank-interface/FORMAL-RESULT.json b/research/overcomplete-rank-interface/FORMAL-RESULT.json new file mode 100644 index 0000000000..1656e2388e --- /dev/null +++ b/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" + ] +} diff --git a/research/overcomplete-rank-interface/README.md b/research/overcomplete-rank-interface/README.md new file mode 100644 index 0000000000..bb2408ed80 --- /dev/null +++ b/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. diff --git a/research/overcomplete-rank-interface/RESULT.json b/research/overcomplete-rank-interface/RESULT.json new file mode 100644 index 0000000000..0cecbc49ce --- /dev/null +++ b/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" +} diff --git a/research/overcomplete-rank-interface/SOURCES.json b/research/overcomplete-rank-interface/SOURCES.json new file mode 100644 index 0000000000..ede40272c4 --- /dev/null +++ b/research/overcomplete-rank-interface/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "1884c509efc004524786e9b7cfcc4aca572316d5", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "git_blob": "1a2195004c5d681679279f0095b7964fb14a01e6", + "sha256": "c37c7e0f6a1134983990e1b3efef55e65239b38be780e8a4cc10f5aefdaf2df5" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + ] +} diff --git a/research/overcomplete-rank-interface/TASK.json b/research/overcomplete-rank-interface/TASK.json new file mode 100644 index 0000000000..c7904facbe --- /dev/null +++ b/research/overcomplete-rank-interface/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 5, + "base_commit": "1884c509efc004524786e9b7cfcc4aca572316d5", + "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" + ] + }, + "picker_nonce": "ad89b619e94d237299b77316f1d1a534", + "scope_status": "changed", + "actual_scope": "Complete the written rank, complementary rank and normalized one-extra outer-product consequence of PR2277 Lemma OC in Lean over arbitrary fields.", + "scope_change_reason": "The baseline orientation passed. Adjacent ceiling range defects were handed to one coherent N025 repair; the explicitly unformalized source rank interface supplies a distinct bounded verification obligation.", + "bottleneck_link": "Root-code decoder lower bounds use the cross-matrix coupling; this removes its forward rank and rank-one proof-assistant boundary without repeating geometry tables or improving a cost bound.", + "budget_minutes": 180, + "stop_rule": "Stop after the forward rank/corank and normalized one-extra entry interface, source pins, independent finite controls and kernel replay.", + "outcome": "completed", + "evidence": "Coupling.lean, FORMAL-RESULT.json and RESULT.json; see README for distinct formal and finite checks.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance; predecessor Lemma OC and its original formal algebra are credited to DreamingOfClouds.", + "open_questions": [ + { + "question": "Can the converse and prescribed-direction criterion in PR2277 Lemma OC be formalized?", + "why_it_matters": "It would close the remaining algebraic interface before using finite geometric tables.", + "first_step": "Prove cancellation from the full ranks of both factors, then formalize the diagonal-plus-rank-one criterion.", + "blocked_by": "Not required for the forward rank and normalized one-extra consequence proved here." + } + ] +} diff --git a/research/overcomplete-rank-interface/TOOLCHAIN.json b/research/overcomplete-rank-interface/TOOLCHAIN.json new file mode 100644 index 0000000000..97795a4b1f --- /dev/null +++ b/research/overcomplete-rank-interface/TOOLCHAIN.json @@ -0,0 +1,9 @@ +{ + "lean_version": "4.33.0-rc1", + "lean_commit": "62eed1db4d67327ec8120be05f1a1b0847d74561", + "mathlib_commit": "55b7917b472489c7c56a0fa6393af05cfd536599", + "mathlib_manifest_sha256": "46612fb7c7c9a449af2d375e0736db59ae16d40928355fe96bedbb67e0a4ea00", + "windows_archive": "lean-4.33.0-rc1-windows.tar.zst", + "windows_archive_sha256": "20ce6f79ca6b42967a0215e2515eddbf4bd922034fd901fbf4232a86cdeb99d7", + "official_release": "https://github.com/leanprover/lean4/releases/tag/v4.33.0-rc1" +} diff --git a/research/overcomplete-rank-interface/VERIFY.json b/research/overcomplete-rank-interface/VERIFY.json new file mode 100644 index 0000000000..d822e59948 --- /dev/null +++ b/research/overcomplete-rank-interface/VERIFY.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate predecessor and formal source receipt; independently check exact rational and finite-field rank interfaces and semantic controls. Does not invoke Lean; the separate pinned Lean command is mandatory for the formal result." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/exportchecks.py" + ], + "timeout_seconds": 120, + "checks": "Optimized Git-free read-only finite replay; existing-output and predecessor/formal-source corruption controls." + } + ] +} diff --git a/research/overcomplete-rank-interface/exportchecks.py b/research/overcomplete-rank-interface/exportchecks.py new file mode 100644 index 0000000000..ba4392db84 --- /dev/null +++ b/research/overcomplete-rank-interface/exportchecks.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python3 +"""Git-free finite-replay controls; no implicit formal-toolchain download.""" +import hashlib +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def run(path, *args): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(path / 'verify.py'), *args], + capture_output=True, text=True, timeout=90) + + +def snapshot(path): + return {p.relative_to(path).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in path.rglob('*') if p.is_file()} + + +def main(): + with tempfile.TemporaryDirectory(prefix='oc-export-') as temp: + dest = Path(temp) / 'package' + shutil.copytree(HERE, dest) + before = snapshot(dest) + result = run(dest) + require(result.returncode == 0, result.stdout + result.stderr) + require(snapshot(dest) == before, 'default replay writes files') + result = run(dest, '--out', str(dest / 'RESULT.json')) + require(result.returncode != 0 and 'output already exists' in result.stderr, 'overwrite control') + for name, marker in [('vendor/pr2277/lean/Overcomplete.lean', 'predecessor source pin'), + ('Coupling.lean', 'formal source receipt pin')]: + path = dest / name + original = path.read_bytes() + path.write_bytes(original + b'\n-- altered\n') + result = run(dest) + require(result.returncode != 0 and marker in result.stderr, name + ' corruption control') + path.write_bytes(original) + require(snapshot(dest) == before, 'export content not restored') + print('PASS_OC_EXPORT: optimized Git-free read-only replay; three failure controls') + + +if __name__ == '__main__': + main() diff --git a/research/overcomplete-rank-interface/leancheck.py b/research/overcomplete-rank-interface/leancheck.py new file mode 100644 index 0000000000..060e24f0d9 --- /dev/null +++ b/research/overcomplete-rank-interface/leancheck.py @@ -0,0 +1,105 @@ +#!/usr/bin/env python3 +"""Replay the pinned formal proof and reject four altered theorem contracts. + +Apache-2.0. Prepared for ywz65 with OpenAI Codex assistance. +This never downloads tools or modifies the supplied Mathlib checkout. +""" +import argparse +import hashlib +import json +import os +from pathlib import Path +import re +import subprocess +import tempfile + +HERE = Path(__file__).resolve().parent +ROOTS = ['factor_rank', 'cross_rank', 'complement_rank', + 'rank_one_factorization', 'one_extra_factorization', 'one_extra_entries'] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def run(argv, **kwargs): + return subprocess.run(argv, capture_output=True, text=True, encoding='utf-8', + errors='replace', timeout=180, **kwargs) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--mathlib-root', type=Path, required=True) + parser.add_argument('--lean-bin', type=Path, required=True) + parser.add_argument('--out', type=Path) + args = parser.parse_args() + if args.out: + require(not args.out.exists(), 'output already exists') + pin = json.loads((HERE / 'TOOLCHAIN.json').read_bytes()) + mathlib = args.mathlib_root.resolve() + suffix = '.exe' if os.name == 'nt' else '' + lean = args.lean_bin.resolve() / ('lean' + suffix) + lake = args.lean_bin.resolve() / ('lake' + suffix) + version = run([str(lean), '--version']) + require(version.returncode == 0 and pin['lean_version'] in version.stdout + and pin['lean_commit'] in version.stdout, 'Lean version/commit mismatch') + head = run(['git', 'rev-parse', 'HEAD'], cwd=mathlib) + require(head.returncode == 0 and head.stdout.strip() == pin['mathlib_commit'], + 'Mathlib commit mismatch') + require(hashlib.sha256((mathlib / 'lake-manifest.json').read_bytes()).hexdigest() + == pin['mathlib_manifest_sha256'], 'Mathlib dependency manifest mismatch') + clean = run(['git', 'diff', '--quiet', 'HEAD', '--', 'Mathlib', 'lakefile.lean', + 'lakefile.toml', 'lake-manifest.json', 'lean-toolchain'], cwd=mathlib) + require(clean.returncode == 0, 'tracked Mathlib source differs') + env = dict(os.environ, PATH=str(args.lean_bin.resolve()) + os.pathsep + os.environ.get('PATH', '')) + code = (HERE / 'Coupling.lean').read_text(encoding='utf-8') + # Compilation and axiom checks are authoritative; this catches obvious bypass edits early. + require(not re.search(r'\b(sorry|admit|axiom|unsafe)\b', code), 'unproved declaration in source') + with tempfile.TemporaryDirectory(prefix='oc-lean-') as temp: + path = Path(temp) / 'Coupling.lean' + path.write_text(code, encoding='utf-8') + result = run([str(lake), 'env', 'lean', '-j', '2', str(path)], cwd=mathlib, env=env) + require(result.returncode == 0, 'Lean failed:\n' + result.stdout + result.stderr) + for name in ROOTS: + expected = "'OvercompleteRank." + name + "' depends on axioms: [propext, Classical.choice, Quot.sound]" + require(expected in result.stdout, 'axiom audit missing: ' + name) + require('sorryAx' not in result.stdout + result.stderr, 'unproved axiom found') + changes = [ + ('cross rank replaced by ambient size', + '(Y.transpose * X).rank = Fintype.card T := by', + '(Y.transpose * X).rank = Fintype.card M := by'), + ('exactness replaced by zero product', + 'theorem cross_rank (X Y : Matrix T M K) (h : X * Y.transpose = 1)', + 'theorem cross_rank (X Y : Matrix T M K) (h : X * Y.transpose = 0)'), + ('two extra columns called rank one', + 'theorem one_extra_rank (X Y : Matrix T M K) (h : X * Y.transpose = 1)\n (hm : Fintype.card M = Fintype.card T + 1)', + 'theorem one_extra_rank (X Y : Matrix T M K) (h : X * Y.transpose = 1)\n (hm : Fintype.card M = Fintype.card T + 2)'), + ('normalization changed to zero', + '(h : Matrix.vecMulVec a b * Matrix.vecMulVec a b = Matrix.vecMulVec a b) :\n dotProduct b a = 1 := by', + '(h : Matrix.vecMulVec a b * Matrix.vecMulVec a b = Matrix.vecMulVec a b) :\n dotProduct b a = 0 := by')] + rejected = [] + for label, before, after in changes: + require(code.count(before) == 1, 'mutation anchor differs: ' + label) + path.write_text(code.replace(before, after), encoding='utf-8') + mutant = run([str(lake), 'env', 'lean', '-j', '2', str(path)], cwd=mathlib, env=env) + require(mutant.returncode != 0 and 'error:' in mutant.stdout, + 'altered contract did not fail elaboration: ' + label) + rejected.append(label) + receipt = dict(schema_version=1, status='kernel-checked', + source_sha256=hashlib.sha256(code.encode()).hexdigest(), + lean_version=pin['lean_version'], lean_commit=pin['lean_commit'], + mathlib_commit=pin['mathlib_commit'], audited_roots=ROOTS, + allowed_axioms=['propext', 'Classical.choice', 'Quot.sound'], + rejected_contract_mutants=rejected) + if args.out: + with args.out.open('x', encoding='utf-8') as stream: + stream.write(json.dumps(receipt, indent=2) + '\n') + else: + require(receipt == json.loads((HERE / 'FORMAL-RESULT.json').read_bytes()), + 'formal receipt differs') + print('PASS_OC_LEAN: six audited roots; four rejected contract mutants') + + +if __name__ == '__main__': + main() diff --git a/research/overcomplete-rank-interface/vendor/pr2277/README.md b/research/overcomplete-rank-interface/vendor/pr2277/README.md new file mode 100644 index 0000000000..02660b10d4 --- /dev/null +++ b/research/overcomplete-rank-interface/vendor/pr2277/README.md @@ -0,0 +1,190 @@ +# Dense-pairing floors for overcomplete root-code decoders (E6 36, D5 20, every m) and for every rank-T realisation (E8 72, E7 49, D6 30, D4 12, P104 56), with a correction to Conjecture ID (a) (no κ claim) + +> **Scope, stated first.** This package is about the **algebraic cost** `Σ_j rank_F2 B[R_j, A_j]` of exact decoders of root units (and punctured root units) in the model of #446 / #595 / #1590 / #2111 / #2125 / #2228. It proves lower bounds **in stated classes** and one **correction** to a conjecture of ours. It contains **no κ claim, no window closed, no new supplier, no copy / hosting / restoration cost**, and it says nothing about decoders whose factors leave the column space of the realisation, about realisations of rank above T, or (except where a SAT statement says so) about pairings B other than the dense one. Every statement carries one of the labels below; every scope is spelled out in §2. +> +> **Labels.** **PROVEN** (full proof in this README); **CHECKED** (recomputed by `verify.sh`, exact integer / `Fraction` / bit arithmetic, or SAT with a DRAT proof that `drat-trim` verifies); **RECORDED** (a number of another PR or of the author's working notes, or a solver verdict whose proof is not shipped, not re-run here; for SAT items, "RECORDED: DRAT-verified at generation" means `verify.sh` regenerates the CNFs and checks their sha256 hashes and the recorded verdicts, while the DRAT proofs themselves are regenerable with `sat/run.py solve` but are not shipped); **OPEN**. +> +> **Correction (read this first).** Conjecture ID of #2228 §6, branch (a), says that for an *odd geometry* (an integral normalisation with unit diagonal exists) the optimal cost is `v`. **That branch is false when the number of terms is unbounded**: the 120-line unit "all lines pairwise orthogonal" with `M = I` has an exact decoder of cost **72 < 120** (§3, **PROVEN + CHECKED**). The values of Conjecture ID for the nine even root units are untouched, and #2228's Theorem 1 and Corollary 2.2 are not contradicted (their hypothesis is that all lines survive); but "odd geometry ⇒ cost* = v" and the framing of "geometry" as an invariant of the cost are wrong in the any-number-of-terms model. §3 gives the repaired statement `cost*(U) = min over admissible B of c(B)`. + +## 0. Reading this package + +```sh +bash research/overcomplete-and-realisation-floors/verify.sh /fresh/output/dir # from a checkout or `git archive`; Python >= 3.11, standard library only +DRAT_TRIM=/path/to/drat-trim bash research/overcomplete-and-realisation-floors/verify.sh /fresh/output/dir # additionally re-checks the shipped DRAT proofs +``` + +`verify.sh` first checks every file against `MANIFEST.sha256` and every pin of `SOURCES.json` (stops with exit 1 on mismatch), then runs six check scripts that print one `PASS` / `FAIL` line per assertion (`SKIP` for the DRAT re-check when `drat-trim` is neither on `PATH`, nor in `$DRAT_TRIM`, nor buildable from the vendored `research/p111-minrank-proof-reconciliation/vendor/drat-trim/drat-trim.c` with `cc`). One core, a few minutes (57 PASS lines including step 0's two, with `drat-trim`). No solver is needed for verification; `kissat` is only needed to *re-solve* (optional, `KISSAT_RESOLVE=n`). + +| script | what it recomputes | +|---|---| +| `checks/c1_overcomplete_d5.py` | Lemma OC on 120 exact random decompositions; D5: deficient directions, pair ranks 3 / 4, the combinatorial core of the D5 theorem | +| `checks/c2_free_terms_frame120.py` | the 6,728-term exact decoder of the 120-line frame unit, `M = I`, cost 72 | +| `checks/c3_realisation_free_floors.py` | frame-intersection certificate on D4, D5, D6, E6, E7, E8, P104, P112, E7 minus a 7-frame (all 2^h − 1 label classes of each); P104 / P112 pair-rank tables | +| `checks/c4_e6_overcomplete.py` | E6: 27 deficient directions, 432 + 297 pair ranks, 1-dimensional bilinear-form space, transitivity of W(E6) on the 432 rank-5 pairs, exhaustive search over **5,504,660** seven-sets | +| `checks/c5_known_decoders.py` | the decoders that attain the floors: E8 72, E7 49, D6 30, D4 12, P112 64, P104 56 (and the trivial decoders for E6 / D5) | +| `checks/c6_sat_replay.py` | regenerates all 1,473 SAT instances, compares DIMACS hashes, checks SAT models clause by clause, re-checks the shipped DRAT proofs | + +**Prior work this builds on.** The model, the dense pairing and the root-code floor: **#446** (cost model, Theorem C), **#595 / #1590** (merged; two lemmas and an erratum), **#2111**, **#2125** (T² threshold, E7 first gain), **#2162** (T = 3 side), **#2228** (the dense polar law, Theorem 4 root-code floors, **Conjecture ID**, which this package corrects in one branch), **#2244** (the Lagrangian bound for line systems; unrelated to the statements here but the same model). The E8 / P112 / P104 floors for exactly 8 terms or for factors in the live root code: **#968** (merged, frame-pair decoders), **#1077**, **#1180** (merged; overcomplete factor-linear E8 decoders retain the puncture floor, and the 9-term example *outside* the root code that marks the boundary of this package), **#1224** (merged, joaqcoo: for E8 with live roots spanning `R^8`, factors split as `D = RA + N₁`, `T = RB + N₂` with exactness `ABᵀ = 2I`, `N₁Bᵀ = 0`, …; nine-term decoders are one-sided overcomplete representations), **#1633** (merged, bbMisk: for exact overcomplete E8 decoders the ranks of the two factors outside the live root code satisfy `s + t ≤ m − 8`), **#1212** (merged; rank-8 decoders are gauge-rigid), **#1236**, **#1744**, **#1815** (merged; unit diagonals and required zeros force `N = R Rᵀ`, `B = U Uᵀ` for P112 — the same mechanism as our Lemma 7.1 for E6 / D5). Forced minors: **#2176**, **#2206**. Independent E6 screens: **#2137** (1337isnot1337: the orthogonal-zero constraints on the 36 coordinates of a bilinear form `L` have rank 35, kernel `Q·G`; this is our §7 check `c4.nspace` / `c1.d5nspace`, found independently), **#2232**, **#2240** (one-extra frame screen, minimum 40 over its alphabet), **#2247** (sheared one-extra screen, 330,486 support cells, minimum 37 and none below 36): these are RECORDED, scoped to their finite families, and agree with §7 below, which closes the E6 seven-term question **for the whole root-code class**. Swarm discussion of the minrank / shadow viewpoint: #2232, #2240, #2247. **Free terms are not new.** Zero-cost corrections supported on zero-pairing rectangles ("free rectangles") are the mechanism of **#1331** (Arham-Tahir64: one free P112 rectangle cannot improve a coordinate COPY term; sharp whole-decoder floor 64) and **#1375** (commdata2338: two-coordinate mixing with small free rectangles keeps COPY 64), followed by **#1460** (bbMisk: pair (4,6), arbitrary free rectangles), **#1468** (bitplane: arbitrary one-column corrections) and **#1591** (Arham-Tahir64: all nine-factor singleton completions, COPY ≥ 64); all are scoped negative results for P112. Proposition 3.1 is the same move applied to whole units; what is new here is its use against Conjecture ID (a). The Shadow Lemma is Lemma CR2 / `hadamard_diag_rank_sum` of #2162 (`lean/DecoderDuality.lean`), with a rectangular Lean form in #2267; only `Overcomplete.lean` is shipped (§4). The repository helper `scripts/find_overlap.py --refresh` was run before submission (it also searches discussions: it surfaced discussion 1316, the free-rectangle line of #1331, and discussion 1622 = #1633, already cited; nothing else new). + +## 1. Setting and notation + +* A **unit** `U` is a list of `v` pairwise non-proportional vectors `r_t ∈ Q^n` ("lines"); `t ⊥ s` means `r_t · r_s = 0`. `V := span{r_t}`, `T := dim V`. All units here are root systems or punctures of E8: `D4, D5, D6, E6, E7, E8` and `P112 = E8 minus an 8-frame`, `P104 = E8 minus two 8-frames`, `E7-frame = E7 minus a 7-frame`; `lib/roots.py` builds them (E8 in doubled integer coordinates, E7 / E6 as orthogonal complements of one resp. two roots, D_n from `±e_i ± e_j`). +* A **realisation** of `U` over a field `K ⊇ Q` is a matrix `M ∈ K^{v×v}` with `M_tt ≠ 0` and `M_ts = 0` whenever `t ⊥ s` (other entries arbitrary, possibly 0). A **decoder** is `M = Σ_{j=1..m} p_j q_jᵀ` (`p_j, q_j ∈ K^v`) together with an **admissible pairing** `B ∈ F2^{v×v}`: `B_tt = 1`, and `B_ts = 1` (`t ≠ s`) only if `t ⊥ s`. Then `B̃ ∘ M = diag(M_tt)` holds automatically. `R_j = supp p_j`, `A_j = supp q_j`, and + **cost = Σ_j rank_{F2} B[R_j, A_j]**. + The factors are *unrestricted* unless a theorem says otherwise. Terms with `p_j = 0` or `q_j = 0` contribute nothing and are dropped. +* The **dense pairing** is `B_d := J + Ā`, i.e. `B_ts = 1` iff `t = s` or `t ⊥ s`; it depends on the orthogonality pattern only. `h := rank_F2 B_d` (D4 3, D5 5, D6 5, E6 7, E7 7, E8 9, P104 9, P112 9, E7-frame 7). It is symmetric. +* **Label classes.** Let `C := col(B_d) ⊆ F2^v` (dimension `h`). A **class** is the support of a nonzero vector `w ∈ C` (`2^h − 1` of them, counted by vector). For `R ⊆ [v]` put `Def(R) := {w ∈ C : supp w ∩ R = ∅}` (a subspace of `C`) and `δ(R) := dim Def(R)`. In the notation of #2228, the classes are the sets `O_z = {t : Ω(u_t, z) = 1}`. +* **Root-code decoders** (the class of #2228 Theorem 4). For a unit with line matrix `R ∈ Q^{v×n}`: `p_j = D₁ R x_j`, `q_j = D₂ R y_j` with `x_j, y_j ∈ V_K` and `D₁, D₂` invertible diagonal. Then `R(x) := supp(D₁Rx) = {t : r_t · x ≠ 0}`. +* **Frames.** A **T-frame** is a set of `T` pairwise orthogonal lines; `α_⊥` is the size of a largest orthogonal set. If `U` has a `T`-frame `F`, every realisation `M` has `M[F,F]` diagonal and invertible, so **every realisation has rank ≥ α_⊥** (PROVEN, one line). + +## 2. Results at a glance + +| # | statement | label | exact scope | where | +|---|---|---|---|---| +| ID-a | Conjecture ID branch (a) (odd geometry ⇒ cost* = v) is false: the 120-line frame unit has an exact decoder of cost 72 | **PROVEN + CHECKED** | model with an unbounded number of terms; `M = I`; `B = J + Ā_E8`; 6,728 terms | §3, `c2` | +| Mono | `orth(U') ⊆ orth(U)` on the same lines ⇒ `cost*(U) ≤ cost*(U')`; and `cost*(U) = min over admissible B of c(B)`, `c(B)` = cost of the unit whose orthogonality relation is `supp B` | **PROVEN** | any number of terms, any field of characteristic 0 | §3 | +| OC | `Σ_{j≤m} x_j y_jᵀ = id_V` ⇔ `K = (⟨y_i,x_j⟩)` is an idempotent of rank `T`; `m = T` ⇒ biorthogonal; `m = T+1` ⇒ `I − K` has rank one, off-diagonal of `K` is rank one; criterion for prescribed directions | **PROVEN** (idempotency, traces, square case: **Lean**, no `sorry`); spot-checked on 120 exact instances (`c1`) | any field of characteristic 0; factors in `V` | §4 | +| E6 | every root-code decoder of E6 (scaled-Gram realisation), dense `B`, **every** number of terms `m`, costs **≥ 36** | **PROVEN** from **CHECKED** data (`c4`: 5,504,660 seven-sets, exact integers) | factors in `col M`; realisations `D₁ G D₂`; dense `B`; char 0 | §7 | +| D5 | same for D5: **≥ 20** | **PROVEN** from **CHECKED** data (`c1`) | same | §7 | +| 4′ | Theorem 4′: the root-code floor `cost ≥ Σ_j (h − δ(R_j) − δ(A_j))` holds for **every realisation** `M` of rank `T`, deficiency being a property of the label class in that realisation | **PROVEN** | col P ⊆ col M, col Q ⊆ row M (all square decoders; any `m` otherwise); dense `B`; rank of `M` exactly `T` | §5 | +| 3.3 | frame-intersection certificate: a class is non-deficient in **every** rank-`T` realisation if it contains a `T`-frame, or (clause (c)) if a `T`-frame contains the parts `F_i ∖ O` of frames with empty common intersection | **PROVEN** | rank-`T` realisations of units with a `T`-frame | §5 | +| 3.4 | for every rank-`T` realisation and every decoder with col P ⊆ col M, col Q ⊆ row M, dense `B`: **E8 ≥ 72, E7 ≥ 49, D6 ≥ 30, D4 ≥ 12, P104 ≥ 56, P112 ≥ 56**; E8, E7, D6, D4, P104 are attained (P112: 64 attained, 56 proven here), see `c5` | **PROVEN** from **CHECKED** tables (`c3`) | as in 4′ | §5 | +| – | E6 / D5 have no `T`-frame (`α_⊥ = 4`), so §5 gives nothing; the realisation-free statement for E6 / D5 is open | **OPEN** | | §8 | +| SAT-1 | `min over admissible B of rank_F2 B` on E6 equals **7** (UNSAT at 5 and 6, each under three symmetry-breaking cliques; SAT at 7) | **CHECKED** (kissat 4.0.4 + DRAT, drat-trim VERIFIED) | all 36 lines | §9.1 | +| SAT-2 | char-2 shadow minranks: `mr₂(Γ_E6) ≥ 7`, `mr₂(Γ_E7) ≥ 8` (UNSAT at 6 resp. 7, two cliques each) ⇒ a B-independent F2 shadow cannot certify all lines with `T` terms | **RECORDED**: DRAT-verified at generation (E7 part: shipped proof, **CHECKED**); `verify.sh` checks the CNF hashes and recorded verdicts for the E6 part, whose proofs are regenerable, not shipped ⇒ **PROVEN** consequence given those | over `F2` only | §9.2 | +| SAT-3 | per-term drops are real: an E6 deficient pair of dense rank 6 has fitting minrank 4; E8 root blocks: 9, 9, ≤ 8 | **CHECKED** (DRAT / model) | single blocks, any `B` | §9.3 | +| SAT-4 | the known optimal decoders are `B`-robust: every term of the E8 frame decoder (8), E8 coordinate decoder (terms 0, 7), E7 frame decoder (7), P112 removed-frame decoder (8), P104 frame-pair decoder (8) has fitting minrank equal to its dense rank (UNSAT at dense − 1) | **CHECKED** (DRAT) | those specific terms, any `B` | §9.4 | +| SAT-5 | a shared `B` never brings any of **26** E6 square decoders below 36: **1,262** instances (every cap vector with `c_j ≥ fr_j`, `Σ c_j = 35`), all UNSAT, plus 156 floor instances | **RECORDED**: DRAT-verified at generation; `verify.sh` checks CNF hashes and recorded verdicts (proofs regenerable with `sat/run.py solve`, not shipped); decoder exactness is **CHECKED** (`c6.decoders`) | those 26 decoders (`data/e6_square_decoders.json`), every admissible `B` | §9.5 | + +**What is *not* proven here.** Arbitrary admissible `B` for a whole unit (only SAT-1..5 above); decoders with `col P ⊄ col M` (e.g. the 9-term example of #1180); realisations of rank `> T`; the E6 / D5 statements for realisations other than `D₁ G D₂`; P112 `≥ 64` for every realisation; any bound for `T = 3`. + +## 3. A correction to Conjecture ID (a), and the shape of cost* + +Free terms are the point (the "free rectangle" of #1331 / #1375). A term whose block `B[R_j, A_j]` is zero costs nothing, and a single-entry term `c e_t e_sᵀ` is free whenever `B_ts = 0`. + +**Proposition 3.1 (monotonicity) — PROVEN.** If `orth(U') ⊆ orth(U)` on the same `v` lines (patterns of required zeros, possibly directed) then `cost*(U) ≤ cost*(U')`. +*Proof.* Take an optimal decoder `(M', P', Q', B')` of `U'`. Its `B'` is admissible for `U` (its off-diagonal ones lie in `orth(U') ⊆ orth(U)`). For every `(t,s) ∈ orth(U) ∖ orth(U')` add the term `−M'_ts e_t e_sᵀ`; its block is `B'_ts = 0`, so it is free. The new `M` vanishes on `orth(U)`, its diagonal is unchanged. ∎ + +**Proposition 3.2 (reformulation) — PROVEN.** `cost*(U) = min over B admissible for U of c(B)`, where `c(B)` is the optimal cost, with the fixed pairing `B`, of decoders whose realisation `M` has `M_tt ≠ 0` and `M_ts = 0` exactly where required by the pattern `S(B) := {(t,s) : t ≠ s, B_ts = 1}` (a directed pattern if `B` is not symmetric; nothing else is asked of `M`). +*Proof.* "≤": Proposition 3.1 with `U'` the `B`-unit. "≥": take a decoder of `U` with pairing `B`. Every line has `M_tt ≠ 0`, so some term covers `(t,t)`, and its block contains `B_tt = 1`; hence free terms never touch a diagonal entry. The paid terms (nonzero block) sum to a matrix `N` with the same diagonal as `M`, and `N_ts = 0` wherever `B_ts = 1`, `t ≠ s` (there every free term contributes 0 and `B̃ ∘ M = Δ`). So the paid part is a decoder of the `B`-unit of the same cost. ∎ + +**Proposition 3.3 (the 120-line frame unit costs at most 72) — PROVEN + CHECKED (`c2`).** Let `F_120` be the unit of 120 lines, all pairs orthogonal; it admits every `B` with unit diagonal, and `M = I` (unit diagonal, "odd geometry") is a realisation. Take the E8 lines `r_t` (norm 2), `B = J + Ā_{E8}` (dense pairing of E8), and the terms + * `j = 1..8`: `p_j(t) = r_t[j]/2`, `q_j(s) = r_s[j]` (coordinate `j` of the E8 lines in the standard coordinates), whose sum is `½ G` (`G` the E8 Gram matrix); + * one **free term** `p = −(G_ts/2) e_t`, `q = e_s` for each of the 6,720 ordered non-orthogonal E8 pairs `(t,s)`. +Then `Σ p q^T = ½G − ½(G − 2I) = I` exactly (`G_tt = 2`, the free terms cancel the off-diagonal part), `B̃ ∘ I = I`, the 8 coordinate terms have `F2`-rank 9 each (the 78 lines with a nonzero coordinate `j`; computed), and every free term has block `B_ts = 0` (the pair is non-orthogonal in E8), i.e. rank 0. Total cost **72 < 120 = v**. `c2` recomputes the sum `M = I` over 6,728 exact `Fraction` terms and the 8 + 6,720 ranks. ∎ + +*Consequences, stated plainly.* (i) Conjecture ID (a) ("odd geometry ⇒ cost* = v") fails for `F_120`; the "odd geometry" property (an integral normalisation with unit diagonal) is not an invariant of cost* in the model where the number of terms is unbounded. F_120 (and F_104) are degenerate (`T = v`); no counterexample to (a) with `T < v` is known, and the only non-degenerate odd-geometry row of #2228 (Eisenstein, 40) still satisfies (a) by #2017. (ii) The correct way to read the frame unit is Proposition 3.2: the unit allows every `B`, and `c(B_dense(E8)) ≤ 72`. In this reading the search for good units is a search for **admissible pairings `B` with small `c(B)/v`**. (iii) #2228's Theorem 1 is *not* contradicted: it bounds the cost below by the number of lines whose leading 2-adic terms survive, and #2228 Corollary 2.2 derives "cost ≥ v" only for decoders in which all lines survive for some prime and shift; the decoder above has cost 72 < 120, so by Theorem 1 not all lines survive in it. (We have not recomputed the count of surviving lines for this decoder.) (iv) The theorems of §§5–7 are *not* affected: they assume `col P ⊆ col M`, `col Q ⊆ row M`, and a single-entry term `e_t e_sᵀ` lies outside `col M` as soon as `rank M < v`. (v) Scope: the decoder needs more than `T` terms; with the number of terms capped at the rank of the realisation, free terms are not available. The same move gives `cost*(F_104) ≤ 56` from the known P104 decoder; we did not re-run that and do not claim it. + +## 4. Lemma OC (overcomplete coupling) + +*Relation to #1224.* For E8 with `R` the matrix of live roots, #1224 Theorem A contains the identity `A Bᵀ = 2I` for the root-code parts; Lemma OC below is the same identity written as a statement about the cross matrix `K = YᵀX`, which (i) is basis-free, (ii) holds for any unit and any field (it is used here for E6 and D5, where a root basis does not have a dual basis of roots), and (iii) gives the idempotent / rank-one-off-diagonal structure used in §7. It is elementary and we claim nothing deeper. + +**Lemma OC — PROVEN.** Let `V = 𝕜^T` (`𝕜` a field of characteristic 0, or any field), `x_1..x_m ∈ V`, `y_1..y_m ∈ V*`, and `Σ_j x_j ⊗ y_j = id_V` (absorb coefficients into `y_j`). Put `K_ij := ⟨y_i, x_j⟩` (an `m × m` matrix). Then **`K` is idempotent of rank `T`**, so `Π := I_m − K` is idempotent of rank `m − T` and `trace Π = m − T`. Conversely, if `rank(x_j) = rank(y_j) = T` and `K² = K`, then `Σ_j x_j ⊗ y_j = id_V`. +*Proof.* With `X = [x_j]`, `Y = [y_j]` (`T × m`): `XYᵀ = I_T`, so `K = YᵀX` satisfies `K² = Yᵀ(XYᵀ)X = K`, and `rank K = rank X = T` (`Yᵀ` is injective since `XYᵀ = I`). Conversely `K² = K` reads `Yᵀ(XYᵀ − I)X = 0`; `Yᵀ` is injective (rank `T`) and `X` surjective (rank `T`). ∎ +**Lean:** `lean/Overcomplete.lean` proves `oc_idempotent` (`(Yᵀ X)² = Yᵀ X`), `oc_trace` (`tr(Yᵀ X) = T`), `oc_complement_idempotent`, `oc_complement_trace` (`tr(1 − YᵀX) = m − T`) and `oc_square` (`m = T` ⇒ `Yᵀ X = 1`), with `#print axioms` showing only `propext, Classical.choice, Quot.sound`, no `sorry`. The rank statements, the converse and the consequences below are written proofs (not formalised). + +**Consequences — PROVEN.** + (a) `m = T`: `Π = 0`, so `⟨y_i, x_j⟩ = δ_ij` (biorthogonality; this is also `oc_square`). + (b) `m = T + 1`: `Π = u wᵀ` with `wᵀ u = 1` (rank-one idempotent), so `⟨y_i, x_j⟩ = −u_i w_j` for `i ≠ j`: **the cross matrix agrees off the diagonal with the rank-one matrix `−u wᵀ`**, and `⟨y_i, x_i⟩ = 1 − u_i w_i`. + (c) A term with `⟨y_i, x_i⟩ = 0` has `Π_ii = 1`. + (d) (**criterion for prescribed directions**) Let `m = T + 1 ≥ 3`, prescribed lines `x̂_j, ŷ_j` with `rank[x̂_j] = rank[ŷ_j] = T` and `Λ_ij := ⟨ŷ_i, x̂_j⟩ ≠ 0` for `i ≠ j`. There are scalars with `Σ_j (s_j x̂_j) ⊗ (t_j ŷ_j) = id` **iff** `Λ = D + a bᵀ` with `D` diagonal and invertible. + *Proof of (d).* "⇒": by the Lemma, `K = diag(t) Λ diag(s) = I − u wᵀ` for some `u, w` (the scalars `s_j, t_i` multiply `x̂_j, ŷ_i`; and `Π := I − K` is idempotent of rank `m − T = 1`, hence `Π = u wᵀ`), so `Λ = diag(1/t) (I − u wᵀ) diag(1/s)` has the form `D + a bᵀ` with `D = diag(1/(t_i s_i))` invertible. "⇐": given `Λ = D + a bᵀ`, choose `s_i t_i = 1/D_ii`, `u_i = −t_i a_i`, `w_j = s_j b_j`. Then `K := diag(t) Λ diag(s) = I − u wᵀ`. Since `rank Λ ≤ T < m`, `det Λ = 0`, i.e. `det(I + D⁻¹ a bᵀ) = 0`, i.e. `1 + Σ a_i b_i / D_ii = 0`, i.e. `wᵀ u = −Σ s_i t_i a_i b_i = 1`. So `Π = uwᵀ` is idempotent, `K² = K`, and the converse of the Lemma gives `Σ = id`. ∎ + (e) A term-count consequence: at least `T` terms have `x_j ≠ 0 ≠ y_j`. + +## 5. Theorem 4′ and the frame-intersection certificate (realisation-free floors) + +Fix a unit with a `T`-frame and a realisation `M` of rank exactly `T` (so `T = α_⊥` is the minimum possible rank). Write `M = P₀ N Q₀ᵀ` with `P₀, Q₀ ∈ K^{v×T}` bases of `col M`, `col Mᵀ` and `N ∈ GL_T(K)`; `π(t)` (resp. `κ(s)`) is row `t` of `P₀` (row `s` of `Q₀`). Consider decoders with `p_j = P₀ x_j`, `q_j = Q₀ y_j` (`col P ⊆ col M`, `col Q ⊆ row M`); **every square decoder (`m = T`) is of this form** (`rank M = T ≤ rank P ≤ m`). Then `N = Σ_j x_j y_jᵀ` (as `P₀, Q₀` are injective), so at least `T` terms are nonzero. + +**Lemma 5.1 (support-only bound) — PROVEN.** For any `R, A ⊆ [v]`: `rank_F2 B_d[R, A] ≥ h − δ(R) − δ(A)`, and `rank B_d[R,A]` depends only on the two subspaces `Def(R), Def(A) ⊆ C`. +*Proof.* Choose a rank factorisation `B_d = X Yᵀ` with `X, Y ∈ F2^{v×h}` of full column rank; `col X = col Y = C` (`B_d` is symmetric). `ker X_R = {z : X_R z = 0} ≅ {w ∈ C : w|_R = 0} = Def(R)` (via `w = Xz`), so `rank X_R = h − δ(R)`; likewise `rank Y_A = h − δ(A)`. Sylvester: `rank(X_R Y_Aᵀ) ≥ rank X_R + rank Y_A − h`. If `X_R` and `X_{R'}` have the same kernel they have the same row space `W`, and `X_R = S W` with `S` of full column rank, so `rank(X_R Y_Aᵀ) = rank(W Y_Aᵀ)`; the same on the other side. ∎ + +**Theorem 4′ — PROVEN.** In the setting above and with the dense pairing `B_d`, + **cost ≥ Σ_{j : x_j,y_j ≠ 0} ( h − δ(R(x_j)) − δ(A(y_j)) ),** where `R(x) = {t : π(t)·x ≠ 0}`, `A(y) = {s : κ(s)·y ≠ 0}`. +Call a class `O` **π-deficient** if `π(O)` lies in a hyperplane of `K^T` (**κ-deficient** analogously). If `w ∈ Def(R(x))` then `supp w ∩ R(x) = ∅`, i.e. `π(supp w) ⊆ x^⊥`: the class `supp w` is π-deficient. **If no class is π-deficient or κ-deficient, every term costs ≥ h and cost ≥ T·h.** +*Proof.* Lemma 5.1 and the count of nonzero terms (§5, last sentence of the setting). ∎ +This is #2228 Theorem 4 (which already allows `M = D₁ R N Rᵀ D₂` with arbitrary `N`, for factors in the scaled root code) extended to rank-`T` realisations whose column space is not a scaled root code (`col M ≠ D₁·RV`); in the Gram case `π = κ = ` coordinates of the line. + +**Lemma 5.2 (frame-intersection certificate) — PROVEN.** Let `M` be a rank-`T` realisation and `O ⊆ [v]` with `π(O) ⊆ ker c` for a nonzero functional `c`. Then + (a) `O` contains no `T`-frame; + (b) for every `T`-frame `F`, `c ∈ span σ(F ∖ O)`, where `σ(s) := N κ(s)ᵀ`; + (c) if a `T`-frame `E` contains the sets `F_1∖O, …, F_k∖O` of `T`-frames `F_i` whose intersection `∩_i (F_i ∖ O)` is empty, then `c = 0`, a contradiction. +Hence **a class that contains a `T`-frame, or satisfies (c), is not π-deficient in any rank-`T` realisation.** Replacing `M` by `Mᵀ` (a realisation of the same pattern) gives the same for κ. +*Proof.* For a `T`-frame `F`, `M[F,F] = P₀[F] N Q₀[F]ᵀ` is diagonal (all pairs orthogonal) with nonzero diagonal, hence invertible, so `{π(f)}_{f∈F}` is a basis of `K^T`, and `π(f)·σ(f') = 0` for `f ≠ f'`, `≠ 0` for `f = f'`: `{σ(f)}` is the dual basis up to scalars, and **σ(f) depends on the line `f` only, not on the frame**. (a): `F ⊆ O` would give `c ⟂ π(F)`, a basis. (b): expand `c = Σ_{f∈F} λ_f σ(f)`; then `π(f')·c = λ_{f'} π(f')·σ(f')`, which is 0 for `f' ∈ F ∩ O`. (c): by (b), `c ∈ ∩_i span σ(F_i∖O)`; all `F_i ∖ O ⊆ E` and `σ(E)` is a basis, so these spans are coordinate subspaces and their intersection is `span σ(∩_i F_i∖O) = 0`. ∎ + +**Corollary 5.3 (realisation-free floors) — PROVEN from the CHECKED tables of `c3`.** (`c3` enumerates, for each unit, all maximal cliques of the orthogonality graph (frames = cliques of size `T`), all `2^h − 1` classes, and decides for each class: contains a `T`-frame / certified by (c) / uncertified.) + +| unit | v | T | h | α_⊥ | T-frames | classes (2^h−1) | contain a T-frame | certified by (c) | uncertified | 2-dim subspace of uncertified? | +|---|---|---|---|---|---|---|---|---|---|---| +| D4 | 12 | 4 | 3 | 4 | 3 | 7 | 7 | – | 0 | – | +| D6 | 30 | 6 | 5 | 6 | 15 | 31 | 16 | 15 | 0 | – | +| E7 | 63 | 7 | 7 | 7 | 135 | 127 | 64 | 63 | 0 | – | +| E8 | 120 | 8 | 9 | 8 | 2025 | 511 | 391 | 120 | 0 | – | +| P104 | 104 | 8 | 9 | 8 | 759 | 511 | 375 | 104 | 32 (size 52) | no | +| P112 | 112 | 8 | 9 | 8 | 1260 | 511 | 383 | 112 | 16 (size 56) | no | +| E7-frame | 56 | 7 | 7 | 7 | 64 | 127 | 57 | 56 | 14 (sizes 24, 32) | yes | +| E6 | 36 | 6 | 7 | 4 | 0 | 127 | 0 | 0 | 127 | yes | +| D5 | 20 | 5 | 5 | 4 | 0 | 31 | 0 | 0 | 31 | yes | + +(The classes without a `T`-frame are exactly the neighbourhoods `N(α) = {t ≠ α : r_t · r_α ≠ 0}` — `c3.N.*`; in E8 every frame not through `α` meets `N(α)` in exactly 4 lines, which is why clause (c) is needed — `c3.e8meet`.) Consequently, for **every realisation of rank `T`** and **every decoder with `col P ⊆ col M`, `col Q ⊆ row M`** (all square decoders, any number of terms otherwise), dense `B`: + * **E8 ≥ 72, E7 ≥ 49, D6 ≥ 30, D4 ≥ 12** (no class is deficient, every term has rank `h`, `T` terms at least); + * **P104 ≥ 56** and **P112 ≥ 56**: the uncertified classes contain no 2-dimensional subspace, so `δ(R), δ(A) ≤ 1` for every term (a `Def(R)` consists of π-deficient, hence uncertified, classes and is a subspace), each uncertified class has deficiency exactly 1 (`c3.pairs.*`), and the rank of a term depends only on `(Def(R), Def(A))` (Lemma 5.1); over the `(uncertified or none)²` pairs the computed ranks are `{7: 640, 8: 448, 9: 1}` (P104) and `{7: 192, 8: 96, 9: 1}` (P112), minimum 7, so `8 · 7 = 56`. +**Sharpness (CHECKED, `c5`).** The decoders of `c5` attain E8 72, E7 49, D6 30, D4 12 (frame decoders with `M = G`), P112 64 (removed-frame decoder) and P104 56 (the eight frame-pair terms of #968; `M = R N Rᵀ` with `N` not the Gram form). For P112 the gap between the realisation-free 56 and the attained 64 is **OPEN** (§8); in the Gram realisation 64 is #2228 Theorem 4 (RECORDED, not re-run). The E6 and D5 values are covered in §7. + +*How this relates to earlier work.* For the E8 / P112 / P104 values with factors in the live root code, the statement is #1180 and #2228 Theorem 4; for exactly 8 terms, #968 / #1077 / #1212. What Theorem 4′ adds to #2228 Theorem 4 is the case `col M ≠ D₁·(root code)`: Lemma 5.2 shows that *no realisation of rank `T`* can make a class deficient, so the floors hold for every rank-`T` realisation (the hypothesis `col P ⊆ col M`, `col Q ⊆ row M` remains). We do not claim priority for the E8 value itself. + +## 6. The cap on what is proven: realisations of rank above T + +If `rank M = ρ > T`, a `T`-frame no longer spans `K^ρ` and Lemma 5.2 fails. Theorem 4′ still gives `cost ≥ Σ_j (h − δ_j − δ'_j)` with at least `ρ` terms, but `δ` is no longer controlled by frames. This is **OPEN** (§8). + +## 7. E6 and D5 for every number of terms (scaled-Gram realisations) + +**The class.** `p_j = D₁ R x_j`, `q_j = D₂ R y_j`, `x_j, y_j ∈ V_K`, any `m`, dense `B`. Then `M = D₁ R N Rᵀ D₂` with `N = Σ x_j y_jᵀ ∈ V ⊗ V`. + +**Lemma 7.1 — CHECKED (`c4.nspace`, `c1.d5nspace`).** For E6 and for D5 the space `𝒩 = {N ∈ V ⊗ V : r_tᵀ N r_s = 0 for all orthogonal t, s}` is **one-dimensional**, spanned by the metric (identity in orthonormal coordinates). (Exact rational rank of the constraint system on the `T²` unknowns; #2137 computes the same kernel for E6 in its coordinates.) Hence `N = c·Id_V`, `c ≠ 0` (the diagonal of `M` is nonzero), and after absorbing `c`: **`Σ_j x_j ⊗ y_j = id_V`**, so Lemma OC applies with `T = 6` (E6) resp. `5` (D5), and `m ≥ T`. + +**Lemma 7.2 — CHECKED (`c4.dirs`, `c4.pairranks`, `c4.cross`, `c1.d5dirs`, `c1.d5ranks`).** Over `Q`, the classes of E6 (127) with `rank π(O) < 6` are exactly 27, each with a one-dimensional annihilator; the 27 annihilators are 27 distinct lines (the minuscule weights). Call a direction `x ∈ V_K` **deficient** if it lies on one of them; for a deficient `x`, `δ(R(x)) = 1`, for every other `x`, `δ(R(x)) = 0` (a class sits inside `x^⊥` iff `x` spans its annihilator, and the map class ↦ direction is injective). The same holds on the column side with the same 27 lines (`B_d` is symmetric). Dense-pairing ranks of terms (Lemma 5.1 and the table): both deficient: **5** (432 ordered pairs) or **6** (297 pairs); exactly one deficient: 6; none: 7. **All 27 × 27 cross products `⟨y, x⟩` of deficient directions are nonzero.** For D5 the deficient directions are the five axes `e_1..e_5`; both deficient: rank **4** if matched (`e_a, e_a`), **3** if `a ≠ b` (20 pairs); one deficient: 4; none: 5. + +**Theorem 7.3 (E6 ≥ 36 for every `m`) — PROVEN from CHECKED data (Lemmas 7.1, 7.2 and `c4.transitive`, `c4.nodes`, `c4.noleaf`).** Every root-code decoder of E6 with dense `B` has cost `≥ 36`. +*Proof.* By Lemma 7.1 `Σ x_j y_jᵀ = id`. Suppose a decoder of cost `c₀` exists and take one of cost `≤ c₀` with the fewest terms. Two terms with proportional `x` and proportional `y` have the same supports and can be merged into one term of the same rank (or both vanish), contradicting minimality; so the ordered pairs of lines `([x_j],[y_j])` are pairwise distinct (and terms with a zero factor are absent). Every term costs `≥ 5` (Lemma 7.2). + *`m ≥ 8`*: cost `≥ 40`. + *`m = 6`* (square, `m = T`): by OC(a), `⟨y_i, x_j⟩ = δ_ij`. Let `k` (resp. `l`) be the number of deficient `x_j` (resp. `y_j`). If `y_j` is deficient, every `x_i`, `i ≠ j`, is non-deficient — otherwise `⟨y_j, x_i⟩ = 0` for two deficient directions, contradicting Lemma 7.2. Hence `l ≥ 1` forces `k ≤ 1`, and `k ≥ 2` forces `l = 0`. By Lemma 5.1 each term costs `≥ 7 − [x_j def] − [y_j def]`, so cost `≥ 42 − k − l`. If `k ≥ 2` then `l = 0`, cost `≥ 42 − 6 = 36`; symmetrically for `l ≥ 2`; if `k, l ≤ 1`, cost `≥ 40`. + *`m = 7`*: cost `≤ 35` forces all seven terms to have rank 5 (`7 · 5 = 35`), i.e. seven distinct pairs from the 432 rank-5 pairs. By OC(b) the off-diagonal of `Λ_ij = ⟨y_i, x_j⟩` has rank one (rescaling rows and columns by the nonzero scalars `s_j, t_i` does not change this), and `rank[x_j] = rank[y_j] = 6`. W(E6) is transitive on the 432 rank-5 pairs (`c4.transitive`: the orbit of one pair under the 36 reflections has 432 elements), and it permutes the lines and so preserves everything, so one pair may be fixed. `c4` then enumerates **all** 7-sets containing that pair whose `Λ` has rank-one off-diagonal (exact integer cross-multiplication, no floating point): there are 27,250 triples, 206,275 / 898,460 / 2,502,409 / **5,504,660** sets of sizes 4 / 5 / 6 / 7 (`c4.nodes`; these numbers reproduce the node counts of an independent floating-point search of the working notes, which used `numpy`), and **none** of the 5,504,660 has both its row directions and its column directions spanning `V` — in fact none has `≥ 6` distinct row directions and `≥ 6` distinct column directions (`c4.noleaf`). So no 7-term decomposition exists. + Since `m = 6, 7` and `m ≥ 8` exhaust the possibilities (`m ≥ 6` is needed for `Σ x_j y_jᵀ = id`), cost `≥ 36` in all cases. ∎ + *Remarks.* The value 36 is attained by the trivial decoder (`c5.E6`, `M = I`, a different realisation). (RECORDED, not re-run: the working notes' floating-point search found 5,208 exact 7-term decompositions with deficient `x_j, y_j`, the best of cost 40, consistent with the above; #2240 / #2247 report minimum 40 / 37 for their finite alphabets.) + +**Theorem 7.4 (D5 ≥ 20 for every `m`) — PROVEN from CHECKED data (Lemmas 7.1, 7.2 for D5).** Every root-code decoder of D5 with dense `B` costs `≥ 20`. +*Proof.* Each term has rank `≥ 3`, with equality iff `x_j = e_a`, `y_j = e_b` with `a ≠ b` (both deficient, unmatched); all other terms have rank `≥ 4`. Let `n₃` be the number of rank-3 terms. Cost `≤ 19` needs `3 n₃ + 4(m − n₃) ≤ 19`, i.e. `n₃ ≥ 4m − 19`; with `n₃ ≤ m` this gives `m ≤ 6`, and `m ≥ 5` is forced. *`m = 5`* (square): `n₃ ≥ 1` is impossible, since a rank-3 term has `⟨y_i, x_i⟩ = ⟨e_b, e_a⟩ = 0`, contradicting `⟨y_i, x_i⟩ = 1`. *`m = 6`*: `n₃ ≥ 5`. By OC(b), `Π = u wᵀ`; a rank-3 term `i` has `⟨y_i,x_i⟩ = 0`, so `u_i w_i = 1` (OC(c)), and for two rank-3 terms `i ≠ j`, `⟨y_i, x_j⟩ = −u_i w_j ≠ 0`, i.e. `b_i = a_j`. Three rank-3 terms `i, j, k` then give `a_j = b_i = a_k` and `a_i = b_j = a_k`, so `a_i = b_i`, a contradiction (`c1.d5core` checks that no three pairs `(a_i, b_i)`, `a_i ≠ b_i`, satisfy `b_i = a_j` for all `i ≠ j`); so `n₃ ≤ 2 < 5`. ∎ The value 20 is attained by the trivial decoder (`c5.D5`). An independent counting proof for D5 is in the working notes (RECORDED). + +## 8. Open next questions (ranked by what they would buy) + +1. **Arbitrary `B`, E8.** A per-term census of fitting minranks `fr(R_x, A_y)` over pairs of maximal-flat normals (E8 has 8 orbits of normals; only root × root is done, §9.3) plus a coupling argument (Lemma OC bounds how many terms with `fr = 8` can occur) would give E8 `≥ 72` for root-code decoders and arbitrary `B`. +2. **P112.** Exclude the extra 8 of the 16 uncertified classes in every rank-8 realisation (a stronger certificate than (c), e.g. two-step propagation); this gives P112 `≥ 64` for every rank-8 realisation. +3. **Rank `> T` realisations and factors outside `col M`** (the 9-term decoder of #1180 is the test case): the supports are hyperplane sections of a lifted configuration in `K^{dim col P}` and Lemma 5.2 does not apply. For E8-type units with live roots spanning `R^8`, #1224 and #1633 give structure (one-sided nine-term decoders are overcomplete representations; `s + t ≤ m − 8`), but no cost floor outside the root code is known to us; Lemma OC generalises to idempotents of the lifted configuration, but no cost bound is derived. +4. **E6 / D5 realisation-free.** Neither has a `T`-frame; a rank-5 realisation of E6 would give dense cost `≤ 35`. No such realisation is known; rigidity of the Gram point and global uniqueness at rank `T` are open. (A floating-point search of the working notes found none; not reproduced, not claimed.) +5. **A human proof of `mr₂(Γ̄_E6) = 7`** (SAT-1 is a DRAT certificate, not an argument; a 16-line sub-configuration already needs rank 7 in the working notes' minimisation), and the exact values of `mr₂(Γ_E6)`, `mr₂(Γ_E7)` (only lower bounds 7, 8 are proved), over `F2` and over larger fields of characteristic 2. +6. **A B-dependent proof.** SAT-2 says a B-independent shadow cannot certify E6 / E7 with `T` terms, and SAT-5 says a shared `B` defeats every per-term drop on 26 decoders; an argument that explains the second by using that one `B` serves all terms is missing. +7. **Does a sparser admissible `B` ever beat the dense value for a whole unit?** All evidence here (SAT-1, SAT-4, SAT-5) says no for the nine test units; Proposition 3.2 says this is exactly the question of whether `min_B c(B)` is attained at the dense `B`. + +## 9. SAT evidence (arbitrary pairings) + +Everything in this section is about **all admissible B** (not just the dense one). Standard facts used: (i) `rank_F2 X ≤ r` iff `X = U Vᵀ` with `U, V` having `r` columns; this is encoded with an AND per entry and an XOR chain (`lib/satgen.py`). (ii) **Symmetry breaking** is valid: if `C` is a set of rows/columns with `X[C,C] = I` (a clique of pairwise *non-orthogonal* lines for fitting problems, where `X_tt = 1`, `X_ts = 0`; a clique of pairwise *orthogonal* lines for the `Γ` problems), then `U[C]` has rank `|C|` and a change of basis `U ↦ UA`, `V ↦ VA^{-T}` of `F2^r` makes `U[C] = [I | 0]` (and `V[C] = [I | 0]` when `r = |C|`). Any clique may be chosen; we use several. (iii) Every UNSAT is a **DRAT proof** checked by `drat-trim` (built from the upstream source vendored in `research/p111-minrank-proof-reconciliation/vendor/drat-trim/`); every SAT answer is a **model** checked clause by clause. (iv) **Controls** (SAT at the known feasible rank, so the encoding is not vacuously unsatisfiable): E6 at rank 7, E8 / P104 / E7 frame blocks at their dense ranks, three E6 shared-B instances at the dense ranks (`jointctrl_d00/07/18`). +Solver: kissat 4.0.4 only. Every instance is regenerated by `sat/instances.py` (deterministic); `sat/results.jsonl` and `sat/joint_results.jsonl` record the sha256 of its DIMACS text, the status, and the DRAT verdict; `c6` regenerates all 1,473 and compares. Proof files: the 44 DRAT proofs of the primary instances other than the two E6 `Γ` ones are shipped (`sat/proofs/*.drat.xz`, 2 MB compressed), with all 55 primary CNFs (`sat/cnf/*.cnf.xz`) and the 9 SAT models (`sat/models/`); the two E6 `Γ` proofs (about 90 MB each) and the 1,418 shared-B / floor proofs (about 600 MB in total, each ≤ 2.5 MB) are **not** shipped: regenerate with `python3 sat/run.py solve OUT NAME...` (`kissat` and `drat-trim` on `PATH`; sub-second per shared-B instance) and verify with `drat-trim OUT/NAME.cnf OUT/NAME.drat`. All of them were solved and DRAT-verified by the author (`seconds` and `proof_bytes` in the results files). + +### 9.1 SAT-1: the smallest rank of an admissible B on E6 is 7 — CHECKED +`e6glob_r5_c{0,1,2}`, `e6glob_r6_c{0,1,2}`: UNSAT (three different 5-cliques of pairwise non-orthogonal lines); `e6glob_r7_c0`: SAT (model checked). So **every** admissible `B` on the 36 E6 lines has rank `≥ 7` (the 5-clique already forces `≥ 5`), and the dense `B` attains 7. Note `ω(Γ) = 5 < 7`, so this is not a clique bound. Meaning: a decoder cannot lower its cost below `m · 7` by using a globally low-rank `B` (the bound "cost ≤ m · rank B" is useless below 42 for `m = 6`). + +### 9.2 SAT-2: B-independent shadows cannot certify E6 or E7 — E7 CHECKED (shipped DRAT), E6 RECORDED (DRAT-verified at generation), consequence PROVEN +**Shadow Lemma — PROVEN** (this is Lemma CR2 / `hadamard_diag_rank_sum` of #2162, `lean/DecoderDuality.lean`; rectangular Lean form in #2267; cited, not shipped). For any field `L ⊇ F2`, `x_j, y_j ∈ L^v` with `supp x_j ⊆ R_j`, `supp y_j ⊆ A_j`, and `N := Σ_j x_j y_jᵀ`: for every admissible `B`, **cost ≥ rank_L(B ∘ N)**. *Proof:* `B ∘ N = Σ_j D(x_j) B D(y_j)` and each summand factors through `B[R_j, A_j]`, so has rank `≤ rank_F2 B[R_j,A_j]` (rank is invariant under field extension); rank is subadditive. If moreover `N` vanishes on every orthogonal pair, `B ∘ N` is diagonal (a non-orthogonal pair has `B_ts = 0`), so **cost ≥ #{t : N_tt ≠ 0} for every B**. +A shadow `N` certifying all `v` lines with `m` terms is a matrix of rank `≤ m` over `L` with nonzero diagonal vanishing on orthogonal pairs. Over `L = F2` this is a matrix of rank `≤ m` with unit diagonal and zeros on orthogonal pairs: its minimum rank is `mr₂(Γ)`. **E6 RECORDED** (DRAT-verified at generation; the two ~90 MB proofs are not shipped, `verify.sh` checks the CNF hashes and verdicts) **and E7 CHECKED:** `gamma_E6_r6_c{0,1}` UNSAT (so `mr₂(Γ_E6) ≥ 7 > 6 = T`) and `gamma_E7_r7_c{0,1}` UNSAT (`mr₂(Γ_E7) ≥ 8 > 7 = T`); symmetry-breaking cliques of pairwise orthogonal lines (E6 has `α_⊥ = 4`). **PROVEN consequence:** for square decoders (`m = T`) no **F2-valued, B-independent** Shadow-Lemma certificate certifies all lines of E6 or of E7. Larger fields of characteristic 2 are not covered (OPEN, §8.5). The E-type floors for arbitrary `B`, if true, need an argument using that one `B` is shared. + +### 9.3 SAT-3: per-term drops — CHECKED +`e6term_r4` (SAT) and `e6term_r3` (UNSAT): a pair of deficient directions with dense rank 6 and `|R ∩ A| = 8` has fitting minrank exactly 4 over all admissible `B`. E8 root blocks (`e8blk_*`, any `B`): `fr(R_α, R_α) ≥ 9` and `fr(R_α, R_β) ≥ 9` for non-orthogonal `α, β` (UNSAT at 8); `fr(R_α, R_β) ≤ 8` for orthogonal `α, β` (SAT). So per-term monotonicity in `B` fails (a sparser `B` can lower a *single* term) — which is what makes SAT-5 informative. + +### 9.4 SAT-4: the known optimal decoders are B-robust — CHECKED +For each of the following terms the F2-fitting minrank over all admissible `B` equals the dense rank (UNSAT at dense − 1; SAT at the dense rank for the controls): E8 frame-normal decoder, 8 terms (dense 9); E8 coordinate decoder, terms 0 and 7 (78 lines each; dense 9; the other coordinates are equivalent under coordinate permutations of E8); E7 frame decoder, 7 terms (dense 7); P112 removed-frame decoder, 8 terms (dense 8); P104 frame-pair decoder, 8 terms (dense 7). So **no admissible `B` lowers the cost of these decoders** (72, 49, 64, 56), i.e. the sharp dense values are also robust to the choice of `B` *for these decoders*. (This is a statement about those decoders, not a lower bound for the unit.) + +### 9.5 SAT-5: a shared B does not rescue per-term drops on E6 — RECORDED (DRAT-verified at generation; CNF hashes and verdicts checked by verify.sh) +`data/e6_square_decoders.json` lists 26 square (`m = 6`) root-code decoders of E6 (found by hill climbing over bases of normals of maximal flats; dense costs 38 to 41). For each decoder `d` and term `j` let `lo_j` be the F2-fitting minrank of `B[R_j, A_j]` over all admissible `B` (computed with kissat from the dense rank downwards; each `lo_j > 1` is backed by an UNSAT instance `floor_dXX_tY` at rank `lo_j − 1`, DRAT-verified; 156 of them). Every admissible `B` has `rank B[R_j,A_j] ≥ lo_j`, and `Σ_j lo_j ≤ 35` for all 26 decoders. If some `B` had total cost `≤ 35`, then with `c_j := rank B[R_j,A_j] ≥ lo_j` and `Σ c_j ≤ 35` we may enlarge the `c_j` to reach `Σ = 35`; `B` then satisfies `rank B[R_j,A_j] ≤ c_j` for **a** cap vector `c ≥ lo` with `Σ c = 35`. So it suffices to refute each such cap vector with the shared variables (`B` entries on orthogonal pairs shared by all six blocks): **1,262 instances** (`joint_dXX_c1-…-c6`; 1, 6, 21, 56, 126 or 252 per decoder), **all UNSAT, all DRAT-verified**. Controls: with the dense ranks as caps the instances are SAT (`jointctrl_*`). So **no admissible `B` brings any of these 26 decoders to cost `≤ 35`**, although the sums of their per-term floors are as low as 30. Scope: those 26 decoders only. + +## 10. What was *not* reproduced, and discrepancies +`verify.sh` reproduces every CHECKED number above. Items quoted from other PRs or from the working notes are marked RECORDED in place and are not claimed. The earlier helper `mrsub.py` of the working notes reports solver timeouts as SAT and was **not** used; all SAT / UNSAT verdicts here come from `sat/run.py`, which records `UNKNOWN` / `TIMEOUT` separately (there are none). diff --git a/research/overcomplete-rank-interface/vendor/pr2277/lean/Overcomplete.lean b/research/overcomplete-rank-interface/vendor/pr2277/lean/Overcomplete.lean new file mode 100644 index 0000000000..58d9d97a92 --- /dev/null +++ b/research/overcomplete-rank-interface/vendor/pr2277/lean/Overcomplete.lean @@ -0,0 +1,46 @@ +import Mathlib + +/-! +# Lemma OC (overcomplete coupling), IDEAL2 §2.1 + +If `X : T × m` and `Y : T × m` satisfy `X * Yᵀ = 1` (an `m`-term exact decomposition of the +identity, `Σⱼ xⱼ yⱼᵀ = I_T`), then the `m × m` cross matrix `K = Yᵀ * X` (entries `⟨y_i, x_j⟩`) is +idempotent with trace `T`; hence `Π = 1 - K` is idempotent with trace `m - T`. +-/ + +open Matrix +set_option linter.unusedSectionVars false + +namespace DecoderDuality + +variable {K : Type*} [Field K] {T m : Type*} [Fintype T] [Fintype m] [DecidableEq T] [DecidableEq m] + +theorem oc_idempotent (X Y : Matrix T m K) (h : X * Yᵀ = 1) : + (Yᵀ * X) * (Yᵀ * X) = Yᵀ * X := by + calc (Yᵀ * X) * (Yᵀ * X) = Yᵀ * (X * Yᵀ) * X := by simp only [Matrix.mul_assoc] + _ = Yᵀ * X := by rw [h, Matrix.mul_one] + +theorem oc_trace (X Y : Matrix T m K) (h : X * Yᵀ = 1) : + (Yᵀ * X).trace = (Fintype.card T : K) := by + rw [Matrix.trace_mul_comm, h, Matrix.trace_one] + +theorem oc_complement_idempotent (X Y : Matrix T m K) (h : X * Yᵀ = 1) : + (1 - Yᵀ * X) * (1 - Yᵀ * X) = 1 - Yᵀ * X := by + have hK := oc_idempotent X Y h + rw [sub_mul, mul_sub, mul_sub, Matrix.one_mul, Matrix.mul_one, Matrix.one_mul, hK] + abel + +theorem oc_complement_trace (X Y : Matrix T m K) (h : X * Yᵀ = 1) : + (1 - Yᵀ * X).trace = (Fintype.card m : K) - (Fintype.card T : K) := by + rw [Matrix.trace_sub, Matrix.trace_one, oc_trace X Y h] + +/-- Square case (biorthogonality): if moreover `Yᵀ * X` has an inverse-side identity, it is `1`. +For `m = T` with `X * Yᵀ = 1` we get `Yᵀ * X = 1`, i.e. `⟨y_i, x_j⟩ = δ_ij`. -/ +theorem oc_square (X Y : Matrix T T K) (h : X * Yᵀ = 1) : Yᵀ * X = 1 := + mul_eq_one_comm.mp h + +end DecoderDuality + +#print axioms DecoderDuality.oc_idempotent +#print axioms DecoderDuality.oc_complement_trace +#print axioms DecoderDuality.oc_square diff --git a/research/overcomplete-rank-interface/vendor/pr2277/lean/lake-manifest.json b/research/overcomplete-rank-interface/vendor/pr2277/lean/lake-manifest.json new file mode 100644 index 0000000000..94973914f6 --- /dev/null +++ b/research/overcomplete-rank-interface/vendor/pr2277/lean/lake-manifest.json @@ -0,0 +1,117 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "55b7917b472489c7c56a0fa6393af05cfd536599", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "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": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "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": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "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": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "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": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "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": "2c810760f0a0c4536b397dbe30ca9b2f2f467366", + "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": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0-rc1", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "Overcomplete", + "lakeDir": ".lake", + "fixedToolchain": false +} \ No newline at end of file diff --git a/research/overcomplete-rank-interface/vendor/pr2277/lean/lakefile.toml b/research/overcomplete-rank-interface/vendor/pr2277/lean/lakefile.toml new file mode 100644 index 0000000000..ae1ee720f1 --- /dev/null +++ b/research/overcomplete-rank-interface/vendor/pr2277/lean/lakefile.toml @@ -0,0 +1,9 @@ +name = "Overcomplete" +defaultTargets = ["Overcomplete"] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" + +[[lean_lib]] +name = "Overcomplete" diff --git a/research/overcomplete-rank-interface/vendor/pr2277/lean/lean-toolchain b/research/overcomplete-rank-interface/vendor/pr2277/lean/lean-toolchain new file mode 100644 index 0000000000..fd85b262bf --- /dev/null +++ b/research/overcomplete-rank-interface/vendor/pr2277/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.0-rc1 diff --git a/research/overcomplete-rank-interface/verify.py b/research/overcomplete-rank-interface/verify.py new file mode 100644 index 0000000000..1a2a8f73d9 --- /dev/null +++ b/research/overcomplete-rank-interface/verify.py @@ -0,0 +1,131 @@ +#!/usr/bin/env python3 +"""Independent exact finite checks; these are not a substitute for leancheck.py. + +Apache-2.0. Prepared for ywz65 with OpenAI Codex assistance. +""" +import argparse +from fractions import Fraction +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def authenticate(): + dependency = json.loads((HERE / 'DEPENDENCY.json').read_bytes()) + for row in dependency['files']: + data = (HERE / row['retained']).read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'predecessor source pin') + obj = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + require(obj == row['git_blob'], 'predecessor blob pin') + formal = json.loads((HERE / 'FORMAL-RESULT.json').read_bytes()) + require(hashlib.sha256((HERE / 'Coupling.lean').read_bytes()).hexdigest() + == formal['source_sha256'], 'formal source receipt pin') + require(formal['status'] == 'kernel-checked' and len(formal['audited_roots']) == 6, + 'formal receipt shape') + + +def field(p): + def f(x): + return Fraction(x) if not p else x % p + def inv(x): + return 1 / x if not p else pow(x, -1, p) + return f, inv + + +def rank(a, p): + f, inv = field(p) + a = [[f(x) for x in row] for row in a] + r = 0 + for c in range(len(a[0])): + pivot = next((i for i in range(r, len(a)) if a[i][c]), None) + if pivot is None: + continue + a[r], a[pivot] = a[pivot], a[r] + scale = inv(a[r][c]) + a[r] = [f(x * scale) for x in a[r]] + for i in range(len(a)): + if i != r: + scale = a[i][c] + a[i] = [f(x - scale * y) for x, y in zip(a[i], a[r])] + r += 1 + if r == len(a): + break + return r + + +def mul(a, b, p): + f, _ = field(p) + return [[f(sum(x * y for x, y in zip(row, col))) for col in zip(*b)] for row in a] + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def check(): + count = one_extra = 0 + for p in (0, 2, 3, 5): + f, inv = field(p) + for t in range(1, 5): + for extra in range(4): + m = t + extra + for seed in range(7): + a = [[f((i + 2) * (j + 3) + seed - 4) for j in range(extra)] for i in range(t)] + b = [[f((i + 3) * (j + 1) - seed + 2) for j in range(t)] for i in range(extra)] + ab = mul(a, b, p) if extra else [[f(0)] * t for _ in range(t)] + x = [row + ar for row, ar in zip(identity(t), a)] + yt = [[f(int(i == j) - ab[i][j]) for j in range(t)] for i in range(t)] + b + require(mul(x, yt, p) == identity(t), 'fixture exactness') + k = mul(yt, x, p) + d = [[f(int(i == j) - k[i][j]) for j in range(m)] for i in range(m)] + require(rank(x, p) == t and rank(k, p) == t and rank(d, p) == extra, + 'rank/corank interface') + require(mul(k, k, p) == k and mul(d, d, p) == d, 'idempotence') + if extra == 1: + i, j = next((i, j) for i in range(m) for j in range(m) if d[i][j]) + u = [d[q][j] for q in range(m)] + w = [f(d[i][q] * inv(d[i][j])) for q in range(m)] + require([[f(v * z) for z in w] for v in u] == d, 'outer product') + require(f(sum(v * z for v, z in zip(w, u))) == 1, 'normalization') + require(all(k[i][j] == f(-u[i] * w[j]) for i in range(m) for j in range(m) if i != j), + 'off-diagonal formula') + one_extra += 1 + count += 1 + # The finite-field control explains why trace alone is not the rank proof. + require(rank(identity(3), 2) == 3 and sum(identity(3)[i][i] for i in range(3)) % 2 == 1, + 'trace-one rank-three control') + require(rank([[0, 0], [0, 0]], 0) != 1, 'exactness omission control') + require(rank(identity(2), 0) != 1, 'two-extra complement control') + require(mul([[1, 1], [0, 0]], [[1, 1], [0, 0]], 0) == [[1, 1], [0, 0]], + 'nonsymmetric idempotent positive control') + return dict(schema_version=1, exact_fixtures=count, one_extra_fixtures=one_extra, + 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') + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path) + args = parser.parse_args() + if args.out: + require(not args.out.exists(), 'output already exists') + authenticate() + receipt = check() + if args.out: + with args.out.open('x', encoding='utf-8') as stream: + stream.write(json.dumps(receipt, indent=2) + '\n') + else: + require(receipt == json.loads((HERE / 'RESULT.json').read_bytes()), 'finite receipt differs') + print('PASS_OC_FINITE:', receipt['exact_fixtures'], 'fixtures;', receipt['one_extra_fixtures'], 'one-extra') + + +if __name__ == '__main__': + main()