From ed86bcbe8f728e5412a6ef8f1910bac38f073f51 Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 06:34:36 -0700 Subject: [PATCH] Formalize the paired-plane C5 Schur obstruction in Lean --- .../LEAN-CHECK.json | 36 ++ research/paired-plane-c5-schur-lean/README.md | 155 ++++++++ .../paired-plane-c5-schur-lean/RESULT.json | 344 ++++++++++++++++++ .../paired-plane-c5-schur-lean/SOURCES.json | 40 ++ .../paired-plane-c5-schur-lean/Schur.lean | 134 +++++++ research/paired-plane-c5-schur-lean/TASK.json | 86 +++++ .../paired-plane-c5-schur-lean/VERIFY.json | 34 ++ .../paired-plane-c5-schur-lean/check_lean.py | 73 ++++ .../test_boundary.py | 77 ++++ research/paired-plane-c5-schur-lean/verify.py | 165 +++++++++ 10 files changed, 1144 insertions(+) create mode 100644 research/paired-plane-c5-schur-lean/LEAN-CHECK.json create mode 100644 research/paired-plane-c5-schur-lean/README.md create mode 100644 research/paired-plane-c5-schur-lean/RESULT.json create mode 100644 research/paired-plane-c5-schur-lean/SOURCES.json create mode 100644 research/paired-plane-c5-schur-lean/Schur.lean create mode 100644 research/paired-plane-c5-schur-lean/TASK.json create mode 100644 research/paired-plane-c5-schur-lean/VERIFY.json create mode 100644 research/paired-plane-c5-schur-lean/check_lean.py create mode 100644 research/paired-plane-c5-schur-lean/test_boundary.py create mode 100644 research/paired-plane-c5-schur-lean/verify.py diff --git a/research/paired-plane-c5-schur-lean/LEAN-CHECK.json b/research/paired-plane-c5-schur-lean/LEAN-CHECK.json new file mode 100644 index 0000000000..820b06c95e --- /dev/null +++ b/research/paired-plane-c5-schur-lean/LEAN-CHECK.json @@ -0,0 +1,36 @@ +{ + "status": "PASS_PAIRED_C5_LEAN", + "version": "Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)", + "source_sha256": "0e714c6f64ac8895080959babb8595ba7bdb391e43a2cee6be51d81690f56db0", + "theorem_axioms": { + "reverse_inverse": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "no_four_pivot": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "relaxed_diagonal": [ + "propext" + ], + "relaxed_remaining_zeros": [ + "propext" + ], + "relaxed_four_pivot": [ + "propext" + ], + "relaxed_missing_edge": [ + "propext" + ] + }, + "rejected_mutations": [ + "wrong_reversed_inverse", + "zero_diagonal", + "drop_nontriviality", + "free_B_D" + ], + "scope": "C5 normalized-four-pivot obstruction and integer one-edge-relaxed counterexample; no formal matrix rank bridge." +} diff --git a/research/paired-plane-c5-schur-lean/README.md b/research/paired-plane-c5-schur-lean/README.md new file mode 100644 index 0000000000..1e8ebb780b --- /dev/null +++ b/research/paired-plane-c5-schur-lean/README.md @@ -0,0 +1,155 @@ +# Lean core for the paired-plane C5 Schur obstruction + +The C5 lower-bound proof in [PR2484](https://github.com/CrocSwap/integer-mult-bounds/pull/2484) +uses a square-block inverse step and a Schur factorization. This package +formalizes that precise algebraic interface in standalone **Lean 4.34.1 / Std**, +and binds its mask to the actual five planes in the predecessor certificate. + +The exact formal theorem is `PairedC5.no_four_pivot`: over any commutative ring +with `0 != 1`, a five-by-five matrix of two-by-two blocks with identity diagonal +blocks and the five C5 forbidden unordered block pairs cannot satisfy + +``` +M_ij = M_i0 M_0j + M_i2 M_2j for every i,j. (1) +``` + +This is the normalized four-scalar-pivot factorization through planes 0 and 2. +It is **not a theorem whose formal hypothesis is `rank(M)<=4`**: this standalone +file has no matrix-rank definition or Mathlib dependency. The standard +linear-algebra implication from rank at most four and an identity pivot to (1) +remains written mathematics. The full rank-49 result is credited to PR2484; +it is not newly claimed to be fully Lean-formalized. + +## Formal proof and boundary + +`Schur.lean` defines literal two-by-two matrices, addition and multiplication. +It proves associativity, identities and zero laws from the commutative-ring +axioms. The square-block direct-finiteness theorem + +``` +XY = I_2 => YX = I_2 +``` + +is proved algebraically, not assumed. It supplies the right cancellation step +needed by the Schur proof. This avoids silently using rectangular one-sided +inverses as if they were square. + +Write the five planes in cycle order as A,B,C,D,E. Their diagonal blocks are +`I_2`; the forbidden unordered pairs are AC, AD, BD, BE and CE. Equation (1) +at DD and EE gives + +``` +M_DC M_CD = I_2, M_EA M_AE = I_2. +``` + +At BD and BE it gives `M_BC M_CD=0` and `M_BA M_AE=0`. The proved inverse and +cancellation lemmas force `M_BC=M_BA=0`. Equation (1) at BB would then make +`I_2=0`, contradicting nontriviality of the coefficient ring. No symmetry, +ordering, characteristic restriction, chosen scalar coefficients or numerical +rank computation is assumed. + +Four further Lean theorems check a concrete **integer** boundary witness: +free the BD pair, assign A/E one pair of coordinates and B/C/D the other pair. +The resulting ten-by-ten matrix has identity diagonal blocks, every other +required zero block, and the exact four-pivot factorization. Its BD and DB +blocks are `I_2`. This is a valid factorization of the relaxed mask, not a +counterexample to the strict-mask theorem. The same literal 0/1 matrix also +works over the rationals. + +## Binding to the source mask + +The external Python checker authenticates the selected source archive, its +`DATA-PHASES.json` member and the PR1825 matching fixture before parsing them. +It reconstructs all 56 complete four-element binary plane spans and their +orthogonality, importing no predecessor executable. It verifies the exact +PR2484 core + +``` +(13,23,35,16,34) +``` + +in that cycle order. Its ten scalar ports have exactly the formal `Far` +predicate's 40 forced off-diagonal scalar zeros, plus identity diagonal blocks. +It also checks the predecessor's 22-plane nonorthogonal clique and all core +cross pairs. Those 44 ports give `I_44`, with 880 forced zero cross entries, +so the 54-port principal submatrix is `I_44 (+) M`. + +The usual field argument then gives the predecessor's lower bound: rank at +most four for M, together with its I4 pivot, implies (1), contradicted by the +formal core; hence `rank(M)>=5` and the full fitting matrix has rank at least +49. **The field-rank bridge, rank monotonicity/additivity and Python-to-Lean +source correspondence are external to the Lean theorem.** The Python check +certifies the finite mask premises; it does not turn them into imported Lean +constants or prove the rank bridge. + +The credited rank-49 upper bound, fractional colouring and graph optima are not +rerun here: they are unnecessary for this formal-interface contribution. +This addresses PR2484's stated unformalized-lemma boundary rather than adding +another equivalent finite rank search. + +## Reproduce and validation status + +Fresh formal kernel check, including axiom inventory and four deliberately +false weakened/mutated statements: + +```sh +python3.12 -I -B research/paired-plane-c5-schur-lean/check_lean.py --lean /path/to/lean-4.34.1/bin/lean +``` + +This command actually ran locally with Lean 4.34.1 and CPython 3.12.14. All six +named theorems compiled, using only the ordinary `propext`, `Classical.choice` +and `Quot.sound` axioms (the concrete boundary theorems use only `propext`). +No `sorry`, extra axiom, `native_decide`, unsafe definition or untrusted tactic +result is admitted. Four mutations are rejected: wrong reverse inverse, +zero diagonal, absent nontriviality, and freeing BD. `LEAN-CHECK.json` records +the exact source hash and local result. It is a recorded receipt, not a +substitute for rerunning the command. + +Finite source-binding replay, standard library only: + +```sh +python3.12 -I -O -B research/paired-plane-c5-schur-lean/verify.py +python3.12 scripts/research_package.py --package research/paired-plane-c5-schur-lean +``` + +The registered Python hook checks the finite source binding and recorded formal +source hash; **it does not run Lean**. Its output states that distinction. +It also checks the entire receipt, literal relaxed factorization, modular +rank-four cross-checks and four rejecting controls. Boundary tests cover +unchanged Git-free export, altered formal source, wrong receipt, source drift, +and exclusive regeneration. `--out NEW.json` and the formal checker's optional +`--out NEW.json` both refuse to overwrite. On Windows, TEMP/TMP may need a +writable workspace directory. No selected supplier cold replay or hosted-CI +success is claimed. + +## Open next questions + +The next formal step is the field-rank-to-normalized-pivot lemma in a maintained +matrix library, followed by embedding this exact source mask and I44 block. +This package deliberately states that missing bridge as an obligation; it does +not claim a machine-checked rank-49 theorem. Separately, the native cost of +the 49 scalar channels remains open. None of the formal algebra prices COPY, +physical frames, dirty storage, hosting, precision, tape or all-size admission. +No new supplier, kappa or selected-frontier change is claimed. + +## Credit and provenance + +Base: canonical main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority four. +The fresh picker selected independent-verification/formal-interface-lemma. +[TASK.json](TASK.json) records the exact scope and overlap coverage; +[SOURCES.json](SOURCES.json) records source SHA256/Git bindings. + +Credit **thakrarsagar / PR2484** for the exact rank-49 result, C5 core, +22-plane clique and both written proofs, including the reviewer-suggested +Schur proof formalized here. Credit ywz65 / PR2471 for the preceding bracket, +Cinna Davis / PR1825 and PR2126 for the matched planes and scalar fit, Adam +Gall / PR1889 for the strict mask, Jeremy Diviney / PR2203 for the physical +payload distinction, Philippe Van Velzen and Josie Elliston / PR1977 for the +related plane and submatrix bounds. Frozen evidence remains unchanged. + +Prepared for **ywz65** with substantial OpenAI Codex assistance in formalization, +binding checks and exposition. A separate AI-assisted reviewer inspected the +typed statement, cancellation order, six audited theorem roots and stated +formal/external boundaries, with no actionable finding. Apache-2.0. No independent human review is +claimed. Lean kernel checking and external finite validation have the distinct +scopes stated above. diff --git a/research/paired-plane-c5-schur-lean/RESULT.json b/research/paired-plane-c5-schur-lean/RESULT.json new file mode 100644 index 0000000000..03fc5a67e5 --- /dev/null +++ b/research/paired-plane-c5-schur-lean/RESULT.json @@ -0,0 +1,344 @@ +{ + "scope": "External source binding to PairedC5.no_four_pivot; formal rank bridge excluded", + "source_hashes": { + "research/community-frontier1094-audit/selected-replay.tar.gz": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + }, + "member_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "core": [ + 13, + 23, + 35, + 16, + 34 + ], + "clique22": [ + 0, + 4, + 8, + 17, + 18, + 19, + 20, + 21, + 24, + 26, + 28, + 29, + 32, + 36, + 38, + 39, + 41, + 42, + 43, + 45, + 46, + 52 + ], + "core_ports": [ + 21, + 16, + 41, + 29, + 69, + 57, + 35, + 22, + 64, + 54 + ], + "clique_ports": [ + 0, + 1, + 80, + 6, + 79, + 10, + 53, + 18, + 55, + 20, + 47, + 25, + 24, + 19, + 91, + 26, + 39, + 27, + 96, + 43, + 86, + 37, + 88, + 34, + 87, + 44, + 102, + 58, + 92, + 48, + 62, + 52, + 94, + 61, + 95, + 65, + 97, + 60, + 111, + 67, + 106, + 68, + 100, + 74 + ], + "formal_far": [ + [ + false, + false, + true, + true, + false + ], + [ + false, + false, + false, + true, + true + ], + [ + true, + false, + false, + false, + true + ], + [ + true, + true, + false, + false, + false + ], + [ + false, + true, + true, + false, + false + ] + ], + "forced_zero_core_scalar_entries": 40, + "identity_block_scalar_dimension": 44, + "cross_forced_zero_entries": 880, + "relaxed_matrix": [ + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ] + ], + "relaxed_factor": [ + [ + 1, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0 + ], + [ + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 1, + 0 + ], + [ + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 1, + 0 + ], + [ + 0, + 0, + 0, + 1 + ], + [ + 1, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0 + ] + ], + "relaxed_rank_mod_2_3_101": [ + 4, + 4, + 4 + ], + "relaxed_only_violations": [ + [ + 1, + 3 + ], + [ + 3, + 1 + ] + ], + "controls": [ + "wrong cycle order", + "clique still internal but core cross edge changed", + "relaxed factorization passed as strict", + "matching drift" + ], + "formal_source_sha256": "0e714c6f64ac8895080959babb8595ba7bdb391e43a2cee6be51d81690f56db0", + "formal_status": "Source-bound recorded kernel run; run check_lean.py for a fresh Lean check." +} diff --git a/research/paired-plane-c5-schur-lean/SOURCES.json b/research/paired-plane-c5-schur-lean/SOURCES.json new file mode 100644 index 0000000000..95548030e4 --- /dev/null +++ b/research/paired-plane-c5-schur-lean/SOURCES.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f" + }, + { + "path": "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json", + "usage": "input", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11" + } + ], + "predecessors": [ + { + "pr": 2484, + "head": "4823273c8163e4c72472bdf7d42202e2c12d2e46", + "path": "research/paired-plane-minrank-bracket-audit/CERTIFICATE.json", + "git_blob": "393db5def16d76b3a0ebddc983c9bab6c3cc25fc", + "sha256": "6f5d3478290156c4fe703104572cc3aa593ad50079476ae08c942833714e3179", + "usage": "thakrarsagar C5 core and22clique certificate; literal constants are checked against pinned main geometry, no executable imported." + } + ] +} diff --git a/research/paired-plane-c5-schur-lean/Schur.lean b/research/paired-plane-c5-schur-lean/Schur.lean new file mode 100644 index 0000000000..569563457a --- /dev/null +++ b/research/paired-plane-c5-schur-lean/Schur.lean @@ -0,0 +1,134 @@ +/- Apache-2.0. Prepared for ywz65 with substantial OpenAI Codex assistance. + Formal Schur interface from thakrarsagar/PR2484's C5 proof. + This file does not define matrix rank or formalize the rank-to-pivot bridge. -/ +import Std + +namespace PairedC5 +open Lean.Grind + +structure Mat2 (K : Type) where + a : K + b : K + c : K + d : K + deriving DecidableEq + +variable {K : Type} [CommRing K] + +def mul (x y : Mat2 K) : Mat2 K := + ⟨x.a*y.a+x.b*y.c, x.a*y.b+x.b*y.d, + x.c*y.a+x.d*y.c, x.c*y.b+x.d*y.d⟩ +def one : Mat2 K := ⟨1,0,0,1⟩ +def zero : Mat2 K := ⟨0,0,0,0⟩ +def add (x y : Mat2 K) : Mat2 K := ⟨x.a+y.a,x.b+y.b,x.c+y.c,x.d+y.d⟩ + +theorem mul_assoc (x y z : Mat2 K) : mul (mul x y) z = mul x (mul y z) := by + cases x; cases y; cases z + simp only [mul, Mat2.mk.injEq] + grind + +@[simp] theorem mul_one (x : Mat2 K) : mul x one = x := by + cases x + simp only [mul, one, Mat2.mk.injEq] + grind + +@[simp] theorem one_mul (x : Mat2 K) : mul one x = x := by + cases x + simp only [mul, one, Mat2.mk.injEq] + grind + +@[simp] theorem mul_zero (x : Mat2 K) : mul x zero = zero := by + cases x + simp only [mul, zero, Mat2.mk.injEq] + grind + +@[simp] theorem zero_mul (x : Mat2 K) : mul zero x = zero := by + cases x + simp only [mul, zero, Mat2.mk.injEq] + grind + +@[simp] theorem add_zero (x : Mat2 K) : add x zero = x := by + cases x + simp only [add, zero, Mat2.mk.injEq] + grind + +@[simp] theorem zero_add (x : Mat2 K) : add zero x = x := by + cases x + simp only [add, zero, Mat2.mk.injEq] + grind + +/-- The square-block step cannot be replaced by rectangular one-sided inversion. -/ +theorem reverse_inverse (x y : Mat2 K) (h : mul x y = one) : mul y x = one := by + cases x; cases y + simp only [mul, one, Mat2.mk.injEq] at h ⊢ + grind + +theorem cancel_right_zero (x y z : Mat2 K) + (hinv : mul x y = one) (hzero : mul z y = zero) : z = zero := by + have rev := reverse_inverse x y hinv + calc + z = mul z (mul y x) := by rw [rev, mul_one] + _ = mul (mul z y) x := (mul_assoc z y x).symm + _ = zero := by rw [hzero, zero_mul] + +abbrev BlockMatrix (K : Type) := Fin 5 → Fin 5 → Mat2 K + +/-- Non-neighbouring planes of the orthogonality C5 have forced zero blocks. -/ +def Far (i j : Fin 5) : Prop := (i.val+2)%5 = j.val ∨ (j.val+2)%5 = i.val + +def Fits (m : BlockMatrix K) : Prop := + (∀ i, m i i = one) ∧ (∀ i j, Far i j → m i j = zero) + +/-- Schur factorization through the four scalar pivot ports in planes 0 and 2. -/ +def FourPivot (m : BlockMatrix K) : Prop := + ∀ i j, m i j = add (mul (m i 0) (m 0 j)) (mul (m i 2) (m 2 j)) + +/-- Exact formalized proposition: no fitting C5 matrix has the normalized + four-pivot factorization. Ordinary matrix rank is not a hypothesis here. -/ +theorem no_four_pivot (hne : (0 : K) ≠ 1) (m : BlockMatrix K) + (hfit : Fits m) (hf : FourPivot m) : False := by + rcases hfit with ⟨hd, hz⟩ + have h30 : m 3 0 = zero := hz 3 0 (by unfold Far; decide) + have h03 : m 0 3 = zero := hz 0 3 (by unfold Far; decide) + have h42 : m 4 2 = zero := hz 4 2 (by unfold Far; decide) + have h24 : m 2 4 = zero := hz 2 4 (by unfold Far; decide) + have h13 : m 1 3 = zero := hz 1 3 (by unfold Far; decide) + have h14 : m 1 4 = zero := hz 1 4 (by unfold Far; decide) + have d : mul (m 3 2) (m 2 3) = one := by + simpa [h30, hd 3] using (hf 3 3).symm + have e : mul (m 4 0) (m 0 4) = one := by + simpa [h42, hd 4] using (hf 4 4).symm + have bd : mul (m 1 2) (m 2 3) = zero := by + simpa [h13, h03] using (hf 1 3).symm + have be : mul (m 1 0) (m 0 4) = zero := by + simpa [h14, h24] using (hf 1 4).symm + have bc : m 1 2 = zero := cancel_right_zero _ _ _ d bd + have ba : m 1 0 = zero := cancel_right_zero _ _ _ e be + have contradiction : (one : Mat2 K) = zero := by + simpa [hd 1, ba, bc] using hf 1 1 + have scalar : (1 : K) = 0 := congrArg Mat2.a contradiction + exact hne scalar.symm + +/-- Concrete integer witness after freeing the B-D pair. Planes A,E share + two coordinates; B,C,D share the other two. -/ +def group (i : Fin 5) : Bool := i.val == 0 || i.val == 4 + +def relaxed : BlockMatrix Int := fun i j => if group i == group j then one else zero + +theorem relaxed_diagonal : ∀ i, relaxed i i = one := by decide + +theorem relaxed_remaining_zeros : ∀ i j, Far i j → + ¬ ((i = 1 ∧ j = 3) ∨ (i = 3 ∧ j = 1)) → relaxed i j = zero := by unfold Far; decide + +theorem relaxed_four_pivot : FourPivot relaxed := by unfold FourPivot; decide + +theorem relaxed_missing_edge : relaxed 1 3 = one ∧ relaxed 1 3 ≠ zero := by decide + +end PairedC5 + +#print axioms PairedC5.reverse_inverse +#print axioms PairedC5.no_four_pivot +#print axioms PairedC5.relaxed_diagonal +#print axioms PairedC5.relaxed_remaining_zeros +#print axioms PairedC5.relaxed_four_pivot +#print axioms PairedC5.relaxed_missing_edge diff --git a/research/paired-plane-c5-schur-lean/TASK.json b/research/paired-plane-c5-schur-lean/TASK.json new file mode 100644 index 0000000000..cb6e1c6d16 --- /dev/null +++ b/research/paired-plane-c5-schur-lean/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "refined", + "actual_scope": "Formalize the precise C5 normalized-four-pivot Schur obstruction and bind its mask to PR2484 source geometry; matrix-rank bridge remains external.", + "scope_change_reason": "Use explicit PR2484 unformalized-lemma handoff; new formal object and proof obligation, not another unchanged arithmetic replay.", + "bottleneck_link": "Certifies a missing universal algebra step behind the current49-channel scalar floor while separating it from native price and the full rank proof.", + "budget_minutes": 60, + "stop_rule": "Stop after kernel compilation, exact axiom inventory, strict/relaxed mask controls, source binding, read-only export and clearly stated rank-interface limit.", + "outcome": "completed", + "evidence": "Schur.lean; actual Lean4.34.1 check with4rejectedmutations and6theorems; source-bound core/I44 receipt; external boundary tests.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance for formalization, checking and writing. No independent human review.", + "selection": { + "nonce": "a390dd0a9cf41cfee6ad908e17a475cc", + "track": "independent-verification", + "scope_key": "e3ffea67887eeb4c396c" + }, + "open_questions": [ + { + "question": "Can a maintained matrix library discharge rank<=4 plus I4 pivot implies the normalized four-pivot equation and bind the actual source mask?", + "why_it_matters": "This would join the checked Schur core to a complete formal rank49 lower bound.", + "first_step": "Prove the field-rank-to-pivot lemma with explicit row/column injections, then instantiate it on the pinned10port core.", + "blocked_by": "Standalone Std development has no matrix-rank library or formal JSON source interpretation." + } + ], + "freshness": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/2484#issuecomment-6193177522", + "submission_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "submission_overlap": { + "open_prs": { + "fetched_at": "2026-10-15T13:33:30.360214+00:00", + "complete_pagination": true, + "records": 721 + }, + "discussions": { + "fetched_at": "2026-10-15T13:34:03.864146+00:00", + "complete_pagination": true, + "records": 1209 + } + }, + "warnings": [], + "overlap_tool": "Temporary copy of reviewed batched find_overlap.py at91156f0d41b133979c8004ad8d0f7e9f58d73cbc; canonical source unchanged.", + "validation": "Lean4.34.1 actual kernel run:6theorems,4false-premise controls; registered optimized CPython3.12 finite/export checks; separate AI source/proof review found no actionable issue." + } +} diff --git a/research/paired-plane-c5-schur-lean/VERIFY.json b/research/paired-plane-c5-schur-lean/VERIFY.json new file mode 100644 index 0000000000..3c80161158 --- /dev/null +++ b/research/paired-plane-c5-schur-lean/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "External finite mask/pivot/source binding and full receipt. Does not rerun Lean; recorded Lean source hash checked." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_boundary.py" + ], + "timeout_seconds": 120, + "checks": "Unchanged Git-free export; changed formal source, geometry, receipt, axiom inventory, missing proof receipt and exclusive output." + } + ] +} diff --git a/research/paired-plane-c5-schur-lean/check_lean.py b/research/paired-plane-c5-schur-lean/check_lean.py new file mode 100644 index 0000000000..77687896cf --- /dev/null +++ b/research/paired-plane-c5-schur-lean/check_lean.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Fresh Lean4.34.1 kernel check and actual false-premise controls; Apache-2.0.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import re +import subprocess +import tempfile + +HERE = Path(__file__).resolve().parent +THEOREMS = {'reverse_inverse', 'no_four_pivot', 'relaxed_diagonal', + 'relaxed_remaining_zeros', 'relaxed_four_pivot', 'relaxed_missing_edge'} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def run(lean, path): + return subprocess.run([str(lean), '-j1', str(path)], capture_output=True, + text=True, encoding='utf-8', timeout=90) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--lean', required=True, type=Path) + parser.add_argument('--out', type=Path) + args = parser.parse_args() + version = subprocess.check_output([str(args.lean), '--version'], text=True).strip() + need('version 4.34.1,' in version, 'Lean 4.34.1 required') + raw = (HERE/'Schur.lean').read_bytes() + source = raw.decode('utf-8') + bare = re.sub(r'/-.*?-/', '', source, flags=re.S) + bare = re.sub(r'--[^\n]*', '', bare) + need(not re.search(r'\b(sorry|admit|axiom|native_decide|implemented_by|unsafe)\b', bare), 'unsupported formal shortcut') + mutations = { + 'wrong_reversed_inverse': ('(h : mul x y = one) : mul y x = one', '(h : mul x y = one) : mul y x = zero'), + 'zero_diagonal': ('(∀ i, m i i = one)', '(∀ i, m i i = zero)'), + 'drop_nontriviality': ('(hne : (0 : K) ≠ 1)', '(hne : True)'), + 'free_B_D': ('(i.val+2)%5 = j.val ∨ (j.val+2)%5 = i.val', + '((i.val+2)%5 = j.val ∨ (j.val+2)%5 = i.val) ∧ ¬ ((i = 1 ∧ j = 3) ∨ (i = 3 ∧ j = 1))')} + with tempfile.TemporaryDirectory(prefix='paired-c5-lean-') as tmp: + path = Path(tmp)/'Schur.lean' + path.write_bytes(raw) + good = run(args.lean, path) + need(good.returncode == 0, good.stdout+good.stderr) + reports = re.findall(r"'PairedC5\.([^']+)' depends on axioms: \[([^\]]*)\]", good.stdout) + need(len(reports) == len(THEOREMS) and {name for name, _ in reports} == THEOREMS, 'exact formal theorem inventory') + axioms = {} + for name, report in reports: + values = sorted(v.strip() for v in report.split(',') if v.strip()) + need(set(values) <= {'propext', 'Classical.choice', 'Quot.sound'}, 'unexpected axiom: '+name) + axioms[name] = values + for label, (old, new) in mutations.items(): + need(source.count(old) == 1, 'mutation target: '+label) + path.write_text(source.replace(old, new), encoding='utf-8', newline='\n') + bad = run(args.lean, path) + need(bad.returncode != 0 and 'error' in bad.stdout, 'false statement/premise accepted: '+label) + receipt = {'status': 'PASS_PAIRED_C5_LEAN', 'version': version, + 'source_sha256': sha256(raw).hexdigest(), 'theorem_axioms': axioms, + 'rejected_mutations': list(mutations), + 'scope': 'C5 normalized-four-pivot obstruction and integer one-edge-relaxed counterexample; no formal matrix rank bridge.'} + if args.out: + with args.out.open('x', encoding='utf-8') as stream: + json.dump(receipt, stream, indent=2) + stream.write('\n') + print(json.dumps(receipt)) + + +if __name__ == '__main__': + main() diff --git a/research/paired-plane-c5-schur-lean/test_boundary.py b/research/paired-plane-c5-schur-lean/test_boundary.py new file mode 100644 index 0000000000..af2cab792b --- /dev/null +++ b/research/paired-plane-c5-schur-lean/test_boundary.py @@ -0,0 +1,77 @@ +#!/usr/bin/env python3 +"""Git-free source/evidence binding probes; these do not rerun Lean.""" +from hashlib import sha256 +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +REL = HERE.relative_to(ROOT) +INPUTS = ['research/community-frontier1094-audit/selected-replay.tar.gz', + 'research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json'] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def hashes(root): + return {str(p.relative_to(root)): sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + + +def run(root, success, reason='', extra=()): + p = subprocess.run([sys.executable, '-I', '-O', '-B', str(root/REL/'verify.py'), *map(str, extra)], + cwd=root, text=True, capture_output=True, timeout=45) + need((p.returncode == 0) == success and reason in p.stdout+p.stderr, 'unexpected result: '+p.stdout+p.stderr) + + +def main(): + with tempfile.TemporaryDirectory(prefix='paired-c5-export-') as tmp: + root = Path(tmp) + shutil.copytree(HERE, root/REL, ignore=shutil.ignore_patterns('__pycache__')) + for name in INPUTS: + (root/name).parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT/name, root/name) + before = hashes(root) + run(root, True) + need(hashes(root) == before, 'default replay changed export') + for name, reason in [(str(REL/'Schur.lean'), 'Lean receipt source binding'), + (INPUTS[1], 'source hash mismatch')]: + path = root/name + saved = path.read_bytes() + path.write_bytes(saved+b' ') + run(root, False, reason) + path.write_bytes(saved) + receipt = root/REL/'RESULT.json' + saved = receipt.read_bytes() + data = json.loads(saved) + data['identity_block_scalar_dimension'] = 46 + receipt.write_text(json.dumps(data)) + run(root, False, 'complete receipt mismatch') + receipt.write_bytes(saved) + formal = root/REL/'LEAN-CHECK.json' + saved_formal = formal.read_bytes() + data = json.loads(saved_formal) + data['theorem_axioms']['no_four_pivot'].append('sorryAx') + formal.write_text(json.dumps(data)) + run(root, False, 'recorded formal inventory') + formal.unlink() + run(root, False, 'LEAN-CHECK.json') + formal.write_bytes(saved_formal) + out = root/'new.json' + run(root, True, extra=('--out', out)) + need(json.loads(out.read_text()) == json.loads(saved), 'regeneration drift') + run(root, False, 'FileExistsError', extra=('--out', out)) + out.unlink() + need(hashes(root) == before, 'boundary probes failed to restore export') + print('PASS_PAIRED_C5_BOUNDARY git_free_unchanged=1 changed_source_and_receipts=5 exclusive_output=1') + + +if __name__ == '__main__': + main() diff --git a/research/paired-plane-c5-schur-lean/verify.py b/research/paired-plane-c5-schur-lean/verify.py new file mode 100644 index 0000000000..76425810dd --- /dev/null +++ b/research/paired-plane-c5-schur-lean/verify.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""External finite binding of the exact PR2484 mask to the formal C5 interface. +This Python replay does not execute Lean; use check_lean.py for a fresh kernel run. +Prepared for ywz65 with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from hashlib import sha256 +import io +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +MATCHING = 'research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json' +PINS = {ARCHIVE: 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6', + MATCHING: '4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1'} +MEMBER_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +CORE = [13, 23, 35, 16, 34] +CLIQUE = [0,4,8,17,18,19,20,21,24,26,28,29,32,36,38,39,41,42,43,45,46,52] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canon(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':')).encode() + + +def pinned(path, raw=None): + raw = (ROOT/path).read_bytes() if raw is None else raw + need(sha256(raw).hexdigest() == PINS[path], 'source hash mismatch: '+path) + return raw + + +def dot(x, y): + return (x & y).bit_count() % 2 + + +def load(): + archive, matching = pinned(ARCHIVE), pinned(MATCHING) + with tarfile.open(fileobj=io.BytesIO(archive), mode='r:gz') as tar: + handle = tar.extractfile(MEMBER) + need(handle is not None, 'missing source member') + raw = handle.read() + need(sha256(raw).hexdigest() == MEMBER_SHA, 'source member hash') + rows = sorted(json.loads(raw)['recipes'], key=lambda r: r['port']) + need([r['port'] for r in rows] == list(range(112)), 'port indexing') + labels = [r['q'] for r in rows] + need(len(set(labels)) == 112 and all(0 < q < 512 and dot(q, q) for q in labels), 'binary labels') + pairs = json.loads(matching)['matching'] + need(len(pairs) == 56 and sorted(v for pair in pairs for v in pair) == list(range(112)), 'matching partition') + need(all(len(p) == 2 and dot(labels[p[0]], labels[p[1]]) == 0 for p in pairs), 'nondegenerate plane bases') + planes = [{0, labels[a], labels[b], labels[a] ^ labels[b]} for a, b in pairs] + # Whole four-element spans, instead of trusting the predecessor's four basis pairings. + orth = [[i != j and all(dot(a, b) == 0 for a in planes[i] for b in planes[j]) + for j in range(56)] for i in range(56)] + return labels, pairs, orth + + +def check_binding(orth, core, clique): + need(len(core) == 5 and len(set(core)) == 5, 'core size') + need(len(clique) == 22 and len(set(clique)) == 22 and not set(core) & set(clique), 'clique size/disjointness') + need(all(orth[core[i]][core[j]] == ((i-j) % 5 in [1,4]) + for i in range(5) for j in range(5)), 'induced C5 in named cycle order') + need(all(not orth[a][b] for a in clique for b in clique if a != b), 'identity clique') + need(all(not orth[a][b] for a in clique for b in core), 'isolated core cross blocks') + + +def multiply(a, b): + return [[sum(x*y for x, y in zip(row, col)) for col in zip(*b)] for row in a] + + +def rank_mod(a, p): + rows = [[v % p for v in row] for row in a] + pos = 0 + for col in range(len(rows[0])): + pivot = next((i for i in range(pos, len(rows)) if rows[i][col]), None) + if pivot is None: + continue + rows[pos], rows[pivot] = rows[pivot], rows[pos] + scale = pow(rows[pos][col], -1, p) + rows[pos] = [(v*scale) % p for v in rows[pos]] + for i in range(len(rows)): + if i != pos: + scale = rows[i][col] + rows[i] = [(x-scale*y) % p for x, y in zip(rows[i], rows[pos])] + pos += 1 + return pos + + +def reject(action, label): + try: + action() + except ValueError: + return label + raise ValueError('negative control accepted: '+label) + + +def build(): + labels, pairs, orth = load() + check_binding(orth, CORE, CLIQUE) + # Match the formal definition exactly: two scalar entries per plane, identity diagonal blocks. + far = [[(i+2) % 5 == j or (j+2) % 5 == i for j in range(5)] for i in range(5)] + need(all(far[i][j] == (i != j and not orth[CORE[i]][CORE[j]]) + for i in range(5) for j in range(5)), 'formal Far predicate binding') + core_ports = [p for i in CORE for p in pairs[i]] + clique_ports = [p for i in CLIQUE for p in pairs[i]] + need(len(set(core_ports+clique_ports)) == 54, '54 distinct source ports') + # The relaxed witness is an integer Gram factorization with four columns. + groups = [0,1,1,1,0] + u = [[int(k == 2*groups[i]+j) for k in range(4)] for i in range(5) for j in range(2)] + m = multiply(u, list(map(list, zip(*u)))) + s = [0,1,4,5] + need([[m[i][j] for j in s] for i in s] == [[int(i == j) for j in range(4)] for i in range(4)], 'four pivot identity') + need(m == multiply([[row[j] for j in s] for row in m], [m[i] for i in s]), 'literal Schur boundary') + need(all(m[i][j] == int(i == j) for i in range(10) for j in range(10) if i//2 == j//2), 'boundary diagonal') + violations = [(i,j) for i in range(5) for j in range(5) if far[i][j] + and any(m[2*i+a][2*j+b] for a in range(2) for b in range(2))] + need(violations == [(1,3),(3,1)], 'exact missing edge') + need([rank_mod(m, p) for p in [2,3,101]] == [4]*3, 'boundary rank crosscheck') + controls = [reject(lambda: check_binding(orth, [CORE[1],CORE[0],*CORE[2:]], CLIQUE), 'wrong cycle order'), + reject(lambda: check_binding(orth, CORE, [22 if i == 20 else i for i in CLIQUE]), 'clique still internal but core cross edge changed'), + reject(lambda: need(not violations, 'strict mask fails'), 'relaxed factorization passed as strict'), + reject(lambda: pinned(MATCHING, pinned(MATCHING)+b' '), 'matching drift')] + # An ordinary full check may verify this local receipt but does not rerun Lean. + lean = json.loads((HERE/'LEAN-CHECK.json').read_text()) + formal_hash = sha256((HERE/'Schur.lean').read_bytes()).hexdigest() + need(lean['status'] == 'PASS_PAIRED_C5_LEAN' and lean['source_sha256'] == formal_hash, 'Lean receipt source binding') + names = {'reverse_inverse','no_four_pivot','relaxed_diagonal','relaxed_remaining_zeros','relaxed_four_pivot','relaxed_missing_edge'} + need(set(lean['theorem_axioms']) == names and all(set(v) <= {'propext','Classical.choice','Quot.sound'} + for v in lean['theorem_axioms'].values()), 'recorded formal inventory') + need('version 4.34.1,' in lean['version'] and lean['rejected_mutations'] == + ['wrong_reversed_inverse','zero_diagonal','drop_nontriviality','free_B_D'], 'recorded toolchain and controls') + return {'scope': 'External source binding to PairedC5.no_four_pivot; formal rank bridge excluded', + 'source_hashes': PINS, 'member_sha256': MEMBER_SHA, + 'core': CORE, 'clique22': CLIQUE, 'core_ports': core_ports, 'clique_ports': clique_ports, + 'formal_far': far, 'forced_zero_core_scalar_entries': sum(map(sum, far))*4, + 'identity_block_scalar_dimension': 44, 'cross_forced_zero_entries': 2*44*10, + 'relaxed_matrix': m, 'relaxed_factor': u, 'relaxed_rank_mod_2_3_101': [4,4,4], + 'relaxed_only_violations': violations, 'controls': controls, + 'formal_source_sha256': formal_hash, + 'formal_status': 'Source-bound recorded kernel run; run check_lean.py for a fresh Lean check.'} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path) + args = parser.parse_args() + result = build() + if args.out: + with args.out.open('x', encoding='utf-8') as stream: + json.dump(result, stream, indent=2) + stream.write('\n') + else: + need(canon(result) == canon(json.loads((HERE/'RESULT.json').read_text())), 'complete receipt mismatch') + print('PASS_PAIRED_C5_FINITE_BINDING planes=56 core_ports=10 isolated_identity=44 controls=4; not a fresh Lean run') + + +if __name__ == '__main__': + main()