From 985fd79ffea7ae7375fe6aa3ce9940b125c7dca2 Mon Sep 17 00:00:00 2001 From: Andrey Mas <67960725+an664@users.noreply.github.com> Date: Wed, 14 Oct 2026 07:57:23 +0400 Subject: [PATCH] formalize integral retraction and monomial bridge --- .../LICENSE | 202 +++ .../PR1497Bridge.lean | 1405 +++++++++++++++++ .../README.md | 130 ++ .../REPLAY.json | 1139 +++++++++++++ .../SCOPE.md | 193 +++ .../SOURCES.json | 56 + .../TASK.json | 72 + .../VERIFY.json | 18 + .../check_axioms.py | 73 + .../fixtures/Positive.lean | 252 +++ .../fixtures/RejectMissingMP.lean | 5 + .../fixtures/RejectMissingQP.lean | 5 + .../fixtures/RejectWrongW.lean | 5 + .../replay.py | 102 ++ .../test_tooling.py | 123 ++ 15 files changed, 3780 insertions(+) create mode 100644 research/integral-retraction-monomial-bridge/LICENSE create mode 100644 research/integral-retraction-monomial-bridge/PR1497Bridge.lean create mode 100644 research/integral-retraction-monomial-bridge/README.md create mode 100644 research/integral-retraction-monomial-bridge/REPLAY.json create mode 100644 research/integral-retraction-monomial-bridge/SCOPE.md create mode 100644 research/integral-retraction-monomial-bridge/SOURCES.json create mode 100644 research/integral-retraction-monomial-bridge/TASK.json create mode 100644 research/integral-retraction-monomial-bridge/VERIFY.json create mode 100644 research/integral-retraction-monomial-bridge/check_axioms.py create mode 100644 research/integral-retraction-monomial-bridge/fixtures/Positive.lean create mode 100644 research/integral-retraction-monomial-bridge/fixtures/RejectMissingMP.lean create mode 100644 research/integral-retraction-monomial-bridge/fixtures/RejectMissingQP.lean create mode 100644 research/integral-retraction-monomial-bridge/fixtures/RejectWrongW.lean create mode 100644 research/integral-retraction-monomial-bridge/replay.py create mode 100644 research/integral-retraction-monomial-bridge/test_tooling.py diff --git a/research/integral-retraction-monomial-bridge/LICENSE b/research/integral-retraction-monomial-bridge/LICENSE new file mode 100644 index 0000000000..d645695673 --- /dev/null +++ b/research/integral-retraction-monomial-bridge/LICENSE @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/integral-retraction-monomial-bridge/PR1497Bridge.lean b/research/integral-retraction-monomial-bridge/PR1497Bridge.lean new file mode 100644 index 0000000000..950829a287 --- /dev/null +++ b/research/integral-retraction-monomial-bridge/PR1497Bridge.lean @@ -0,0 +1,1405 @@ +/- +Copyright (c) 2026 Andrey Mas and contributors. +SPDX-License-Identifier: Apache-2.0 + +PR1497 universal integral-retraction and monomial bridge. +TARGET: official Lean 4.30.0, commit + d024af099ca4bf2c86f649261ebf59565dc8c622 +Only import: Std. No package manager is needed. + +STATUS: Locally kernel checked with the exact compiler identified above. +The producer delivered source and diagnostic repairs without running Lean. +Subsequent local replay accepted the universal source, repaired fixtures, +and queried axiom census. See README.md and REPLAY.json for that evidence. + +Project credits: Andrey Mas / GPT6Pro for the PR1497 audit; +Brett Halligan (burntout76) and Ninefold for inherited PR1212; +DreamingOfClouds (PR717); themilkman216 (PR968). +Substantial AI mathematical/formalization assistance is disclosed in README.md. +Formalization assistance used GPT-6 Pro, as observed in the ChatGPT browser UI. + +All custom algebra structures below contain operations and ordinary algebra +laws only. Kernel/image equality, saturation, and reconstruction are theorems, +not fields. Independent test data is kept in fixtures/Positive.lean. +-/ +import Std + +set_option autoImplicit false +set_option maxRecDepth 4096 +set_option maxHeartbeats 2000000 + +namespace PR1497 + +universe u v w t + +/-! ## 1. Small, explicit abelian-group and homomorphism interfaces -/ + +structure AbGroup (A : Type u) where + zero : A + add : A → A → A + neg : A → A + add_assoc : ∀ a b c, add (add a b) c = add a (add b c) + zero_add : ∀ a, add zero a = a + add_zero : ∀ a, add a zero = a + add_comm : ∀ a b, add a b = add b a + neg_add : ∀ a, add (neg a) a = zero + add_neg : ∀ a, add a (neg a) = zero + +namespace AbGroup + +variable {A : Type u} (G : AbGroup A) + +def sub (a b : A) : A := G.add a (G.neg b) + +theorem add_left_cancel {a b c : A} + (h : G.add a b = G.add a c) : b = c := by + have h' := congrArg (fun x => G.add (G.neg a) x) h + simpa only [← G.add_assoc, G.neg_add, G.zero_add] using h' + +theorem add_right_cancel {a b c : A} + (h : G.add b a = G.add c a) : b = c := by + apply G.add_left_cancel (a := a) + calc + G.add a b = G.add b a := G.add_comm _ _ + _ = G.add c a := h + _ = G.add a c := G.add_comm _ _ + +theorem add_left_comm (a b c : A) : + G.add a (G.add b c) = G.add b (G.add a c) := by + rw [← G.add_assoc, G.add_comm a b, G.add_assoc] + +theorem add_four (a b c d : A) : + G.add (G.add a b) (G.add c d) = + G.add (G.add a c) (G.add b d) := by + rw [G.add_assoc a b (G.add c d), G.add_left_comm b c d, + ← G.add_assoc a c (G.add b d)] + +theorem neg_zero : G.neg G.zero = G.zero := by + calc + G.neg G.zero = G.add (G.neg G.zero) G.zero := (G.add_zero _).symm + _ = G.zero := G.neg_add _ + +theorem neg_neg (a : A) : G.neg (G.neg a) = a := by + apply G.add_right_cancel (a := G.neg a) + rw [G.neg_add, G.add_neg] + +theorem neg_add_distrib (a b : A) : + G.neg (G.add a b) = G.add (G.neg a) (G.neg b) := by + apply G.add_left_cancel (a := G.add a b) + rw [G.add_neg, G.add_four, G.add_neg, G.add_neg, G.zero_add] + +theorem sub_zero (a : A) : G.sub a G.zero = a := by + rw [sub, G.neg_zero, G.add_zero] + +theorem sub_self (a : A) : G.sub a a = G.zero := G.add_neg a + +theorem sub_add_cancel (a b : A) : G.add (G.sub a b) b = a := by + rw [sub, G.add_assoc, G.neg_add, G.add_zero] + +theorem add_sub_cancel (a b : A) : G.sub (G.add a b) b = a := by + rw [sub, G.add_assoc, G.add_neg, G.add_zero] + +theorem sub_eq_zero_iff (a b : A) : G.sub a b = G.zero ↔ a = b := by + constructor + · intro h + have h' := congrArg (fun x => G.add x b) h + simpa only [G.sub_add_cancel, G.zero_add] using h' + · intro h + subst b + exact G.sub_self a + +theorem eq_of_sub_eq (a b c : A) (h : G.sub a b = c) : + a = G.add b c := by + calc + a = G.add (G.sub a b) b := (G.sub_add_cancel a b).symm + _ = G.add c b := congrArg (fun x => G.add x b) h + _ = G.add b c := G.add_comm c b + +/-- Repeated addition, with the empty sum equal to zero. -/ +def nsmul (G : AbGroup A) : Nat → A → A + | 0, _ => G.zero + | n + 1, a => G.add (nsmul G n a) a + +/-- Ordinary integral multiple: negative coefficients use the group inverse. -/ +def zsmul : Int → A → A + | .ofNat n, a => G.nsmul n a + | .negSucc n, a => G.neg (G.nsmul (n + 1) a) + +theorem nsmul_zero (n : Nat) : G.nsmul n G.zero = G.zero := by + induction n with + | zero => rfl + | succ n ih => simp only [nsmul, ih, G.add_zero] + +theorem zsmul_zero (a : A) : G.zsmul 0 a = G.zero := rfl + +theorem zsmul_zero_right (k : Int) : G.zsmul k G.zero = G.zero := by + cases k with + | ofNat n => exact G.nsmul_zero n + | negSucc n => simp only [zsmul, G.nsmul_zero, G.neg_zero] + +theorem zsmul_one (a : A) : G.zsmul 1 a = a := by + change G.add G.zero a = a + exact G.zero_add a + +/-- A two-sided integer induction principle, proved from the constructors. -/ +theorem int_induction (C : Int → Prop) (h0 : C 0) + (up : ∀ k, C k → C (k + 1)) + (down : ∀ k, C k → C (k - 1)) (k : Int) : C k := by + cases k with + | ofNat n => + induction n with + | zero => exact h0 + | succ n ih => exact up (Int.ofNat n) ih + | negSucc n => + induction n with + | zero => exact down 0 h0 + | succ n ih => exact down (Int.negSucc n) ih + +theorem zsmul_succ (k : Int) (a : A) : + G.zsmul (k + 1) a = G.add (G.zsmul k a) a := by + cases k with + | ofNat n => rfl + | negSucc n => + cases n with + | zero => + change G.zero = G.add (G.neg (G.add G.zero a)) a + rw [G.zero_add, G.neg_add] + | succ n => + have hk : Int.negSucc (n + 1) + 1 = Int.negSucc n := by omega + rw [hk] + change G.neg (G.nsmul (n + 1) a) = + G.add (G.neg (G.add (G.nsmul (n + 1) a) a)) a + rw [G.neg_add_distrib (G.nsmul (n + 1) a) a, + G.add_assoc, G.neg_add a, G.add_zero] + +theorem zsmul_pred (k : Int) (a : A) : + G.zsmul (k - 1) a = G.add (G.zsmul k a) (G.neg a) := by + have hs := G.zsmul_succ (k - 1) a + have hk : (k - 1) + 1 = k := by omega + rw [hk] at hs + apply G.add_right_cancel (a := a) + calc + G.add (G.zsmul (k - 1) a) a = G.zsmul k a := hs.symm + _ = G.add (G.add (G.zsmul k a) (G.neg a)) a := by + rw [G.add_assoc, G.neg_add, G.add_zero] + +/-- The exponent-addition law is derived, not assumed. -/ +theorem zsmul_add (k l : Int) (a : A) : + G.zsmul (k + l) a = G.add (G.zsmul k a) (G.zsmul l a) := by + apply int_induction (fun j => + G.zsmul (k + j) a = G.add (G.zsmul k a) (G.zsmul j a)) + · rw [Int.add_zero, G.zsmul_zero, G.add_zero] + · intro j ih + have hk : k + (j + 1) = (k + j) + 1 := by omega + rw [hk, G.zsmul_succ (k + j) a, G.zsmul_succ j a, ih, G.add_assoc] + · intro j ih + have hk : k + (j - 1) = (k + j) - 1 := by omega + rw [hk, G.zsmul_pred (k + j) a, G.zsmul_pred j a, ih, G.add_assoc] + +end AbGroup + +structure Hom {A : Type u} {B : Type v} + (GA : AbGroup A) (GB : AbGroup B) where + run : A → B + map_zero : run GA.zero = GB.zero + map_add : ∀ a b, run (GA.add a b) = GB.add (run a) (run b) + +namespace Hom + +variable {A : Type u} {B : Type v} {C : Type w} +variable {GA : AbGroup A} {GB : AbGroup B} {GC : AbGroup C} + +def id (G : AbGroup A) : Hom G G where + run := fun a => a + map_zero := rfl + map_add := fun _ _ => rfl + +def comp (g : Hom GB GC) (f : Hom GA GB) : Hom GA GC where + run := fun a => g.run (f.run a) + map_zero := by rw [f.map_zero, g.map_zero] + map_add := by intro a b; rw [f.map_add, g.map_add] + +theorem ext (f g : Hom GA GB) (h : ∀ a, f.run a = g.run a) : f = g := by + cases f with + | mk ff f0 fa => + cases g with + | mk gg g0 ga => + have hf : ff = gg := funext h + cases hf + rfl + +theorem map_neg (f : Hom GA GB) (a : A) : + f.run (GA.neg a) = GB.neg (f.run a) := by + apply GB.add_right_cancel (a := f.run a) + rw [← f.map_add, GA.neg_add, f.map_zero, GB.neg_add] + +theorem map_sub (f : Hom GA GB) (a b : A) : + f.run (GA.sub a b) = GB.sub (f.run a) (f.run b) := by + rw [AbGroup.sub, f.map_add, f.map_neg, AbGroup.sub] + +theorem map_nsmul (f : Hom GA GB) (n : Nat) (a : A) : + f.run (GA.nsmul n a) = GB.nsmul n (f.run a) := by + induction n with + | zero => exact f.map_zero + | succ n ih => + simp only [AbGroup.nsmul, f.map_add, ih] + +theorem map_zsmul (f : Hom GA GB) (k : Int) (a : A) : + f.run (GA.zsmul k a) = GB.zsmul k (f.run a) := by + cases k with + | ofNat n => exact f.map_nsmul n a + | negSucc n => + simp only [AbGroup.zsmul, f.map_neg, f.map_nsmul] + +end Hom + +/-! ## 2. Finite sums, honest integer rows, and ordinary matrix products -/ + +/-- Sum over all of Fin n, in increasing coordinate order. -/ +def fsum {A : Type u} (G : AbGroup A) : + (n : Nat) → (Fin n → A) → A + | 0, _ => G.zero + | n + 1, f => G.add (f 0) (fsum G n (fun i => f i.succ)) + +namespace Finite + +variable {A : Type u} {B : Type v} (G : AbGroup A) + +theorem sum_congr {n : Nat} (f g : Fin n → A) + (h : ∀ i, f i = g i) : fsum G n f = fsum G n g := + congrArg (fsum G n) (funext h) + +theorem sum_zero (n : Nat) : fsum G n (fun _ => G.zero) = G.zero := by + induction n with + | zero => rfl + | succ n ih => simp only [fsum, ih, G.add_zero] + +theorem sum_add (n : Nat) (f g : Fin n → A) : + fsum G n (fun i => G.add (f i) (g i)) = + G.add (fsum G n f) (fsum G n g) := by + revert f g + induction n with + | zero => + intro f g + exact (G.add_zero G.zero).symm + | succ n ih => + intro f g + change G.add (G.add (f 0) (g 0)) + (fsum G n (fun i => G.add (f i.succ) (g i.succ))) = + G.add (G.add (f 0) (fsum G n (fun i => f i.succ))) + (G.add (g 0) (fsum G n (fun i => g i.succ))) + rw [ih] + exact G.add_four _ _ _ _ + +theorem sum_neg (n : Nat) (f : Fin n → A) : + fsum G n (fun i => G.neg (f i)) = G.neg (fsum G n f) := by + revert f + induction n with + | zero => + intro f + exact G.neg_zero.symm + | succ n ih => + intro f + change G.add (G.neg (f 0)) (fsum G n (fun i => G.neg (f i.succ))) = + G.neg (G.add (f 0) (fsum G n (fun i => f i.succ))) + rw [ih, G.neg_add_distrib] + +theorem sum_sub (n : Nat) (f g : Fin n → A) : + fsum G n (fun i => G.sub (f i) (g i)) = + G.sub (fsum G n f) (fsum G n g) := by + simp only [AbGroup.sub, sum_add, sum_neg] + +theorem sum_swap (n m : Nat) (f : Fin n → Fin m → A) : + fsum G n (fun i => fsum G m (fun j => f i j)) = + fsum G m (fun j => fsum G n (fun i => f i j)) := by + revert f + induction n with + | zero => + intro f + simp only [fsum, sum_zero] + | succ n ih => + intro f + change G.add (fsum G m (fun j => f 0 j)) + (fsum G n (fun i => fsum G m (fun j => f i.succ j))) = + fsum G m (fun j => G.add (f 0 j) + (fsum G n (fun i => f i.succ j))) + rw [sum_add, ih] + +theorem sum_single (n : Nat) (j : Fin n) (a : A) : + fsum G n (fun i => if i = j then a else G.zero) = a := by + revert j + induction n with + | zero => + intro j + exact (Nat.not_lt_zero j.val j.isLt).elim + | succ n ih => + intro j + refine Fin.cases ?_ (fun k => ?_) j + · simp only [fsum, eq_self, ite_true, Fin.succ_ne_zero, if_false, + sum_zero, G.add_zero] + · have h0 : (0 : Fin (n + 1)) ≠ k.succ := Ne.symm (Fin.succ_ne_zero k) + simp only [fsum, if_neg h0, Fin.succ_inj, ih, G.zero_add] + +theorem map_sum {GA : AbGroup A} {GB : AbGroup B} + (h : Hom GA GB) (n : Nat) (f : Fin n → A) : + h.run (fsum GA n f) = fsum GB n (fun i => h.run (f i)) := by + revert f + induction n with + | zero => + intro f + exact h.map_zero + | succ n ih => + intro f + change h.run (GA.add (f 0) (fsum GA n (fun i => f i.succ))) = + GB.add (h.run (f 0)) (fsum GB n (fun i => h.run (f i.succ))) + rw [h.map_add, ih] + +end Finite + +/-- This is the usual additive group of Lean's built-in integers. -/ +def intGroup : AbGroup Int where + zero := 0 + add := (· + ·) + neg := Neg.neg + add_assoc := Int.add_assoc + zero_add := Int.zero_add + add_zero := Int.add_zero + add_comm := Int.add_comm + neg_add := Int.add_left_neg + add_neg := Int.add_right_neg + +/-- Pointwise abelian group; in particular the group on Fin n → Int. -/ +def functionGroup {I : Type u} {A : Type v} (G : AbGroup A) : + AbGroup (I → A) where + zero := fun _ => G.zero + add := fun a b i => G.add (a i) (b i) + neg := fun a i => G.neg (a i) + add_assoc := by intro a b c; funext i; exact G.add_assoc _ _ _ + zero_add := by intro a; funext i; exact G.zero_add _ + add_zero := by intro a; funext i; exact G.add_zero _ + add_comm := by intro a b; funext i; exact G.add_comm _ _ + neg_add := by intro a; funext i; exact G.neg_add _ + add_neg := by intro a; funext i; exact G.add_neg _ + +abbrev Row (n : Nat) := Fin n → Int +abbrev Mat (m n : Nat) := Fin m → Fin n → Int + +def rowGroup (n : Nat) : AbGroup (Row n) := functionGroup intGroup + +def scale {n : Nat} (k : Int) (v : Row n) : Row n := fun i => k * v i + +def basis (n : Nat) (i : Fin n) : Row n := fun j => if j = i then 1 else 0 + +def eye (n : Nat) : Mat n n := fun i => basis n i + +def zeroMat (m n : Nat) : Mat m n := fun _ _ => 0 + +def matSub {m n : Nat} (A B : Mat m n) : Mat m n := fun i j => A i j - B i j + +/-- Ordinary row-vector multiplication: (v A)_j = sum_i v_i A_ij. -/ +def rowMul {m n : Nat} (v : Row m) (A : Mat m n) : Row n := + fun j => fsum intGroup m (fun i => v i * A i j) + +/-- Ordinary matrix multiplication, with the left index the row index. -/ +def matMul {m n d : Nat} (A : Mat m n) (B : Mat n d) : Mat m d := + fun i => rowMul (A i) B + +namespace Rows + +theorem sum_apply {I : Type u} {A : Type v} (G : AbGroup A) + (n : Nat) (f : Fin n → I → A) (j : I) : + (fsum (functionGroup G) n f) j = fsum G n (fun i => f i j) := by + revert f + induction n with + | zero => + intro f + rfl + | succ n ih => + intro f + change G.add (f 0 j) ((fsum (functionGroup G) n + (fun i => f i.succ)) j) = + G.add (f 0 j) (fsum G n (fun i => f i.succ j)) + rw [ih] + +theorem nsmul_apply {I : Type u} {A : Type v} (G : AbGroup A) + (n : Nat) (f : I → A) (j : I) : + ((functionGroup G).nsmul n f) j = G.nsmul n (f j) := by + induction n with + | zero => rfl + | succ n ih => + change G.add (((functionGroup G).nsmul n f) j) (f j) = + G.add (G.nsmul n (f j)) (f j) + rw [ih] + +theorem zsmul_apply {I : Type u} {A : Type v} (G : AbGroup A) + (k : Int) (f : I → A) (j : I) : + ((functionGroup G).zsmul k f) j = G.zsmul k (f j) := by + cases k with + | ofNat n => exact nsmul_apply G n f j + | negSucc n => + change G.neg (((functionGroup G).nsmul (n + 1) f) j) = + G.neg (G.nsmul (n + 1) (f j)) + rw [nsmul_apply] + +theorem int_nsmul (n : Nat) (a : Int) : + intGroup.nsmul n a = (n : Int) * a := by + induction n with + | zero => exact (Int.zero_mul a).symm + | succ n ih => + change intGroup.nsmul n a + a = ((n + 1 : Nat) : Int) * a + rw [ih, Int.natCast_succ, Int.add_mul, Int.one_mul] + +theorem int_zsmul (k a : Int) : intGroup.zsmul k a = k * a := by + cases k with + | ofNat n => exact int_nsmul n a + | negSucc n => + change -(intGroup.nsmul (n + 1) a) = Int.negSucc n * a + rw [int_nsmul] + change -(((n + 1 : Nat) : Int) * a) = -((n + 1 : Nat) : Int) * a + rw [Int.neg_mul] + +theorem row_zsmul {n : Nat} (k : Int) (v : Row n) : + (rowGroup n).zsmul k v = scale k v := by + funext i + exact (zsmul_apply intGroup k v i).trans (int_zsmul k (v i)) + +theorem sum_mul_right (n : Nat) (f : Fin n → Int) (a : Int) : + (fsum intGroup n f) * a = fsum intGroup n (fun i => f i * a) := by + revert f + induction n with + | zero => + intro f + exact Int.zero_mul a + | succ n ih => + intro f + change (f 0 + fsum intGroup n (fun i => f i.succ)) * a = + f 0 * a + fsum intGroup n (fun i => f i.succ * a) + rw [Int.add_mul, ih] + +theorem sum_mul_left (n : Nat) (a : Int) (f : Fin n → Int) : + a * fsum intGroup n f = fsum intGroup n (fun i => a * f i) := by + rw [Int.mul_comm a, sum_mul_right] + apply Finite.sum_congr + intro i + exact Int.mul_comm _ _ + +theorem rowMul_zero_left {m n : Nat} (A : Mat m n) : + rowMul (rowGroup m).zero A = (rowGroup n).zero := by + funext j + change fsum intGroup m (fun i => 0 * A i j) = 0 + simp only [Int.zero_mul] + exact Finite.sum_zero intGroup m + +theorem rowMul_zero_right {m n : Nat} (v : Row m) : + rowMul v (zeroMat m n) = (rowGroup n).zero := by + funext j + change fsum intGroup m (fun i => v i * 0) = 0 + simp only [Int.mul_zero] + exact Finite.sum_zero intGroup m + +theorem rowMul_add {m n : Nat} (v w : Row m) (A : Mat m n) : + rowMul ((rowGroup m).add v w) A = + (rowGroup n).add (rowMul v A) (rowMul w A) := by + funext j + change fsum intGroup m (fun i => (v i + w i) * A i j) = + fsum intGroup m (fun i => v i * A i j) + + fsum intGroup m (fun i => w i * A i j) + simp only [Int.add_mul] + exact Finite.sum_add intGroup m _ _ + +theorem rowMul_matSub {m n : Nat} (v : Row m) (A B : Mat m n) : + rowMul v (matSub A B) = + (rowGroup n).sub (rowMul v A) (rowMul v B) := by + funext j + change fsum intGroup m (fun i => v i * (A i j - B i j)) = + fsum intGroup m (fun i => v i * A i j) - + fsum intGroup m (fun i => v i * B i j) + simp only [Int.mul_sub] + exact Finite.sum_sub intGroup m _ _ + +/-- This is the row-orientation bridge, including interchange of finite sums. -/ +theorem rowMul_assoc {m n d : Nat} (v : Row m) + (A : Mat m n) (B : Mat n d) : + rowMul (rowMul v A) B = rowMul v (matMul A B) := by + funext j + change fsum intGroup n (fun k => + (fsum intGroup m (fun i => v i * A i k)) * B k j) = + fsum intGroup m (fun i => + v i * fsum intGroup n (fun k => A i k * B k j)) + calc + _ = fsum intGroup n (fun k => + fsum intGroup m (fun i => (v i * A i k) * B k j)) := by + apply Finite.sum_congr + intro k + exact sum_mul_right m _ _ + _ = fsum intGroup m (fun i => + fsum intGroup n (fun k => (v i * A i k) * B k j)) := + Finite.sum_swap intGroup n m _ + _ = fsum intGroup m (fun i => + fsum intGroup n (fun k => v i * (A i k * B k j))) := by + apply Finite.sum_congr + intro i + apply Finite.sum_congr + intro k + exact Int.mul_assoc _ _ _ + _ = _ := by + apply Finite.sum_congr + intro i + exact (sum_mul_left n (v i) _).symm + +theorem rowMul_basis {m n : Nat} (i : Fin m) (A : Mat m n) : + rowMul (basis m i) A = A i := by + funext j + change fsum intGroup m + (fun k => (if k = i then 1 else 0) * A k j) = A i j + calc + _ = fsum intGroup m (fun k => if k = i then A i j else 0) := by + apply Finite.sum_congr + intro k + by_cases h : k = i + · subst k; simp only [eq_self, ite_true, Int.one_mul] + · simp only [if_neg h, Int.zero_mul] + _ = _ := Finite.sum_single intGroup m i (A i j) + +theorem rowMul_eye {n : Nat} (v : Row n) : rowMul v (eye n) = v := by + funext j + change fsum intGroup n + (fun i => v i * (if j = i then 1 else 0)) = v j + calc + _ = fsum intGroup n (fun i => if i = j then v j else 0) := by + apply Finite.sum_congr + intro i + by_cases h : i = j + · subst i; simp only [eq_self, ite_true, Int.mul_one] + · simp only [if_neg h, if_neg (Ne.symm h), Int.mul_zero] + _ = _ := Finite.sum_single intGroup n j (v j) + +/-- Image of rowMul is exactly an integer combination of the individual rows. -/ +theorem rowMul_linear_combination {m n : Nat} (v : Row m) (A : Mat m n) : + rowMul v A = fsum (rowGroup n) m + (fun i => (rowGroup n).zsmul (v i) (A i)) := by + funext j + change fsum intGroup m (fun i => v i * A i j) = + (fsum (functionGroup intGroup) m + (fun i => (rowGroup n).zsmul (v i) (A i))) j + rw [sum_apply intGroup] + apply Finite.sum_congr + intro i + exact ((zsmul_apply intGroup (v i) (A i) j).trans + (int_zsmul (v i) (A i j))).symm + +/-- Actual matrix multiplication defines a homomorphism; no law is assumed. -/ +def rowHom {m n : Nat} (A : Mat m n) : Hom (rowGroup m) (rowGroup n) where + run := fun v => rowMul v A + map_zero := rowMul_zero_left A + map_add := fun v w => rowMul_add v w A + +end Rows + +/-! ## 3. Universal split-map theorem, with an image-difference quotient -/ + +/-- Exactly the three identities, in row-map order. -/ +structure Retraction {C : Type u} {A : Type v} {B : Type w} + (GC : AbGroup C) (GA : AbGroup A) (GB : AbGroup B) where + m : Hom GC GA + p : Hom GA GB + q : Hom GB GA + w : Hom GA GC + mp : ∀ c, p.run (m.run c) = GB.zero + qp : ∀ b, p.run (q.run b) = b + residual : ∀ a, GA.sub a (q.run (p.run a)) = m.run (w.run a) + +/-- A proved pair of inverse additive homomorphisms, not a hypothesis. -/ +structure AddIso {A : Type u} {B : Type v} + (GA : AbGroup A) (GB : AbGroup B) where + forward : Hom GA GB + backward : Hom GB GA + left_inverse : ∀ a, backward.run (forward.run a) = a + right_inverse : ∀ b, forward.run (backward.run b) = b + +/-- No nonzero integer annihilates a nonzero element. -/ +def TorsionFree {A : Type u} (G : AbGroup A) : Prop := + ∀ (k : Int), k ≠ 0 → ∀ a, G.zsmul k a = G.zero → a = G.zero + +namespace Retraction + +variable {C : Type u} {A : Type v} {B : Type w} +variable {GC : AbGroup C} {GA : AbGroup A} {GB : AbGroup B} +variable (s : Retraction GC GA GB) + +/-- The image of m, not the kernel of p by definition. -/ +def L (a : A) : Prop := ∃ c, s.m.run c = a + +theorem mem_image_iff (a : A) : s.L a ↔ s.p.run a = GB.zero := by + constructor + · intro h + cases h with + | intro c hc => + rw [← hc] + exact s.mp c + · intro h + have hr := s.residual a + rw [h, s.q.map_zero, GA.sub_zero] at hr + exact ⟨s.w.run a, hr.symm⟩ + +theorem image_eq_kernel : s.L = (fun a => s.p.run a = GB.zero) := by + funext a + exact propext (s.mem_image_iff a) + +theorem surjective : ∀ b, ∃ a, s.p.run a = b := by + intro b + exact ⟨s.q.run b, s.qp b⟩ + +theorem decomposition (a : A) : + a = GA.add (s.q.run (s.p.run a)) (s.m.run (s.w.run a)) := + GA.eq_of_sub_eq _ _ _ (s.residual a) + +/-- The literal lattice-coset relation: a - b lies in image(m). -/ +def Rel (a b : A) : Prop := s.L (GA.sub a b) + +theorem rel_iff (a b : A) : s.Rel a b ↔ s.p.run a = s.p.run b := by + unfold Rel + rw [s.mem_image_iff, s.p.map_sub] + exact GB.sub_eq_zero_iff _ _ + +def latticeSetoid : Setoid A where + r := s.Rel + iseqv := { + refl := by intro a; exact (s.rel_iff a a).mpr rfl + symm := by + intro a b hab + exact (s.rel_iff b a).mpr ((s.rel_iff a b).mp hab).symm + trans := by + intro a b c hab hbc + exact (s.rel_iff a c).mpr + (((s.rel_iff a b).mp hab).trans ((s.rel_iff b c).mp hbc)) + } + +abbrev LQuot := Quotient s.latticeSetoid + +def qmk (a : A) : s.LQuot := Quotient.mk s.latticeSetoid a + +/-- Well-definedness is the proved rel_iff, not an extra field. -/ +def qmap : s.LQuot → B := + Quotient.lift s.p.run (fun a b h => (s.rel_iff a b).mp h) + +def qinv (b : B) : s.LQuot := s.qmk (s.q.run b) + +theorem qmap_mk (a : A) : s.qmap (s.qmk a) = s.p.run a := rfl + +theorem qmap_qinv (b : B) : s.qmap (s.qinv b) = b := s.qp b + +theorem qinv_qmap (x : s.LQuot) : s.qinv (s.qmap x) = x := by + refine Quotient.inductionOn + (motive := fun q : s.LQuot => s.qinv (s.qmap q) = q) x ?_ + intro a + apply Quotient.sound + exact (s.rel_iff _ _).mpr (s.qp (s.p.run a)) + +theorem qmap_injective {x y : s.LQuot} (h : s.qmap x = s.qmap y) : x = y := by + calc + x = s.qinv (s.qmap x) := (s.qinv_qmap x).symm + _ = s.qinv (s.qmap y) := congrArg s.qinv h + _ = y := s.qinv_qmap y + +/-- Addition induced from representatives; both representative choices are checked. -/ +def qadd (x y : s.LQuot) : s.LQuot := + Quotient.liftOn₂ x y (fun a b => s.qmk (GA.add a b)) (by + intro a b c d hac hbd + apply Quotient.sound + apply (s.rel_iff _ _).mpr + rw [s.p.map_add, s.p.map_add, + (s.rel_iff a c).mp hac, (s.rel_iff b d).mp hbd]) + +def qneg (x : s.LQuot) : s.LQuot := + Quotient.liftOn x (fun a => s.qmk (GA.neg a)) (by + intro a b hab + apply Quotient.sound + apply (s.rel_iff _ _).mpr + rw [s.p.map_neg, s.p.map_neg, (s.rel_iff a b).mp hab]) + +theorem qmap_zero : s.qmap (s.qmk GA.zero) = GB.zero := s.p.map_zero + +theorem qmap_add (x y : s.LQuot) : + s.qmap (s.qadd x y) = GB.add (s.qmap x) (s.qmap y) := by + refine Quotient.inductionOn₂ + (motive := fun q r : s.LQuot => + s.qmap (s.qadd q r) = GB.add (s.qmap q) (s.qmap r)) x y ?_ + intro a b + exact s.p.map_add a b + +theorem qmap_neg (x : s.LQuot) : + s.qmap (s.qneg x) = GB.neg (s.qmap x) := by + refine Quotient.inductionOn + (motive := fun q : s.LQuot => + s.qmap (s.qneg q) = GB.neg (s.qmap q)) x ?_ + intro a + exact s.p.map_neg a + +/-- Every quotient-group axiom follows from the induced operations. -/ +def quotientGroup : AbGroup s.LQuot where + zero := s.qmk GA.zero + add := s.qadd + neg := s.qneg + add_assoc := by + intro x y z + apply s.qmap_injective + simp only [s.qmap_add] + exact GB.add_assoc _ _ _ + zero_add := by + intro x + apply s.qmap_injective + rw [s.qmap_add, s.qmap_zero, GB.zero_add] + add_zero := by + intro x + apply s.qmap_injective + rw [s.qmap_add, s.qmap_zero, GB.add_zero] + add_comm := by + intro x y + apply s.qmap_injective + rw [s.qmap_add, s.qmap_add, GB.add_comm] + neg_add := by + intro x + apply s.qmap_injective + rw [s.qmap_add, s.qmap_neg, s.qmap_zero, GB.neg_add] + add_neg := by + intro x + apply s.qmap_injective + rw [s.qmap_add, s.qmap_neg, s.qmap_zero, GB.add_neg] + +def quotientMap : Hom s.quotientGroup GB where + run := s.qmap + map_zero := s.qmap_zero + map_add := s.qmap_add + +def quotientInv : Hom GB s.quotientGroup where + run := s.qinv + map_zero := by + change s.qinv GB.zero = s.qmk GA.zero + apply s.qmap_injective + rw [s.qmap_qinv, s.qmap_zero] + map_add := by + intro x y + change s.qinv (GB.add x y) = s.qadd (s.qinv x) (s.qinv y) + apply s.qmap_injective + simp only [s.qmap_add, s.qmap_qinv] + +def quotientIso : AddIso s.quotientGroup GB where + forward := s.quotientMap + backward := s.quotientInv + left_inverse := s.qinv_qmap + right_inverse := s.qmap_qinv + +theorem saturated (hTF : TorsionFree GB) (k : Int) (hk : k ≠ 0) + (a : A) (ha : s.L (GA.zsmul k a)) : s.L a := by + apply (s.mem_image_iff a).mpr + apply hTF k hk (s.p.run a) + calc + GB.zsmul k (s.p.run a) = s.p.run (GA.zsmul k a) := + (s.p.map_zsmul k a).symm + _ = GB.zero := (s.mem_image_iff _).mp ha + +/-- Abstract character factorization; the finite-row theorem below proves + this annihilation hypothesis from the individual relation rows. -/ +theorem character_factor {D : Type t} {GD : AbGroup D} + (chi : Hom GA GD) (h : ∀ c, chi.run (s.m.run c) = GD.zero) + (a : A) : chi.run a = chi.run (s.q.run (s.p.run a)) := by + have hc := congrArg chi.run (s.residual a) + rw [chi.map_sub, h (s.w.run a)] at hc + exact (GD.sub_eq_zero_iff _ _).mp hc + +theorem character_unique {D : Type t} {GD : AbGroup D} + (chi : Hom GA GD) (psi : Hom GB GD) + (h : ∀ a, chi.run a = psi.run (s.p.run a)) (b : B) : + psi.run b = chi.run (s.q.run b) := by + have hb := h (s.q.run b) + rw [s.qp] at hb + exact hb.symm + +end Retraction + +/-! ## 4. The concrete integral-matrix instantiation -/ + +/-- The only certificate hypotheses. No geometry or hidden image assertions. -/ +structure MatrixIdentities {m N d : Nat} + (M : Mat m N) (P : Mat N d) (Q : Mat d N) (W : Mat N m) : Prop where + mp : matMul M P = zeroMat m d + qp : matMul Q P = eye d + residual : matSub (eye N) (matMul P Q) = matMul W M + +/-- Derives all three split-map identities from ordinary matrix equalities. -/ +def matrixRetraction {m N d : Nat} + {M : Mat m N} {P : Mat N d} {Q : Mat d N} {W : Mat N m} + (h : MatrixIdentities M P Q W) : + Retraction (rowGroup m) (rowGroup N) (rowGroup d) where + m := Rows.rowHom M + p := Rows.rowHom P + q := Rows.rowHom Q + w := Rows.rowHom W + mp := by + intro z + change rowMul (rowMul z M) P = (rowGroup d).zero + rw [Rows.rowMul_assoc, h.mp, Rows.rowMul_zero_right] + qp := by + intro z + change rowMul (rowMul z Q) P = z + rw [Rows.rowMul_assoc, h.qp, Rows.rowMul_eye] + residual := by + intro z + change (rowGroup N).sub z (rowMul (rowMul z P) Q) = + rowMul (rowMul z W) M + rw [Rows.rowMul_assoc z P Q, Rows.rowMul_assoc z W M] + calc + (rowGroup N).sub z (rowMul z (matMul P Q)) = + rowMul z (matSub (eye N) (matMul P Q)) := by + rw [Rows.rowMul_matSub, Rows.rowMul_eye] + _ = rowMul z (matMul W M) := congrArg (rowMul z) h.residual + +namespace MatrixBridge + +variable {m N d : Nat} +variable {M : Mat m N} {P : Mat N d} {Q : Mat d N} {W : Mat N m} + +/-- Image definition, with literal integer coefficients. -/ +def Lattice (v : Row N) : Prop := ∃ z : Row m, rowMul z M = v + +theorem lattice_iff_integer_span (v : Row N) : + Lattice (M := M) v ↔ ∃ z : Row m, + fsum (rowGroup N) m (fun r => (rowGroup N).zsmul (z r) (M r)) = v := by + constructor + · intro hv + cases hv with + | intro z hz => + exact ⟨z, (Rows.rowMul_linear_combination z M).symm.trans hz⟩ + · intro hv + cases hv with + | intro z hz => + exact ⟨z, (Rows.rowMul_linear_combination z M).trans hz⟩ + +theorem lattice_eq_kernel (h : MatrixIdentities M P Q W) + (v : Row N) : + Lattice (M := M) v ↔ rowMul v P = (rowGroup d).zero := + (matrixRetraction h).mem_image_iff v + +theorem lattice_eq_kernel_as_predicate (h : MatrixIdentities M P Q W) : + Lattice (M := M) = (fun v => rowMul v P = (rowGroup d).zero) := by + funext v + exact propext (lattice_eq_kernel h v) + +theorem quotient_relation (h : MatrixIdentities M P Q W) + (v w : Row N) : + (matrixRetraction h).Rel v w ↔ + ∃ z : Row m, rowMul z M = (fun i => v i - w i) := Iff.rfl + +theorem quotient_equal_iff (h : MatrixIdentities M P Q W) + (v w : Row N) : + (matrixRetraction h).qmk v = (matrixRetraction h).qmk w ↔ + Lattice (M := M) ((rowGroup N).sub v w) := by + constructor + · intro heq + exact Quotient.exact heq + · intro hrel + exact Quotient.sound hrel + +theorem phi_surjective (h : MatrixIdentities M P Q W) : ∀ z : Row d, ∃ v : Row N, rowMul v P = z := + (matrixRetraction h).surjective + +/-- The inverse representative is z Q; this is not an arbitrary chosen section. -/ +def quotientIso (h : MatrixIdentities M P Q W) : + AddIso (matrixRetraction h).quotientGroup (rowGroup d) := + (matrixRetraction h).quotientIso + +theorem quotient_forward_on_representative (h : MatrixIdentities M P Q W) + (v : Row N) : + (quotientIso h).forward.run ((matrixRetraction h).qmk v) = rowMul v P := rfl + +theorem quotient_inverse_on_parameter (h : MatrixIdentities M P Q W) + (z : Row d) : + (quotientIso h).backward.run z = + (matrixRetraction h).qmk (rowMul z Q) := rfl + +theorem quotient_left_inverse (h : MatrixIdentities M P Q W) + (x : (matrixRetraction h).LQuot) : + (quotientIso h).backward.run ((quotientIso h).forward.run x) = x := + (quotientIso h).left_inverse x + +theorem quotient_right_inverse (h : MatrixIdentities M P Q W) + (z : Row d) : + (quotientIso h).forward.run ((quotientIso h).backward.run z) = z := + (quotientIso h).right_inverse z + +/-- Concrete torsion-freeness, from integer multiplication having no zero divisors. -/ +theorem row_torsion_free (n : Nat) : TorsionFree (rowGroup n) := by + intro k hk v hv + rw [Rows.row_zsmul] at hv + funext i + have hi := congrArg (fun a : Row n => a i) hv + change k * v i = 0 at hi + exact (Int.mul_eq_zero.mp hi).resolve_left hk + +theorem lattice_saturated (h : MatrixIdentities M P Q W) + (k : Int) (hk : k ≠ 0) (v : Row N) + (hv : Lattice (M := M) (scale k v)) : Lattice (M := M) v := by + apply (matrixRetraction h).saturated (row_torsion_free d) k hk v + change Lattice (M := M) ((rowGroup N).zsmul k v) + rw [Rows.row_zsmul] + exact hv + +end MatrixBridge + +/-! ## 5. Lawful commutative groups, actual products, and signed powers -/ + +/-- No field, divisibility, roots, or characteristic hypotheses. -/ +structure CommGroup (D : Type u) where + one : D + mul : D → D → D + inv : D → D + mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c) + one_mul : ∀ a, mul one a = a + mul_one : ∀ a, mul a one = a + mul_comm : ∀ a b, mul a b = mul b a + inv_mul : ∀ a, mul (inv a) a = one + mul_inv : ∀ a, mul a (inv a) = one + +namespace CommGroup + +variable {D : Type u} (G : CommGroup D) + +/-- Only a change of notation: addition is multiplication, negation is inverse. -/ +def asAdd : AbGroup D where + zero := G.one + add := G.mul + neg := G.inv + add_assoc := G.mul_assoc + zero_add := G.one_mul + add_zero := G.mul_one + add_comm := G.mul_comm + neg_add := G.inv_mul + add_neg := G.mul_inv + +def npow (a : D) (n : Nat) : D := G.asAdd.nsmul n a + +def zpow (a : D) (k : Int) : D := G.asAdd.zsmul k a + +def prod (n : Nat) (f : Fin n → D) : D := fsum G.asAdd n f + +def div (a b : D) : D := G.mul a (G.inv b) + +theorem npow_zero (a : D) : G.npow a 0 = G.one := rfl + +theorem npow_succ (a : D) (n : Nat) : + G.npow a (n + 1) = G.mul (G.npow a n) a := rfl + +theorem zpow_nat (a : D) (n : Nat) : + G.zpow a (Int.ofNat n) = G.npow a n := rfl + +theorem zpow_negative (a : D) (n : Nat) : + G.zpow a (-((n + 1 : Nat) : Int)) = G.inv (G.npow a (n + 1)) := rfl + +theorem zpow_zero (a : D) : G.zpow a 0 = G.one := rfl + +theorem zpow_one (a : D) : G.zpow a 1 = a := G.asAdd.zsmul_one a + +theorem one_zpow (k : Int) : G.zpow G.one k = G.one := + G.asAdd.zsmul_zero_right k + +theorem zpow_add (a : D) (k l : Int) : + G.zpow a (k + l) = G.mul (G.zpow a k) (G.zpow a l) := + G.asAdd.zsmul_add k l a + +theorem prod_zero (f : Fin 0 → D) : G.prod 0 f = G.one := rfl + +theorem prod_succ (n : Nat) (f : Fin (n + 1) → D) : + G.prod (n + 1) f = G.mul (f 0) (G.prod n (fun i => f i.succ)) := rfl + +theorem prod_mul (n : Nat) (f g : Fin n → D) : + G.prod n (fun i => G.mul (f i) (g i)) = + G.mul (G.prod n f) (G.prod n g) := + Finite.sum_add G.asAdd n f g + +end CommGroup + +/-- Literal finite product of ordinary signed integral powers. -/ +def monomial {D : Type u} (G : CommGroup D) {n : Nat} + (x : Fin n → D) (v : Row n) : D := + G.prod n (fun i => G.zpow (x i) (v i)) + +/-- The monomial is proved to be a character, not supplied as one. -/ +def monomialHom {D : Type u} (G : CommGroup D) {n : Nat} + (x : Fin n → D) : Hom (rowGroup n) G.asAdd where + run := monomial G x + map_zero := by + change fsum G.asAdd n (fun i => G.asAdd.zsmul 0 (x i)) = G.one + simp only [AbGroup.zsmul_zero] + exact Finite.sum_zero G.asAdd n + map_add := by + intro v w + change fsum G.asAdd n (fun i => G.asAdd.zsmul (v i + w i) (x i)) = + G.asAdd.add (fsum G.asAdd n (fun i => G.asAdd.zsmul (v i) (x i))) + (fsum G.asAdd n (fun i => G.asAdd.zsmul (w i) (x i))) + simp only [AbGroup.zsmul_add] + exact Finite.sum_add G.asAdd n _ _ + +namespace Character + +variable {D : Type u} {m n : Nat} + +/-- A finite row image is evaluated as the indicated integer powers of row values. -/ +theorem row_image (G : AbGroup D) (chi : Hom (rowGroup n) G) + (v : Row m) (A : Mat m n) : + chi.run (rowMul v A) = + fsum G m (fun r => G.zsmul (v r) (chi.run (A r))) := by + rw [Rows.rowMul_linear_combination, Finite.map_sum] + apply Finite.sum_congr + intro r + exact chi.map_zsmul (v r) (A r) + +/-- The bridge from INDIVIDUAL rows to their entire INTEGER span. -/ +theorem rows_annihilate_span (G : AbGroup D) (chi : Hom (rowGroup n) G) + (A : Mat m n) (h : ∀ r, chi.run (A r) = G.zero) (v : Row m) : + chi.run (rowMul v A) = G.zero := by + rw [row_image G chi v A] + calc + _ = fsum G m (fun _ => G.zero) := by + apply Finite.sum_congr + intro r + rw [h r, G.zsmul_zero_right] + _ = G.zero := Finite.sum_zero G m + +end Character + +namespace Monomial + +variable {D : Type u} (G : CommGroup D) + +theorem zero {n : Nat} (x : Fin n → D) : + monomial G x (rowGroup n).zero = G.one := (monomialHom G x).map_zero + +theorem add {n : Nat} (x : Fin n → D) (v w : Row n) : + monomial G x ((rowGroup n).add v w) = + G.mul (monomial G x v) (monomial G x w) := + (monomialHom G x).map_add v w + +theorem sub {n : Nat} (x : Fin n → D) (v w : Row n) : + monomial G x ((rowGroup n).sub v w) = + G.div (monomial G x v) (monomial G x w) := + (monomialHom G x).map_sub v w + +theorem scale {n : Nat} (x : Fin n → D) (k : Int) (v : Row n) : + monomial G x (PR1497.scale k v) = G.zpow (monomial G x v) k := by + rw [← Rows.row_zsmul] + exact (monomialHom G x).map_zsmul k v + +theorem on_basis {n : Nat} (x : Fin n → D) (i : Fin n) : + monomial G x (basis n i) = x i := by + change fsum G.asAdd n + (fun j => G.asAdd.zsmul (if j = i then 1 else 0) (x j)) = x i + calc + _ = fsum G.asAdd n (fun j => if j = i then x i else G.asAdd.zero) := by + apply Finite.sum_congr + intro j + by_cases h : j = i + · subst j + simp only [eq_self, ite_true, AbGroup.zsmul_one] + · simp only [if_neg h, AbGroup.zsmul_zero] + _ = x i := Finite.sum_single G.asAdd n i (x i) + +/-- Actual monomial substitution, including negative exponents. -/ +theorem substitution {m n : Nat} (x : Fin n → D) + (v : Row m) (A : Mat m n) : + monomial G x (rowMul v A) = + monomial G (fun r => monomial G x (A r)) v := + Character.row_image G.asAdd (monomialHom G x) v A + +theorem individual_rows_to_span {m n : Nat} (x : Fin n → D) + (A : Mat m n) (h : ∀ r, monomial G x (A r) = G.one) (v : Row m) : + monomial G x (rowMul v A) = G.one := + Character.rows_annihilate_span G.asAdd (monomialHom G x) A h v + +end Monomial + +/-! ## 6. Matrix-to-monomial reconstruction and converse, without root extraction -/ + +namespace MonomialBridge + +variable {D : Type u} (G : CommGroup D) + +def parameters {d N : Nat} (Q : Mat d N) (x : Fin N → D) : Fin d → D := + fun j => monomial G x (Q j) + +def realization {N d : Nat} (P : Mat N d) (theta : Fin d → D) : Fin N → D := + fun i => monomial G theta (P i) + +def Relations {m N : Nat} (M : Mat m N) (x : Fin N → D) : Prop := + ∀ r, monomial G x (M r) = G.one + +variable {m N d : Nat} +variable {M : Mat m N} {P : Mat N d} {Q : Mat d N} {W : Mat N m} + +/-- Stronger than coordinate reconstruction: every exponent vector factors through P. -/ +theorem reconstruction_all_exponents (h : MatrixIdentities M P Q W) + (x : Fin N → D) + (hx : Relations G M x) (v : Row N) : + monomial G x v = monomial G (parameters G Q x) (rowMul v P) := by + have hann : ∀ c, (monomialHom G x).run ((matrixRetraction h).m.run c) = + G.asAdd.zero := by + intro c + exact Monomial.individual_rows_to_span G x M hx c + calc + monomial G x v = monomial G x (rowMul (rowMul v P) Q) := + (matrixRetraction h).character_factor (monomialHom G x) hann v + _ = monomial G (parameters G Q x) (rowMul v P) := + Monomial.substitution G x (rowMul v P) Q + +theorem reconstruct_coordinate (h : MatrixIdentities M P Q W) + (x : Fin N → D) + (hx : Relations G M x) (i : Fin N) : + x i = monomial G (parameters G Q x) (P i) := by + have hi := reconstruction_all_exponents G h x hx (basis N i) + rw [Monomial.on_basis, Rows.rowMul_basis] at hi + exact hi + +theorem reconstruction (h : MatrixIdentities M P Q W) + (x : Fin N → D) (hx : Relations G M x) : + x = realization G P (parameters G Q x) := by + funext i + exact reconstruct_coordinate G h x hx i + +/-- Every arbitrary parameter tuple gives a solution of the individual relations. -/ +theorem converse_relations (h : MatrixIdentities M P Q W) + (theta : Fin d → D) : + Relations G M (realization G P theta) := by + intro r + have hr : rowMul (M r) P = (rowGroup d).zero := + congrArg (fun A : Mat m d => A r) h.mp + calc + monomial G (realization G P theta) (M r) = + monomial G theta (rowMul (M r) P) := + (Monomial.substitution G theta (M r) P).symm + _ = G.one := by rw [hr]; exact Monomial.zero G theta + +/-- QP = I recovers arbitrary parameters exactly, not merely up to powers. -/ +theorem parameters_recover (h : MatrixIdentities M P Q W) + (theta : Fin d → D) : + parameters G Q (realization G P theta) = theta := by + funext j + have hj : rowMul (Q j) P = basis d j := + congrArg (fun A : Mat d d => A j) h.qp + change monomial G (realization G P theta) (Q j) = theta j + calc + _ = monomial G theta (rowMul (Q j) P) := + (Monomial.substitution G theta (Q j) P).symm + _ = theta j := by rw [hj]; exact Monomial.on_basis G theta j + +/-- Any tuple realizing x is the tuple defined by the Q monomials. -/ +theorem parameters_unique (h : MatrixIdentities M P Q W) + (x : Fin N → D) (theta : Fin d → D) + (hreal : ∀ i, x i = monomial G theta (P i)) : + parameters G Q x = theta := by + have hx : x = realization G P theta := funext hreal + rw [hx] + exact parameters_recover G h theta + +/-- First equality in the requested residual calculation. -/ +theorem residual_exponent_formula (x : Fin N → D) (i : Fin N) : + G.div (x i) (monomial G (parameters G Q x) (P i)) = + monomial G x ((rowGroup N).sub (basis N i) ((matMul P Q) i)) := by + change G.div (x i) + (monomial G (fun j => monomial G x (Q j)) (P i)) = + monomial G x ((rowGroup N).sub (basis N i) (rowMul (P i) Q)) + rw [Monomial.sub, Monomial.on_basis, Monomial.substitution] + +/-- Second equality, with a literal finite product and the literal W coefficients. + This equation does not need the row relations to equal one. -/ +theorem residual_relations_formula (h : MatrixIdentities M P Q W) + (x : Fin N → D) (i : Fin N) : + G.div (x i) (monomial G (parameters G Q x) (P i)) = + G.prod m (fun r => G.zpow (monomial G x (M r)) (W i r)) := by + have hi : (rowGroup N).sub (basis N i) ((matMul P Q) i) = + rowMul (W i) M := + congrArg (fun A : Mat N N => A i) h.residual + rw [residual_exponent_formula G, hi] + exact Monomial.substitution G x (W i) M + +theorem residual_eq_one (h : MatrixIdentities M P Q W) + (x : Fin N → D) (hx : Relations G M x) (i : Fin N) : + G.div (x i) (monomial G (parameters G Q x) (P i)) = G.one := by + rw [reconstruct_coordinate G h x hx i] + exact G.mul_inv _ + +/-- Existence and uniqueness are both stated without a choice operator. -/ +theorem unique_parameterization (h : MatrixIdentities M P Q W) + (x : Fin N → D) (hx : Relations G M x) : + (∀ i, x i = monomial G (parameters G Q x) (P i)) ∧ + (∀ theta : Fin d → D, + (∀ i, x i = monomial G theta (P i)) → parameters G Q x = theta) := by + constructor + · exact reconstruct_coordinate G h x hx + · intro theta ht + exact parameters_unique G h x theta ht + +end MonomialBridge + +end PR1497 + +/-! ## Complete axiom-query inventory (output requires actual Lean replay). -/ +set_option pp.fullNames true +#print axioms PR1497.AbGroup +#print axioms PR1497.AbGroup.sub +#print axioms PR1497.AbGroup.add_left_cancel +#print axioms PR1497.AbGroup.add_right_cancel +#print axioms PR1497.AbGroup.add_left_comm +#print axioms PR1497.AbGroup.add_four +#print axioms PR1497.AbGroup.neg_zero +#print axioms PR1497.AbGroup.neg_neg +#print axioms PR1497.AbGroup.neg_add_distrib +#print axioms PR1497.AbGroup.sub_zero +#print axioms PR1497.AbGroup.sub_self +#print axioms PR1497.AbGroup.sub_add_cancel +#print axioms PR1497.AbGroup.add_sub_cancel +#print axioms PR1497.AbGroup.sub_eq_zero_iff +#print axioms PR1497.AbGroup.eq_of_sub_eq +#print axioms PR1497.AbGroup.nsmul +#print axioms PR1497.AbGroup.zsmul +#print axioms PR1497.AbGroup.nsmul_zero +#print axioms PR1497.AbGroup.zsmul_zero +#print axioms PR1497.AbGroup.zsmul_zero_right +#print axioms PR1497.AbGroup.zsmul_one +#print axioms PR1497.AbGroup.int_induction +#print axioms PR1497.AbGroup.zsmul_succ +#print axioms PR1497.AbGroup.zsmul_pred +#print axioms PR1497.AbGroup.zsmul_add +#print axioms PR1497.Hom +#print axioms PR1497.Hom.id +#print axioms PR1497.Hom.comp +#print axioms PR1497.Hom.ext +#print axioms PR1497.Hom.map_neg +#print axioms PR1497.Hom.map_sub +#print axioms PR1497.Hom.map_nsmul +#print axioms PR1497.Hom.map_zsmul +#print axioms PR1497.fsum +#print axioms PR1497.Finite.sum_congr +#print axioms PR1497.Finite.sum_zero +#print axioms PR1497.Finite.sum_add +#print axioms PR1497.Finite.sum_neg +#print axioms PR1497.Finite.sum_sub +#print axioms PR1497.Finite.sum_swap +#print axioms PR1497.Finite.sum_single +#print axioms PR1497.Finite.map_sum +#print axioms PR1497.intGroup +#print axioms PR1497.functionGroup +#print axioms PR1497.Row +#print axioms PR1497.Mat +#print axioms PR1497.rowGroup +#print axioms PR1497.scale +#print axioms PR1497.basis +#print axioms PR1497.eye +#print axioms PR1497.zeroMat +#print axioms PR1497.matSub +#print axioms PR1497.rowMul +#print axioms PR1497.matMul +#print axioms PR1497.Rows.sum_apply +#print axioms PR1497.Rows.nsmul_apply +#print axioms PR1497.Rows.zsmul_apply +#print axioms PR1497.Rows.int_nsmul +#print axioms PR1497.Rows.int_zsmul +#print axioms PR1497.Rows.row_zsmul +#print axioms PR1497.Rows.sum_mul_right +#print axioms PR1497.Rows.sum_mul_left +#print axioms PR1497.Rows.rowMul_zero_left +#print axioms PR1497.Rows.rowMul_zero_right +#print axioms PR1497.Rows.rowMul_add +#print axioms PR1497.Rows.rowMul_matSub +#print axioms PR1497.Rows.rowMul_assoc +#print axioms PR1497.Rows.rowMul_basis +#print axioms PR1497.Rows.rowMul_eye +#print axioms PR1497.Rows.rowMul_linear_combination +#print axioms PR1497.Rows.rowHom +#print axioms PR1497.Retraction +#print axioms PR1497.AddIso +#print axioms PR1497.TorsionFree +#print axioms PR1497.Retraction.L +#print axioms PR1497.Retraction.mem_image_iff +#print axioms PR1497.Retraction.image_eq_kernel +#print axioms PR1497.Retraction.surjective +#print axioms PR1497.Retraction.decomposition +#print axioms PR1497.Retraction.Rel +#print axioms PR1497.Retraction.rel_iff +#print axioms PR1497.Retraction.latticeSetoid +#print axioms PR1497.Retraction.LQuot +#print axioms PR1497.Retraction.qmk +#print axioms PR1497.Retraction.qmap +#print axioms PR1497.Retraction.qinv +#print axioms PR1497.Retraction.qmap_mk +#print axioms PR1497.Retraction.qmap_qinv +#print axioms PR1497.Retraction.qinv_qmap +#print axioms PR1497.Retraction.qmap_injective +#print axioms PR1497.Retraction.qadd +#print axioms PR1497.Retraction.qneg +#print axioms PR1497.Retraction.qmap_zero +#print axioms PR1497.Retraction.qmap_add +#print axioms PR1497.Retraction.qmap_neg +#print axioms PR1497.Retraction.quotientGroup +#print axioms PR1497.Retraction.quotientMap +#print axioms PR1497.Retraction.quotientInv +#print axioms PR1497.Retraction.quotientIso +#print axioms PR1497.Retraction.saturated +#print axioms PR1497.Retraction.character_factor +#print axioms PR1497.Retraction.character_unique +#print axioms PR1497.MatrixIdentities +#print axioms PR1497.matrixRetraction +#print axioms PR1497.MatrixBridge.Lattice +#print axioms PR1497.MatrixBridge.lattice_iff_integer_span +#print axioms PR1497.MatrixBridge.lattice_eq_kernel +#print axioms PR1497.MatrixBridge.lattice_eq_kernel_as_predicate +#print axioms PR1497.MatrixBridge.quotient_relation +#print axioms PR1497.MatrixBridge.quotient_equal_iff +#print axioms PR1497.MatrixBridge.phi_surjective +#print axioms PR1497.MatrixBridge.quotientIso +#print axioms PR1497.MatrixBridge.quotient_forward_on_representative +#print axioms PR1497.MatrixBridge.quotient_inverse_on_parameter +#print axioms PR1497.MatrixBridge.quotient_left_inverse +#print axioms PR1497.MatrixBridge.quotient_right_inverse +#print axioms PR1497.MatrixBridge.row_torsion_free +#print axioms PR1497.MatrixBridge.lattice_saturated +#print axioms PR1497.CommGroup +#print axioms PR1497.CommGroup.asAdd +#print axioms PR1497.CommGroup.npow +#print axioms PR1497.CommGroup.zpow +#print axioms PR1497.CommGroup.prod +#print axioms PR1497.CommGroup.div +#print axioms PR1497.CommGroup.npow_zero +#print axioms PR1497.CommGroup.npow_succ +#print axioms PR1497.CommGroup.zpow_nat +#print axioms PR1497.CommGroup.zpow_negative +#print axioms PR1497.CommGroup.zpow_zero +#print axioms PR1497.CommGroup.zpow_one +#print axioms PR1497.CommGroup.one_zpow +#print axioms PR1497.CommGroup.zpow_add +#print axioms PR1497.CommGroup.prod_zero +#print axioms PR1497.CommGroup.prod_succ +#print axioms PR1497.CommGroup.prod_mul +#print axioms PR1497.monomial +#print axioms PR1497.monomialHom +#print axioms PR1497.Character.row_image +#print axioms PR1497.Character.rows_annihilate_span +#print axioms PR1497.Monomial.zero +#print axioms PR1497.Monomial.add +#print axioms PR1497.Monomial.sub +#print axioms PR1497.Monomial.scale +#print axioms PR1497.Monomial.on_basis +#print axioms PR1497.Monomial.substitution +#print axioms PR1497.Monomial.individual_rows_to_span +#print axioms PR1497.MonomialBridge.parameters +#print axioms PR1497.MonomialBridge.realization +#print axioms PR1497.MonomialBridge.Relations +#print axioms PR1497.MonomialBridge.reconstruction_all_exponents +#print axioms PR1497.MonomialBridge.reconstruct_coordinate +#print axioms PR1497.MonomialBridge.reconstruction +#print axioms PR1497.MonomialBridge.converse_relations +#print axioms PR1497.MonomialBridge.parameters_recover +#print axioms PR1497.MonomialBridge.parameters_unique +#print axioms PR1497.MonomialBridge.residual_exponent_formula +#print axioms PR1497.MonomialBridge.residual_relations_formula +#print axioms PR1497.MonomialBridge.residual_eq_one +#print axioms PR1497.MonomialBridge.unique_parameterization diff --git a/research/integral-retraction-monomial-bridge/README.md b/research/integral-retraction-monomial-bridge/README.md new file mode 100644 index 0000000000..bb2e7e397f --- /dev/null +++ b/research/integral-retraction-monomial-bridge/README.md @@ -0,0 +1,130 @@ +# Integral retraction and monomial reconstruction + +Lean 4.30.0 checks the conditional bridge from three concrete integer matrix +identities to an image/kernel equality, an actual additive quotient isomorphism, +and unique multiplicative reconstruction. The package uses core/Std only. +It addresses the formalization question in [PR 1497](https://github.com/CrocSwap/integer-mult-bounds/pull/1497), +`audit.md` sections 8.2-8.3, under [Discussion 1527](https://github.com/CrocSwap/integer-mult-bounds/discussions/1527). +It does not instantiate the finite E8 matrices or prove their geometric use. + +## Exact conditional result + +`PR1497Bridge.lean` defines `Row n := Fin n -> Int`, finite sums, ordinary integer +matrix products, and the three-field proposition `MatrixIdentities M P Q W`: + +```text +M : Mat m N, P : Mat N d, Q : Mat d N, W : Mat N m +MP = 0, QP = I_d, I_N - PQ = WM. +``` + +For arbitrary natural dimensions, `MatrixBridge` proves that the integer row +image of `M` equals the kernel of `v -> vP`, identifies that image with literal +finite integer row combinations, and constructs the quotient by the relation +`v ~ w iff exists z, zM = v-w`. The quotient isomorphism has forward map +`[v] -> vP` and inverse `z -> [zQ]`. Integer lattice saturation is proved with +concrete integer torsion-freeness; it is not assumed as a certificate field. + +For a lawful commutative group, signed powers, finite products, monomials and +their algebra laws are constructed in the source. From the individual relations +`x^(M_r) = 1`, `MonomialBridge` proves that the Q-defined parameter tuple +`theta_j = x^(Q_j)` reconstructs every coordinate as `x_i = theta^(P_i)`. +It proves reconstruction for every exponent row, the converse for arbitrary +parameter tuples, recovery and uniqueness of those parameters, and the explicit +residual product using `W`. + +The custom group structures contain only operations and ordinary group laws. +The matrix certificate has exactly the three identities above. Image/kernel, +generation, quotient, saturation, monomial substitution and reconstruction are +proved conclusions. `SCOPE.md` gives the exact public interfaces and boundaries. + +## Reproduction and observed evidence + +Use an **already installed** Lean 4.30.0 at full commit +`d024af099ca4bf2c86f649261ebf59565dc8c622` and Python 3.12: + +```sh +LEAN=/path/to/installed/lean python3.12 -I -B research/integral-retraction-monomial-bridge/replay.py > /tmp/integral-retraction-replay.json +``` + +`LEAN` may be omitted if the installed compiler is on `PATH`. Use its direct +binary rather than a package-manager shim. The wrapper checks release, full +commit and source hashes, then uses fresh temporary copies. Inherited `LEAN_*` +settings are discarded; only the scratch import directory is supplied. It +installs nothing, invokes no package manager and leaves compiler outputs in +temporary storage. The JSON receipt goes to standard output. + +The replay sequence is universal compilation, its 159-query axiom census, +positive-fixture compilation, the combined 197-query census, three intended +negative compilations, and the unchanged Python tooling tests. A failed stage +stops the replay. The original `check_axioms.py` rejects missing, unexpected or +duplicate query reports and dependencies outside +`{propext, Quot.sound, Classical.choice}`. The wrapper also requires successful +compilation and fresh `.olean` outputs before accepting those reports. + +`REPLAY.json` records the actual local run on `arm64-apple-darwin24.6.0`, with +Python 3.12.14. Universal and positive sources compiled without errors or +warnings. All 197 queried declarations reported; the observed dependency union +was only `{propext, Quot.sound}`. No `sorryAx` or custom axiom dependency was +observed. Each negative fixture failed at exactly its intended false `decide` +proposition, rather than an import or syntax error. All ten Python tooling and +synthetic arithmetic tests passed. + +The positive fixtures include a signed nonzero-W certificate, negative powers, +an ordinary integer-addition group interface, a Bool XOR torsion group, direct +calls of the universal quotient/reconstruction interfaces, and missing-identity +countermodels. The three negative files separately reject a wrong W sign, +omission of `MP=0`, and omission of `QP=I`. Synthetic fixtures are separate from +an E8 instance or a field/unit adapter. + +The producer delivered source without running Lean and supplied diagnostic +repairs. Later local replay supplies the execution evidence. Packaging changed +only the introductory comments in the main and positive Lean files to report +that evidence and normalize the observed model attribution. Every byte after +those comments is unchanged. The axiom parser, tooling tests, and negative +fixtures are byte-identical to the repaired delivery. `SOURCES.json` records +both original and packaged hashes; `REPLAY.json` also records the body hashes. + +The generic package hook runs only the Python tooling tests, not Lean: + +```sh +python3.12 scripts/research_package.py --package research/integral-retraction-monomial-bridge +``` + +A generic CI pass therefore does not establish kernel acceptance. Use the +separate exact-version replay above for that evidence. + +## Open next questions + +Connect one pinned E8 instance to the concrete `MatrixIdentities` interface and +provide a lawful field nonzero-element group adapter. This would connect the +conditional bridge to actual finite data. The first step is to choose exact +M/P/Q/W source bytes from PR 1497 and check their Lean instance separately from +the adapter. `TASK.json` records the question and blockers. + +The geometric generator-to-relation and coverage obligations remain separate. +This package supplies no E8/P112/P120 matrix instance, rank API, field `Units` +adapter, Laurent scheme, local Lemma 5, decoder K, all-size compiler, or full +multiplication theorem. It changes no selected frontier or supplier profile. + +## Attribution and provenance + +Andrey Mas, with substantial **GPT-6 Pro** mathematical formalization and +diagnostic repair through ChatGPT, as identified in the browser UI. Codex +prepared source briefs, coordinated, audited execution, replayed and mechanically +packaged the artifact. No mathematical proof repair was made locally. A +producer self-reported variant label was not independently verified. + +The source statement is PR 1497 at +`7a1309f18f56d04c2db33bf1607e0332d19f72b3`, +`research/complex-rank8-ratio-gluing-audit/audit.md`, sections 8.2-8.3; its exact +bytes were checked locally. Inherited context credits **Brett Halligan / +burntout76 and Ninefold**, [PR 1212](https://github.com/CrocSwap/integer-mult-bounds/pull/1212); +**DreamingOfClouds**, [PR 717](https://github.com/CrocSwap/integer-mult-bounds/pull/717); +and **themilkman216**, [PR 968](https://github.com/CrocSwap/integer-mult-bounds/pull/968). +No predecessor Lean implementation was copied. Apache-2.0; see `LICENSE`. + +Historical task-card and selected-record provenance remains at revision 2, +`ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c`. The publication checkpoint is +main `81e81af67714bdc8d1693b0bf5c29468b92f62ff`, priority revision 3; the independent +verification follow-up remains relevant. `TASK.json` records the changed scope +without remapping the original card into the newer catalogue. diff --git a/research/integral-retraction-monomial-bridge/REPLAY.json b/research/integral-retraction-monomial-bridge/REPLAY.json new file mode 100644 index 0000000000..7e17d45a63 --- /dev/null +++ b/research/integral-retraction-monomial-bridge/REPLAY.json @@ -0,0 +1,1139 @@ +{ + "status": "Original repaired delivery and packaged sources both passed local kernel replay.", + "recorded_at": "2026-10-14T03:46:20.558611+00:00", + "python": "3.12.14", + "platform": "arm64-apple-darwin24.6.0", + "original_repaired_run": { + "exit_code": 0, + "wall_seconds": 5.301490583980922, + "main_sha256": "f71588d33ddc0373a85102edf16f19f677e14d4d60e96f3cd9f42ef20bd58279", + "fixture_sha256": "0ac121201611e4e1c9ac318397c9f67f73af31bb1812dc18c4294a995e1d226d", + "source_files_unchanged": true + }, + "packaging_body_identity": { + "archive_sha256": "1b2a00320f00d596f0348c770988a3a49e4ce6e7b653d041eff0389c88a1f330", + "lean_files_sha256": { + "PR1497Bridge.lean": "f71588d33ddc0373a85102edf16f19f677e14d4d60e96f3cd9f42ef20bd58279", + "fixtures/Positive.lean": "0ac121201611e4e1c9ac318397c9f67f73af31bb1812dc18c4294a995e1d226d" + }, + "body_after_leading_comment_sha256": { + "PR1497Bridge.lean": "1dfcae946288bb1620a20350c2f265cb04b5811c13f1c9a7c35192c4af9d3812", + "fixtures/Positive.lean": "dcde15c7f553921e9a1d8a1ea6e527f0c245cc9e80e7be3632541e0a1c8553b9" + }, + "packaging_change": "Only leading status/attribution comments changed in the two Lean files. All bytes after those comments match repair 2. The negative fixtures, axiom parser and tooling tests are unchanged." + }, + "portable_packaged_replay": { + "status": "PASS", + "lean_version": "4.30.0", + "lean_commit": "d024af099ca4bf2c86f649261ebf59565dc8c622", + "source_sha256": { + "PR1497Bridge.lean": "a27494b0d40bbf7874fd9a875e468c67d11545b266e17bc98f2ca75c77f6ee40", + "check_axioms.py": "23e86145231da2080a362aa69a01faa4bba9c2408d642155c83d57a29ab43a54", + "fixtures/Positive.lean": "4a5a40f2b845bcbfea48584bf662134ba29202cd4cd43390faee43cb7caa7c8b", + "fixtures/RejectMissingMP.lean": "7fd1d1e6d75ffa7eaef1c8c48ab70b7e24298fbd682360853720e203b6e199d2", + "fixtures/RejectMissingQP.lean": "5162b4ed6b194cce1f77db58213e66f9818d8b4af539f5cdf28eca4f41230dc8", + "fixtures/RejectWrongW.lean": "6952b0a871abbd1158e799e613fecbbd42b3bfde157e0f6ffe09b7a94caeb834", + "test_tooling.py": "2b79fde129bb0cf2e113f36326d29a9f218b053d12535c330ad689943aff7a64" + }, + "commands": [ + { + "argv": [ + "lean", + "-o", + "PR1497Bridge.olean", + "PR1497Bridge.lean" + ], + "exit_code": 0, + "seconds": 3.96689, + "stdout": "'PR1497.AbGroup' does not depend on any axioms\n'PR1497.AbGroup.sub' does not depend on any axioms\n'PR1497.AbGroup.add_left_cancel' does not depend on any axioms\n'PR1497.AbGroup.add_right_cancel' does not depend on any axioms\n'PR1497.AbGroup.add_left_comm' does not depend on any axioms\n'PR1497.AbGroup.add_four' does not depend on any axioms\n'PR1497.AbGroup.neg_zero' does not depend on any axioms\n'PR1497.AbGroup.neg_neg' does not depend on any axioms\n'PR1497.AbGroup.neg_add_distrib' does not depend on any axioms\n'PR1497.AbGroup.sub_zero' does not depend on any axioms\n'PR1497.AbGroup.sub_self' does not depend on any axioms\n'PR1497.AbGroup.sub_add_cancel' does not depend on any axioms\n'PR1497.AbGroup.add_sub_cancel' does not depend on any axioms\n'PR1497.AbGroup.sub_eq_zero_iff' does not depend on any axioms\n'PR1497.AbGroup.eq_of_sub_eq' does not depend on any axioms\n'PR1497.AbGroup.nsmul' does not depend on any axioms\n'PR1497.AbGroup.zsmul' does not depend on any axioms\n'PR1497.AbGroup.nsmul_zero' depends on axioms: [propext]\n'PR1497.AbGroup.zsmul_zero' does not depend on any axioms\n'PR1497.AbGroup.zsmul_zero_right' depends on axioms: [propext]\n'PR1497.AbGroup.zsmul_one' does not depend on any axioms\n'PR1497.AbGroup.int_induction' does not depend on any axioms\n'PR1497.AbGroup.zsmul_succ' depends on axioms: [propext, Quot.sound]\n'PR1497.AbGroup.zsmul_pred' depends on axioms: [propext, Quot.sound]\n'PR1497.AbGroup.zsmul_add' depends on axioms: [propext, Quot.sound]\n'PR1497.Hom' does not depend on any axioms\n'PR1497.Hom.id' does not depend on any axioms\n'PR1497.Hom.comp' does not depend on any axioms\n'PR1497.Hom.ext' depends on axioms: [Quot.sound]\n'PR1497.Hom.map_neg' does not depend on any axioms\n'PR1497.Hom.map_sub' does not depend on any axioms\n'PR1497.Hom.map_nsmul' depends on axioms: [propext]\n'PR1497.Hom.map_zsmul' depends on axioms: [propext]\n'PR1497.fsum' depends on axioms: [propext]\n'PR1497.Finite.sum_congr' depends on axioms: [propext, Quot.sound]\n'PR1497.Finite.sum_zero' depends on axioms: [propext]\n'PR1497.Finite.sum_add' depends on axioms: [propext]\n'PR1497.Finite.sum_neg' depends on axioms: [propext]\n'PR1497.Finite.sum_sub' depends on axioms: [propext]\n'PR1497.Finite.sum_swap' depends on axioms: [propext]\n'PR1497.Finite.sum_single' depends on axioms: [propext, Quot.sound]\n'PR1497.Finite.map_sum' depends on axioms: [propext]\n'PR1497.intGroup' depends on axioms: [propext]\n'PR1497.functionGroup' depends on axioms: [Quot.sound]\n'PR1497.Row' does not depend on any axioms\n'PR1497.Mat' does not depend on any axioms\n'PR1497.rowGroup' depends on axioms: [propext, Quot.sound]\n'PR1497.scale' does not depend on any axioms\n'PR1497.basis' does not depend on any axioms\n'PR1497.eye' does not depend on any axioms\n'PR1497.zeroMat' does not depend on any axioms\n'PR1497.matSub' does not depend on any axioms\n'PR1497.rowMul' depends on axioms: [propext]\n'PR1497.matMul' depends on axioms: [propext]\n'PR1497.Rows.sum_apply' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.nsmul_apply' depends on axioms: [Quot.sound]\n'PR1497.Rows.zsmul_apply' depends on axioms: [Quot.sound]\n'PR1497.Rows.int_nsmul' depends on axioms: [propext]\n'PR1497.Rows.int_zsmul' depends on axioms: [propext]\n'PR1497.Rows.row_zsmul' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.sum_mul_right' depends on axioms: [propext]\n'PR1497.Rows.sum_mul_left' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_zero_left' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_zero_right' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_add' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_matSub' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_assoc' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_basis' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_eye' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowMul_linear_combination' depends on axioms: [propext, Quot.sound]\n'PR1497.Rows.rowHom' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction' does not depend on any axioms\n'PR1497.AddIso' does not depend on any axioms\n'PR1497.TorsionFree' does not depend on any axioms\n'PR1497.Retraction.L' does not depend on any axioms\n'PR1497.Retraction.mem_image_iff' does not depend on any axioms\n'PR1497.Retraction.image_eq_kernel' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.surjective' does not depend on any axioms\n'PR1497.Retraction.decomposition' does not depend on any axioms\n'PR1497.Retraction.Rel' does not depend on any axioms\n'PR1497.Retraction.rel_iff' depends on axioms: [propext]\n'PR1497.Retraction.latticeSetoid' depends on axioms: [propext]\n'PR1497.Retraction.LQuot' depends on axioms: [propext]\n'PR1497.Retraction.qmk' depends on axioms: [propext]\n'PR1497.Retraction.qmap' depends on axioms: [propext]\n'PR1497.Retraction.qinv' depends on axioms: [propext]\n'PR1497.Retraction.qmap_mk' depends on axioms: [propext]\n'PR1497.Retraction.qmap_qinv' depends on axioms: [propext]\n'PR1497.Retraction.qinv_qmap' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.qmap_injective' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.qadd' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.qneg' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.qmap_zero' depends on axioms: [propext]\n'PR1497.Retraction.qmap_add' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.qmap_neg' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.quotientGroup' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.quotientMap' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.quotientInv' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.quotientIso' depends on axioms: [propext, Quot.sound]\n'PR1497.Retraction.saturated' depends on axioms: [propext]\n'PR1497.Retraction.character_factor' does not depend on any axioms\n'PR1497.Retraction.character_unique' does not depend on any axioms\n'PR1497.MatrixIdentities' depends on axioms: [propext]\n'PR1497.matrixRetraction' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.Lattice' depends on axioms: [propext]\n'PR1497.MatrixBridge.lattice_iff_integer_span' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.lattice_eq_kernel' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.lattice_eq_kernel_as_predicate' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.quotient_relation' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.quotient_equal_iff' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.phi_surjective' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.quotientIso' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.quotient_forward_on_representative' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.quotient_inverse_on_parameter' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.quotient_left_inverse' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.quotient_right_inverse' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.row_torsion_free' depends on axioms: [propext, Quot.sound]\n'PR1497.MatrixBridge.lattice_saturated' depends on axioms: [propext, Quot.sound]\n'PR1497.CommGroup' does not depend on any axioms\n'PR1497.CommGroup.asAdd' does not depend on any axioms\n'PR1497.CommGroup.npow' does not depend on any axioms\n'PR1497.CommGroup.zpow' does not depend on any axioms\n'PR1497.CommGroup.prod' depends on axioms: [propext]\n'PR1497.CommGroup.div' does not depend on any axioms\n'PR1497.CommGroup.npow_zero' does not depend on any axioms\n'PR1497.CommGroup.npow_succ' does not depend on any axioms\n'PR1497.CommGroup.zpow_nat' does not depend on any axioms\n'PR1497.CommGroup.zpow_negative' does not depend on any axioms\n'PR1497.CommGroup.zpow_zero' does not depend on any axioms\n'PR1497.CommGroup.zpow_one' does not depend on any axioms\n'PR1497.CommGroup.one_zpow' depends on axioms: [propext]\n'PR1497.CommGroup.zpow_add' depends on axioms: [propext, Quot.sound]\n'PR1497.CommGroup.prod_zero' depends on axioms: [propext]\n'PR1497.CommGroup.prod_succ' depends on axioms: [propext]\n'PR1497.CommGroup.prod_mul' depends on axioms: [propext]\n'PR1497.monomial' depends on axioms: [propext]\n'PR1497.monomialHom' depends on axioms: [propext, Quot.sound]\n'PR1497.Character.row_image' depends on axioms: [propext, Quot.sound]\n'PR1497.Character.rows_annihilate_span' depends on axioms: [propext, Quot.sound]\n'PR1497.Monomial.zero' depends on axioms: [propext, Quot.sound]\n'PR1497.Monomial.add' depends on axioms: [propext, Quot.sound]\n'PR1497.Monomial.sub' depends on axioms: [propext, Quot.sound]\n'PR1497.Monomial.scale' depends on axioms: [propext, Quot.sound]\n'PR1497.Monomial.on_basis' depends on axioms: [propext, Quot.sound]\n'PR1497.Monomial.substitution' depends on axioms: [propext, Quot.sound]\n'PR1497.Monomial.individual_rows_to_span' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.parameters' depends on axioms: [propext]\n'PR1497.MonomialBridge.realization' depends on axioms: [propext]\n'PR1497.MonomialBridge.Relations' depends on axioms: [propext]\n'PR1497.MonomialBridge.reconstruction_all_exponents' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.reconstruct_coordinate' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.reconstruction' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.converse_relations' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.parameters_recover' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.parameters_unique' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.residual_exponent_formula' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.residual_relations_formula' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.residual_eq_one' depends on axioms: [propext, Quot.sound]\n'PR1497.MonomialBridge.unique_parameterization' depends on axioms: [propext, Quot.sound]\n", + "stderr": "" + }, + { + "argv": [ + "lean", + "-o", + "fixtures/Positive.olean", + "fixtures/Positive.lean" + ], + "exit_code": 0, + "seconds": 0.424228, + "stdout": "'PR1497.Fixtures.M' does not depend on any axioms\n'PR1497.Fixtures.P' does not depend on any axioms\n'PR1497.Fixtures.Q' does not depend on any axioms\n'PR1497.Fixtures.W' does not depend on any axioms\n'PR1497.Fixtures.fixtureIdentities' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.nonzero_W' depends on axioms: [propext]\n'PR1497.Fixtures.nontrivial_residual' depends on axioms: [propext]\n'PR1497.Fixtures.wrongW' does not depend on any axioms\n'PR1497.Fixtures.wrongW_rejected' depends on axioms: [propext]\n'PR1497.Fixtures.scalarOne' does not depend on any axioms\n'PR1497.Fixtures.scalarZero' does not depend on any axioms\n'PR1497.Fixtures.missingMP_other_two' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.missingMP_rejected' depends on axioms: [propext]\n'PR1497.Fixtures.missingQP_other_two' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.missingQP_rejected' depends on axioms: [propext]\n'PR1497.Fixtures.fin_one' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.signedAddGroup' depends on axioms: [propext]\n'PR1497.Fixtures.signedPoint' does not depend on any axioms\n'PR1497.Fixtures.negative_power_numeric' depends on axioms: [propext]\n'PR1497.Fixtures.signed_relation' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.signed_parameter' depends on axioms: [propext]\n'PR1497.Fixtures.signed_reconstruction' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.wrongQ' does not depend on any axioms\n'PR1497.Fixtures.wrong_parameter_sign' depends on axioms: [propext]\n'PR1497.Fixtures.xorGroup' does not depend on any axioms\n'PR1497.Fixtures.torsionPoint' does not depend on any axioms\n'PR1497.Fixtures.torsion_relation' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.torsion_reconstruction' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.repeated_addition_step' depends on axioms: [propext]\n'PR1497.Fixtures.synthetic_kernel' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.synthetic_surjectivity' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.synthetic_quotient_roundtrip' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.synthetic_parameter_roundtrip' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.synthetic_saturation' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.signed_all_exponents' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.signed_converse' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.signed_recovery' depends on axioms: [propext, Quot.sound]\n'PR1497.Fixtures.signed_residual_product' depends on axioms: [propext, Quot.sound]\n", + "stderr": "" + }, + { + "argv": [ + "lean", + "fixtures/RejectWrongW.lean" + ], + "exit_code": 1, + "seconds": 0.325046, + "stdout": "fixtures/RejectWrongW.lean:5:2: error: Tactic `decide` proved that the proposition\n matSub (eye 2) (matMul P Q) 0 0 = matMul wrongW M 0 0\nis false\n", + "stderr": "" + }, + { + "argv": [ + "lean", + "fixtures/RejectMissingMP.lean" + ], + "exit_code": 1, + "seconds": 0.324731, + "stdout": "fixtures/RejectMissingMP.lean:5:2: error: Tactic `decide` proved that the proposition\n matMul scalarOne scalarOne 0 0 = zeroMat 1 1 0 0\nis false\n", + "stderr": "" + }, + { + "argv": [ + "lean", + "fixtures/RejectMissingQP.lean" + ], + "exit_code": 1, + "seconds": 0.318335, + "stdout": "fixtures/RejectMissingQP.lean:5:2: error: Tactic `decide` proved that the proposition\n matMul scalarZero scalarZero 0 0 = eye 1 0 0\nis false\n", + "stderr": "" + }, + { + "argv": [ + "python3", + "-B", + "test_tooling.py" + ], + "exit_code": 0, + "seconds": 0.076412, + "stdout": "", + "stderr": "test_missing_identity_countermodels (__main__.FixtureArithmeticTests.test_missing_identity_countermodels) ... ok\ntest_signed_and_torsion_points (__main__.FixtureArithmeticTests.test_signed_and_torsion_points) ... ok\ntest_signed_nonzero_w_identities (__main__.FixtureArithmeticTests.test_signed_nonzero_w_identities) ... ok\ntest_complete_query_inventory (__main__.ParserTests.test_complete_query_inventory) ... ok\ntest_disallowed_dependencies (__main__.ParserTests.test_disallowed_dependencies) ... ok\ntest_duplicate_record (__main__.ParserTests.test_duplicate_record) ... ok\ntest_error_bearing_census (__main__.ParserTests.test_error_bearing_census) ... ok\ntest_incomplete_proof_warning (__main__.ParserTests.test_incomplete_proof_warning) ... ok\ntest_missing_unexpected_duplicate_queries (__main__.ParserTests.test_missing_unexpected_duplicate_queries) ... ok\ntest_permitted_dependencies (__main__.ParserTests.test_permitted_dependencies) ... ok\n\n----------------------------------------------------------------------\nRan 10 tests in 0.003s\n\nOK\n" + } + ], + "universal_axioms": { + "allowed_axioms": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "declaration_count": 159, + "observed_dependencies": { + "PR1497.AbGroup": [], + "PR1497.AbGroup.add_four": [], + "PR1497.AbGroup.add_left_cancel": [], + "PR1497.AbGroup.add_left_comm": [], + "PR1497.AbGroup.add_right_cancel": [], + "PR1497.AbGroup.add_sub_cancel": [], + "PR1497.AbGroup.eq_of_sub_eq": [], + "PR1497.AbGroup.int_induction": [], + "PR1497.AbGroup.neg_add_distrib": [], + "PR1497.AbGroup.neg_neg": [], + "PR1497.AbGroup.neg_zero": [], + "PR1497.AbGroup.nsmul": [], + "PR1497.AbGroup.nsmul_zero": [ + "propext" + ], + "PR1497.AbGroup.sub": [], + "PR1497.AbGroup.sub_add_cancel": [], + "PR1497.AbGroup.sub_eq_zero_iff": [], + "PR1497.AbGroup.sub_self": [], + "PR1497.AbGroup.sub_zero": [], + "PR1497.AbGroup.zsmul": [], + "PR1497.AbGroup.zsmul_add": [ + "Quot.sound", + "propext" + ], + "PR1497.AbGroup.zsmul_one": [], + "PR1497.AbGroup.zsmul_pred": [ + "Quot.sound", + "propext" + ], + "PR1497.AbGroup.zsmul_succ": [ + "Quot.sound", + "propext" + ], + "PR1497.AbGroup.zsmul_zero": [], + "PR1497.AbGroup.zsmul_zero_right": [ + "propext" + ], + "PR1497.AddIso": [], + "PR1497.Character.row_image": [ + "Quot.sound", + "propext" + ], + "PR1497.Character.rows_annihilate_span": [ + "Quot.sound", + "propext" + ], + "PR1497.CommGroup": [], + "PR1497.CommGroup.asAdd": [], + "PR1497.CommGroup.div": [], + "PR1497.CommGroup.npow": [], + "PR1497.CommGroup.npow_succ": [], + "PR1497.CommGroup.npow_zero": [], + "PR1497.CommGroup.one_zpow": [ + "propext" + ], + "PR1497.CommGroup.prod": [ + "propext" + ], + "PR1497.CommGroup.prod_mul": [ + "propext" + ], + "PR1497.CommGroup.prod_succ": [ + "propext" + ], + "PR1497.CommGroup.prod_zero": [ + "propext" + ], + "PR1497.CommGroup.zpow": [], + "PR1497.CommGroup.zpow_add": [ + "Quot.sound", + "propext" + ], + "PR1497.CommGroup.zpow_nat": [], + "PR1497.CommGroup.zpow_negative": [], + "PR1497.CommGroup.zpow_one": [], + "PR1497.CommGroup.zpow_zero": [], + "PR1497.Finite.map_sum": [ + "propext" + ], + "PR1497.Finite.sum_add": [ + "propext" + ], + "PR1497.Finite.sum_congr": [ + "Quot.sound", + "propext" + ], + "PR1497.Finite.sum_neg": [ + "propext" + ], + "PR1497.Finite.sum_single": [ + "Quot.sound", + "propext" + ], + "PR1497.Finite.sum_sub": [ + "propext" + ], + "PR1497.Finite.sum_swap": [ + "propext" + ], + "PR1497.Finite.sum_zero": [ + "propext" + ], + "PR1497.Hom": [], + "PR1497.Hom.comp": [], + "PR1497.Hom.ext": [ + "Quot.sound" + ], + "PR1497.Hom.id": [], + "PR1497.Hom.map_neg": [], + "PR1497.Hom.map_nsmul": [ + "propext" + ], + "PR1497.Hom.map_sub": [], + "PR1497.Hom.map_zsmul": [ + "propext" + ], + "PR1497.Mat": [], + "PR1497.MatrixBridge.Lattice": [ + "propext" + ], + "PR1497.MatrixBridge.lattice_eq_kernel": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.lattice_eq_kernel_as_predicate": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.lattice_iff_integer_span": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.lattice_saturated": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.phi_surjective": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotientIso": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_equal_iff": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_forward_on_representative": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_inverse_on_parameter": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_left_inverse": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_relation": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_right_inverse": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.row_torsion_free": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixIdentities": [ + "propext" + ], + "PR1497.Monomial.add": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.individual_rows_to_span": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.on_basis": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.scale": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.sub": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.substitution": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.zero": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.Relations": [ + "propext" + ], + "PR1497.MonomialBridge.converse_relations": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.parameters": [ + "propext" + ], + "PR1497.MonomialBridge.parameters_recover": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.parameters_unique": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.realization": [ + "propext" + ], + "PR1497.MonomialBridge.reconstruct_coordinate": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.reconstruction": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.reconstruction_all_exponents": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.residual_eq_one": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.residual_exponent_formula": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.residual_relations_formula": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.unique_parameterization": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction": [], + "PR1497.Retraction.L": [], + "PR1497.Retraction.LQuot": [ + "propext" + ], + "PR1497.Retraction.Rel": [], + "PR1497.Retraction.character_factor": [], + "PR1497.Retraction.character_unique": [], + "PR1497.Retraction.decomposition": [], + "PR1497.Retraction.image_eq_kernel": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.latticeSetoid": [ + "propext" + ], + "PR1497.Retraction.mem_image_iff": [], + "PR1497.Retraction.qadd": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qinv": [ + "propext" + ], + "PR1497.Retraction.qinv_qmap": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap": [ + "propext" + ], + "PR1497.Retraction.qmap_add": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap_injective": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap_mk": [ + "propext" + ], + "PR1497.Retraction.qmap_neg": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap_qinv": [ + "propext" + ], + "PR1497.Retraction.qmap_zero": [ + "propext" + ], + "PR1497.Retraction.qmk": [ + "propext" + ], + "PR1497.Retraction.qneg": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientGroup": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientInv": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientIso": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientMap": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.rel_iff": [ + "propext" + ], + "PR1497.Retraction.saturated": [ + "propext" + ], + "PR1497.Retraction.surjective": [], + "PR1497.Row": [], + "PR1497.Rows.int_nsmul": [ + "propext" + ], + "PR1497.Rows.int_zsmul": [ + "propext" + ], + "PR1497.Rows.nsmul_apply": [ + "Quot.sound" + ], + "PR1497.Rows.rowHom": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_add": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_assoc": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_basis": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_eye": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_linear_combination": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_matSub": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_zero_left": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_zero_right": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.row_zsmul": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.sum_apply": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.sum_mul_left": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.sum_mul_right": [ + "propext" + ], + "PR1497.Rows.zsmul_apply": [ + "Quot.sound" + ], + "PR1497.TorsionFree": [], + "PR1497.basis": [], + "PR1497.eye": [], + "PR1497.fsum": [ + "propext" + ], + "PR1497.functionGroup": [ + "Quot.sound" + ], + "PR1497.intGroup": [ + "propext" + ], + "PR1497.matMul": [ + "propext" + ], + "PR1497.matSub": [], + "PR1497.matrixRetraction": [ + "Quot.sound", + "propext" + ], + "PR1497.monomial": [ + "propext" + ], + "PR1497.monomialHom": [ + "Quot.sound", + "propext" + ], + "PR1497.rowGroup": [ + "Quot.sound", + "propext" + ], + "PR1497.rowMul": [ + "propext" + ], + "PR1497.scale": [], + "PR1497.zeroMat": [] + } + }, + "positive_axioms": { + "allowed_axioms": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "declaration_count": 197, + "observed_dependencies": { + "PR1497.AbGroup": [], + "PR1497.AbGroup.add_four": [], + "PR1497.AbGroup.add_left_cancel": [], + "PR1497.AbGroup.add_left_comm": [], + "PR1497.AbGroup.add_right_cancel": [], + "PR1497.AbGroup.add_sub_cancel": [], + "PR1497.AbGroup.eq_of_sub_eq": [], + "PR1497.AbGroup.int_induction": [], + "PR1497.AbGroup.neg_add_distrib": [], + "PR1497.AbGroup.neg_neg": [], + "PR1497.AbGroup.neg_zero": [], + "PR1497.AbGroup.nsmul": [], + "PR1497.AbGroup.nsmul_zero": [ + "propext" + ], + "PR1497.AbGroup.sub": [], + "PR1497.AbGroup.sub_add_cancel": [], + "PR1497.AbGroup.sub_eq_zero_iff": [], + "PR1497.AbGroup.sub_self": [], + "PR1497.AbGroup.sub_zero": [], + "PR1497.AbGroup.zsmul": [], + "PR1497.AbGroup.zsmul_add": [ + "Quot.sound", + "propext" + ], + "PR1497.AbGroup.zsmul_one": [], + "PR1497.AbGroup.zsmul_pred": [ + "Quot.sound", + "propext" + ], + "PR1497.AbGroup.zsmul_succ": [ + "Quot.sound", + "propext" + ], + "PR1497.AbGroup.zsmul_zero": [], + "PR1497.AbGroup.zsmul_zero_right": [ + "propext" + ], + "PR1497.AddIso": [], + "PR1497.Character.row_image": [ + "Quot.sound", + "propext" + ], + "PR1497.Character.rows_annihilate_span": [ + "Quot.sound", + "propext" + ], + "PR1497.CommGroup": [], + "PR1497.CommGroup.asAdd": [], + "PR1497.CommGroup.div": [], + "PR1497.CommGroup.npow": [], + "PR1497.CommGroup.npow_succ": [], + "PR1497.CommGroup.npow_zero": [], + "PR1497.CommGroup.one_zpow": [ + "propext" + ], + "PR1497.CommGroup.prod": [ + "propext" + ], + "PR1497.CommGroup.prod_mul": [ + "propext" + ], + "PR1497.CommGroup.prod_succ": [ + "propext" + ], + "PR1497.CommGroup.prod_zero": [ + "propext" + ], + "PR1497.CommGroup.zpow": [], + "PR1497.CommGroup.zpow_add": [ + "Quot.sound", + "propext" + ], + "PR1497.CommGroup.zpow_nat": [], + "PR1497.CommGroup.zpow_negative": [], + "PR1497.CommGroup.zpow_one": [], + "PR1497.CommGroup.zpow_zero": [], + "PR1497.Finite.map_sum": [ + "propext" + ], + "PR1497.Finite.sum_add": [ + "propext" + ], + "PR1497.Finite.sum_congr": [ + "Quot.sound", + "propext" + ], + "PR1497.Finite.sum_neg": [ + "propext" + ], + "PR1497.Finite.sum_single": [ + "Quot.sound", + "propext" + ], + "PR1497.Finite.sum_sub": [ + "propext" + ], + "PR1497.Finite.sum_swap": [ + "propext" + ], + "PR1497.Finite.sum_zero": [ + "propext" + ], + "PR1497.Fixtures.M": [], + "PR1497.Fixtures.P": [], + "PR1497.Fixtures.Q": [], + "PR1497.Fixtures.W": [], + "PR1497.Fixtures.fin_one": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.fixtureIdentities": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.missingMP_other_two": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.missingMP_rejected": [ + "propext" + ], + "PR1497.Fixtures.missingQP_other_two": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.missingQP_rejected": [ + "propext" + ], + "PR1497.Fixtures.negative_power_numeric": [ + "propext" + ], + "PR1497.Fixtures.nontrivial_residual": [ + "propext" + ], + "PR1497.Fixtures.nonzero_W": [ + "propext" + ], + "PR1497.Fixtures.repeated_addition_step": [ + "propext" + ], + "PR1497.Fixtures.scalarOne": [], + "PR1497.Fixtures.scalarZero": [], + "PR1497.Fixtures.signedAddGroup": [ + "propext" + ], + "PR1497.Fixtures.signedPoint": [], + "PR1497.Fixtures.signed_all_exponents": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.signed_converse": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.signed_parameter": [ + "propext" + ], + "PR1497.Fixtures.signed_reconstruction": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.signed_recovery": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.signed_relation": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.signed_residual_product": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.synthetic_kernel": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.synthetic_parameter_roundtrip": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.synthetic_quotient_roundtrip": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.synthetic_saturation": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.synthetic_surjectivity": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.torsionPoint": [], + "PR1497.Fixtures.torsion_reconstruction": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.torsion_relation": [ + "Quot.sound", + "propext" + ], + "PR1497.Fixtures.wrongQ": [], + "PR1497.Fixtures.wrongW": [], + "PR1497.Fixtures.wrongW_rejected": [ + "propext" + ], + "PR1497.Fixtures.wrong_parameter_sign": [ + "propext" + ], + "PR1497.Fixtures.xorGroup": [], + "PR1497.Hom": [], + "PR1497.Hom.comp": [], + "PR1497.Hom.ext": [ + "Quot.sound" + ], + "PR1497.Hom.id": [], + "PR1497.Hom.map_neg": [], + "PR1497.Hom.map_nsmul": [ + "propext" + ], + "PR1497.Hom.map_sub": [], + "PR1497.Hom.map_zsmul": [ + "propext" + ], + "PR1497.Mat": [], + "PR1497.MatrixBridge.Lattice": [ + "propext" + ], + "PR1497.MatrixBridge.lattice_eq_kernel": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.lattice_eq_kernel_as_predicate": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.lattice_iff_integer_span": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.lattice_saturated": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.phi_surjective": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotientIso": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_equal_iff": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_forward_on_representative": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_inverse_on_parameter": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_left_inverse": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_relation": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.quotient_right_inverse": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixBridge.row_torsion_free": [ + "Quot.sound", + "propext" + ], + "PR1497.MatrixIdentities": [ + "propext" + ], + "PR1497.Monomial.add": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.individual_rows_to_span": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.on_basis": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.scale": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.sub": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.substitution": [ + "Quot.sound", + "propext" + ], + "PR1497.Monomial.zero": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.Relations": [ + "propext" + ], + "PR1497.MonomialBridge.converse_relations": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.parameters": [ + "propext" + ], + "PR1497.MonomialBridge.parameters_recover": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.parameters_unique": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.realization": [ + "propext" + ], + "PR1497.MonomialBridge.reconstruct_coordinate": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.reconstruction": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.reconstruction_all_exponents": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.residual_eq_one": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.residual_exponent_formula": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.residual_relations_formula": [ + "Quot.sound", + "propext" + ], + "PR1497.MonomialBridge.unique_parameterization": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction": [], + "PR1497.Retraction.L": [], + "PR1497.Retraction.LQuot": [ + "propext" + ], + "PR1497.Retraction.Rel": [], + "PR1497.Retraction.character_factor": [], + "PR1497.Retraction.character_unique": [], + "PR1497.Retraction.decomposition": [], + "PR1497.Retraction.image_eq_kernel": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.latticeSetoid": [ + "propext" + ], + "PR1497.Retraction.mem_image_iff": [], + "PR1497.Retraction.qadd": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qinv": [ + "propext" + ], + "PR1497.Retraction.qinv_qmap": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap": [ + "propext" + ], + "PR1497.Retraction.qmap_add": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap_injective": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap_mk": [ + "propext" + ], + "PR1497.Retraction.qmap_neg": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.qmap_qinv": [ + "propext" + ], + "PR1497.Retraction.qmap_zero": [ + "propext" + ], + "PR1497.Retraction.qmk": [ + "propext" + ], + "PR1497.Retraction.qneg": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientGroup": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientInv": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientIso": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.quotientMap": [ + "Quot.sound", + "propext" + ], + "PR1497.Retraction.rel_iff": [ + "propext" + ], + "PR1497.Retraction.saturated": [ + "propext" + ], + "PR1497.Retraction.surjective": [], + "PR1497.Row": [], + "PR1497.Rows.int_nsmul": [ + "propext" + ], + "PR1497.Rows.int_zsmul": [ + "propext" + ], + "PR1497.Rows.nsmul_apply": [ + "Quot.sound" + ], + "PR1497.Rows.rowHom": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_add": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_assoc": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_basis": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_eye": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_linear_combination": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_matSub": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_zero_left": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.rowMul_zero_right": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.row_zsmul": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.sum_apply": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.sum_mul_left": [ + "Quot.sound", + "propext" + ], + "PR1497.Rows.sum_mul_right": [ + "propext" + ], + "PR1497.Rows.zsmul_apply": [ + "Quot.sound" + ], + "PR1497.TorsionFree": [], + "PR1497.basis": [], + "PR1497.eye": [], + "PR1497.fsum": [ + "propext" + ], + "PR1497.functionGroup": [ + "Quot.sound" + ], + "PR1497.intGroup": [ + "propext" + ], + "PR1497.matMul": [ + "propext" + ], + "PR1497.matSub": [], + "PR1497.matrixRetraction": [ + "Quot.sound", + "propext" + ], + "PR1497.monomial": [ + "propext" + ], + "PR1497.monomialHom": [ + "Quot.sound", + "propext" + ], + "PR1497.rowGroup": [ + "Quot.sound", + "propext" + ], + "PR1497.rowMul": [ + "propext" + ], + "PR1497.scale": [], + "PR1497.zeroMat": [] + } + }, + "observed_axiom_union": [ + "Quot.sound", + "propext" + ] + }, + "evidence_boundary": "The producer did not execute Lean; these are subsequent local exact-toolchain observations. All 197 explicitly queried declarations are reported. No finite E8 matrix, rank API, field-unit adapter or geometry is checked.", + "generic_hook": { + "command": [ + "python3.12", + "-I", + "-B", + "scripts/research_package.py", + "--package", + "research/integral-retraction-monomial-bridge" + ], + "exit_code": 0, + "seconds": 0.247462, + "stdout": "CHECK NON-KERNEL ONLY: unchanged producer parser controls and finite synthetic matrix/group arithmetic. Generic CI does not provision Lean; run the separate exact-version replay.py for kernel evidence.\nPASS_REGISTERED_RESEARCH_PACKAGE research/integral-retraction-monomial-bridge outcome=completed\n", + "stderr": "test_missing_identity_countermodels (__main__.FixtureArithmeticTests.test_missing_identity_countermodels) ... ok\ntest_signed_and_torsion_points (__main__.FixtureArithmeticTests.test_signed_and_torsion_points) ... ok\ntest_signed_nonzero_w_identities (__main__.FixtureArithmeticTests.test_signed_nonzero_w_identities) ... ok\ntest_complete_query_inventory (__main__.ParserTests.test_complete_query_inventory) ... ok\ntest_disallowed_dependencies (__main__.ParserTests.test_disallowed_dependencies) ... ok\ntest_duplicate_record (__main__.ParserTests.test_duplicate_record) ... ok\ntest_error_bearing_census (__main__.ParserTests.test_error_bearing_census) ... ok\ntest_incomplete_proof_warning (__main__.ParserTests.test_incomplete_proof_warning) ... ok\ntest_missing_unexpected_duplicate_queries (__main__.ParserTests.test_missing_unexpected_duplicate_queries) ... ok\ntest_permitted_dependencies (__main__.ParserTests.test_permitted_dependencies) ... ok\n\n----------------------------------------------------------------------\nRan 10 tests in 0.003s\n\nOK\n", + "helper_base": "ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c", + "helper_sha256": "d7e12e93799b3e244d74de5cb979855efd5307a088854e52cdb32ce1d4f7646f", + "method": "Full pinned generic hook in temporary package export. Existing checkout Git object database used only for provenance lookup; GIT_WORK_TREE is scratch. No repository files or branches changed." + }, + "binding_controls": [ + { + "control": "source-byte mutation", + "exit_code": 1, + "stderr": "FAIL_INTEGRAL_RETRACTION_REPLAY: source hash mismatch: PR1497Bridge.lean\n" + }, + { + "control": "simulated wrong-commit tool; no Lean compilation attempted", + "exit_code": 1, + "stderr": "FAIL_INTEGRAL_RETRACTION_REPLAY: Lean commit mismatch\n" + } + ] +} diff --git a/research/integral-retraction-monomial-bridge/SCOPE.md b/research/integral-retraction-monomial-bridge/SCOPE.md new file mode 100644 index 0000000000..6b14ad599d --- /dev/null +++ b/research/integral-retraction-monomial-bridge/SCOPE.md @@ -0,0 +1,193 @@ +# Exact formal interfaces and boundaries + +Lean 4.30.0 locally accepted the universal source, positive fixtures and +197 queried axiom reports. The producer delivered source without executing +Lean; local execution is recorded separately in `REPLAY.json`. The interface +description below is retained from the producer, without mathematical changes. + +## 1. Concrete meanings and the only certificate structure + +All names below are within namespace `PR1497` unless stated otherwise. + +* `Row n` is literally `Fin n → Int`; `Mat m n` is `Fin m → Fin n → Int`. +* `fsum` is recursion through coordinates `0,1,...,n-1`, with the empty sum + equal to zero. `rowMul v A j` is `fsum intGroup m (fun i => v i * A i j)`. + `matMul A B i` is `rowMul (A i) B`. These are ordinary built-in integer + operations, not a primitive composition operation with an assumed law. +* `basis n i j` is 1 when `j=i` and 0 otherwise; `eye n i = basis n i`. + `matSub A B i j = A i j - B i j`. + +The proposition `MatrixIdentities M P Q W` has exactly three fields: + +```text +mp : matMul M P = zeroMat m d +qp : matMul Q P = eye d +residual : matSub (eye N) (matMul P Q) = matMul W M +``` + +There are no image/kernel, reconstruction, independence, rank, generation, or +nonzeroness fields. Dimensions are arbitrary natural numbers; the proof source +includes the empty-index cases of its finite-sum arguments. + +`Rows.rowMul_assoc`, `Rows.rowMul_eye`, `Rows.rowMul_basis`, +`Rows.rowMul_matSub`, and `Rows.rowMul_linear_combination` supply the concrete +interpretation. `matrixRetraction` then derives the abstract three identities. +In row-map order the abstract maps are + +```text +m(z)=zM, p(v)=vP, q(z)=zQ, w(v)=vW, +p(m(z))=0, p(q(z))=z, v-q(p(v))=m(w(v)). +``` + +Thus matrix composition/orientation is a proved interface, not an unfinished +assumption of the abstract bridge. + +## 2. Additive result and precise quotient + +`AbGroup` exposes zero, addition, negation, associativity, commutativity, +two identity laws, and two inverse laws. `Hom` exposes only a function, +zero preservation, and addition preservation. Negation, subtraction, natural +multiples, and integer multiples are handled by derived theorems. + +`Retraction.L a` is defined as `∃ c, m(c)=a`. The proof of +`Retraction.mem_image_iff` has the two usual directions: `mp` gives the forward +direction; the residual identity at a kernel element gives the explicit +coefficient vector `w(a)` for the reverse direction. Surjectivity uses `q(b)`. + +The quotient is **not defined to be the parameter group**. It is +`Quotient s.latticeSetoid`, whose actual relation is + +```text +s.Rel a b := ∃ c, s.m.run c = GA.sub a b. +``` + +`Retraction.rel_iff` proves that this relation is equivalent to `p(a)=p(b)`. +That equivalence supplies the setoid laws and well-definedness of the descended +map. `qadd` and `qneg` use `Quotient.liftOn₂` and `Quotient.liftOn` to implement +`[a]+[b]=[a+b]` and `-[a]=[-a]`. Their representative-independence proofs are +explicit. `quotientGroup` proves the resulting abelian-group laws. +`quotientIso` constructs inverse **additive homomorphisms**, not just a set +bijection. Its inverse is precisely `b ↦ [q(b)]`. + +Principal concrete interfaces: + +| Declaration | Conclusion | +|---|---| +| `MatrixBridge.lattice_iff_integer_span` | The row-map image is exactly the displayed finite integer row combinations. | +| `MatrixBridge.lattice_eq_kernel` | Pointwise membership iff `rowMul v P = 0`. | +| `MatrixBridge.lattice_eq_kernel_as_predicate` | Literal equality of the two predicates. | +| `MatrixBridge.phi_surjective` | Every integer parameter row has a preimage. | +| `MatrixBridge.quotient_relation` | The relation is exactly `∃ z, zM = (v-w)`. | +| `MatrixBridge.quotient_equal_iff` | Equality of representative classes iff their difference lies in the row image. | +| `MatrixBridge.quotientIso` | The constructed abelian-group isomorphism. | +| `MatrixBridge.quotient_forward_on_representative` | Forward map sends `[v]` to `vP`. | +| `MatrixBridge.quotient_inverse_on_parameter` | Inverse sends `z` to `[zQ]`. | +| `MatrixBridge.quotient_left_inverse` / `quotient_right_inverse` | Both inverse equations. | +| `MatrixBridge.lattice_saturated` | A nonzero integer multiple in the lattice implies membership of the original row. | + +`MatrixBridge.row_torsion_free` is proved using `Int.mul_eq_zero`; it is not an +assumption about integer rows. `Rows.row_zsmul` connects the recursive group +integer multiple to actual coordinatewise integer multiplication. The generic +saturation lemma has a torsion-free hypothesis; the concrete corollary supplies +it by this proof. No formal rank invariant or rank theorem is supplied. + +## 3. Multiplicative meaning is constructed, not postulated + +`CommGroup D` lists multiplication, identity, inverse, associativity, +commutativity, and the left/right identity and inverse laws. It has no exponent, +finite-product, monomial, composition, or reconstruction law fields. +`CommGroup.asAdd` merely renames these operations so that the elementary group +proofs can be reused. + +The ordinary meanings are exposed by the definition equations: + +```text +npow a 0 = 1 +npow a (n+1) = (npow a n) * a +zpow a (ofNat n)= npow a n +zpow a (-(n+1)) = inverse (npow a (n+1)) +prod 0 f = 1 +prod (n+1) f = f(0) * prod n (fun i => f(i.succ)) +monomial x v = prod n (fun i => zpow (x i) (v i)). +``` + +`AbGroup.zsmul_add` derives the exponent-addition law by two-sided integer +induction. `Finite.sum_add` derives product distribution in the multiplicative +interpretation from associativity and commutativity. `monomialHom` is then a +constructed homomorphism on actual integer rows. In particular, the file does +not assume an evaluation map that already preserves the desired compositions. +`Monomial.add`, `sub`, and `scale` expose the resulting algebra laws. + +The individual-row interface is central: + +```text +Monomial.individual_rows_to_span: + (∀ r, monomial G x (M r) = G.one) → + ∀ z, monomial G x (rowMul z M) = G.one. +``` + +Its proof goes through `Rows.rowMul_linear_combination`, `Hom.map_zsmul`, and +`Finite.map_sum`. Every integer coefficient, including every negative +coefficient, is handled there. The universal abstract factorization lemma has +an annihilation hypothesis, but the concrete theorem supplies that hypothesis +from the **individual** rows by this bridge. It is not an extra certificate +assumption. + +`Monomial.substitution` proves the exact finite-product substitution identity +for arbitrary integer matrices. Define + +```text +parameters G Q x j = monomial G x (Q j) +realization G P theta i = monomial G theta (P i). +``` + +The main interfaces in `MonomialBridge` are: + +| Declaration | Conclusion | +|---|---| +| `reconstruction_all_exponents` | `x^v = theta^(vP)` for every integer exponent row, under the individual relations. | +| `reconstruct_coordinate` / `reconstruction` | `x_i = theta^(P_i)`, respectively equality of tuples. | +| `converse_relations` | Every arbitrary parameter tuple produces a solution, using `MP=0`. | +| `parameters_recover` | Applying the Q monomials to a realization recovers the arbitrary tuple, using `QP=I`. | +| `parameters_unique` / `unique_parameterization` | Every tuple realizing a solution equals its Q-defined tuple. | +| `residual_exponent_formula` | The coordinate ratio equals `x^(e_i-(PQ)_i)`. | +| `residual_relations_formula` | That ratio equals the literal product `∏r (x^(M_r))^(W_ir)`. | +| `residual_eq_one` | Under the individual relations, the ratio equals one. | + +The first residual formula does not need the certificate identities; the +second uses the residual identity, and the last uses the relation hypotheses. +These formulas provide the requested chain without root extraction or a +characteristic/divisibility assumption. There is no supplied Lean field API, +`Units` adapter, or Laurent-scheme construction. Applying this interface to a +particular field's nonzero elements still requires that ordinary group adapter. + +## 4. Remaining application boundaries + +The universal source and synthetic fixtures passed the exact local kernel +replay. The observed dependency union is `propext` and `Quot.sound`; +`Classical.choice` remains permitted by the unchanged parser but was not observed. +The three intended false-`decide` controls also failed at their specified +propositions. See `REPLAY.json` for actual outputs and source hashes. + +Not included: geometric generation and coverage; actual P112/P120/E8 matrices +and W witnesses; matrix certificates from the audit; field/unit and scheme +adapters; the nonzero-field-element premise; a rank API; local Lemma 5; decoder K; +and all all-size, precision, tape, analytic, hosting, and integer-multiplication +consequences. A specific E8 application must supply and check its actual +`MatrixIdentities` term and any field adapter separately. This package cannot +supply the remaining geometric generator-to-relation bridge merely by proving +its conditional algebraic implication. + +## 5. Conditional certificate boundary + +The 20 matrix-conditional public declarations in `MatrixBridge` and +`MonomialBridge` each have an explicit `(h : MatrixIdentities M P Q W)` binder. +`Lattice`, `lattice_iff_integer_span`, `row_torsion_free`, and +`residual_exponent_formula` remain certificate-independent. The explicit +ordinary group laws and the three matrix identities are legitimate hypotheses, +not hidden conclusion fields. No custom axiom declaration is introduced. + +The source statement is PR1497 `audit.md` sections 8.2-8.3 at commit +`7a1309f18f56d04c2db33bf1607e0332d19f72b3`; its exact bytes were checked locally. +The producer worked from the supplied statement. See `SOURCES.json` for the Git +blob and SHA256, and `README.md` for predecessor and substantial AI attribution. diff --git a/research/integral-retraction-monomial-bridge/SOURCES.json b/research/integral-retraction-monomial-bridge/SOURCES.json new file mode 100644 index 0000000000..0557db079c --- /dev/null +++ b/research/integral-retraction-monomial-bridge/SOURCES.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "base_commit": "ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + } + ], + "current_main_at_publication_base": "adc34159e0d6dc3dd2af2bdba3f5ca7376ef957e", + "priority_checkpoint": { + "revision": 3, + "note": "Historical task-card provenance remains revision 2. The independent-verification follow-up is compatible with the current priority checkpoint; no frontier or supplier-profile claim." + }, + "delivered_files": { + "PR1497Bridge.lean": "a27494b0d40bbf7874fd9a875e468c67d11545b266e17bc98f2ca75c77f6ee40", + "check_axioms.py": "23e86145231da2080a362aa69a01faa4bba9c2408d642155c83d57a29ab43a54", + "fixtures/Positive.lean": "4a5a40f2b845bcbfea48584bf662134ba29202cd4cd43390faee43cb7caa7c8b", + "fixtures/RejectMissingMP.lean": "7fd1d1e6d75ffa7eaef1c8c48ab70b7e24298fbd682360853720e203b6e199d2", + "fixtures/RejectMissingQP.lean": "5162b4ed6b194cce1f77db58213e66f9818d8b4af539f5cdf28eca4f41230dc8", + "fixtures/RejectWrongW.lean": "6952b0a871abbd1158e799e613fecbbd42b3bfde157e0f6ffe09b7a94caeb834", + "test_tooling.py": "2b79fde129bb0cf2e113f36326d29a9f218b053d12535c330ad689943aff7a64" + }, + "original_delivery": { + "archive_sha256": "1b2a00320f00d596f0348c770988a3a49e4ce6e7b653d041eff0389c88a1f330", + "lean_files_sha256": { + "PR1497Bridge.lean": "f71588d33ddc0373a85102edf16f19f677e14d4d60e96f3cd9f42ef20bd58279", + "fixtures/Positive.lean": "0ac121201611e4e1c9ac318397c9f67f73af31bb1812dc18c4294a995e1d226d" + }, + "body_after_leading_comment_sha256": { + "PR1497Bridge.lean": "1dfcae946288bb1620a20350c2f265cb04b5811c13f1c9a7c35192c4af9d3812", + "fixtures/Positive.lean": "dcde15c7f553921e9a1d8a1ea6e527f0c245cc9e80e7be3632541e0a1c8553b9" + }, + "packaging_change": "Only leading status/attribution comments changed in the two Lean files. All bytes after those comments match repair 2. The negative fixtures, axiom parser and tooling tests are unchanged." + }, + "external_predecessors": [ + { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1497", + "commit": "7a1309f18f56d04c2db33bf1607e0332d19f72b3", + "path": "research/complex-rank8-ratio-gluing-audit/audit.md", + "git_blob": "8753847aea8d5afdc34fcda85ed6fa54cde7c1d8", + "sha256": "2e6bf15efc5293e85b4a0cc486fbd84989209ee22c6e04a8d741bb2f76405d4c", + "scope": "Sections 8.2-8.3: integral retraction identities and multiplicative reconstruction. Exact source bytes checked locally; no finite E8 matrix instantiation is formalized by this package.", + "attribution": "Andrey Mas with substantial GPT-6 Pro research assistance." + } + ], + "external_predecessor_note": "Source and attribution pins, not runtime inputs. Inherited context credits Brett Halligan/burntout76 and Ninefold (PR1212), DreamingOfClouds (PR717), themilkman216 (PR968). No predecessor Lean implementation copied." +} diff --git a/research/integral-retraction-monomial-bridge/TASK.json b/research/integral-retraction-monomial-bridge/TASK.json new file mode 100644 index 0000000000..163038c868 --- /dev/null +++ b/research/integral-retraction-monomial-bridge/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c", + "current_main_at_publication_base": "81e81af67714bdc8d1693b0bf5c29468b92f62ff", + "priority_checkpoint": { + "revision": 3, + "note": "Historical task-card provenance remains revision 2. The independent-verification follow-up is compatible with the current priority checkpoint; no frontier or supplier-profile claim." + }, + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "changed", + "actual_scope": "Formalize the conditional integer image/kernel quotient and monomial reconstruction bridge from three integral matrix identities in Lean 4.30.0 core/Std.", + "scope_change_reason": "The original complex masked-decoder card led to PR1497 structural audit questions. Discussion1527 claims the reusable formal bridge, not another decoder or a finite matrix certificate.", + "bottleneck_link": "Checks an inherited algebraic implication separately from the finite E8 inputs and geometry needed to apply it.", + "budget_minutes": 120, + "stop_rule": "Deliver the stated conditional bridge, explicit laws, exact compiler receipts and meaningful controls; defer finite E8 instantiation, rank and field/unit adapters.", + "outcome": "completed", + "evidence": "Exact Lean 4.30.0 local replay accepted the universal source, repaired positive fixtures and 197 queried axiom reports. Three deliberately false propositions failed at their intended decide checks. Packaging replay is recorded in REPLAY.json.", + "author": "Andrey Mas", + "ai_assistance": "Substantial GPT-6 Pro mathematical formalization and diagnostic repair through ChatGPT, as identified in its browser UI. Codex prepared sources, audited and replayed the result, and mechanically packaged it; no local mathematical repair.", + "open_questions": [ + { + "question": "Can one pinned E8 instance be connected to the concrete MatrixIdentities and a field nonzero-element group adapter?", + "why_it_matters": "The universal conditional bridge alone does not certify the audit's finite matrices or geometric application.", + "first_step": "Select one exact M/P/Q/W certificate from PR1497, create a Lean MatrixIdentities instance, and separately supply a lawful field-units adapter.", + "blocked_by": "No E8 matrix data, field API, Units adapter, or geometric generator-to-relation coverage theorem is included." + } + ], + "scope_key": "independent-verification/integral-retraction/concrete-Int-matrices/quotient-and-monomials", + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1527", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/1497", + "overlap": "Scoped claim and predecessor checks recorded at entry; final overlap refresh is required before publication.", + "prepublication_overlap": "Complete 2026-10-14T03:49:56/03:51:07Z snapshot: 733 open PRs, 244 Discussion body/comment/reply records, no warnings. Direct1527 has no replies; PR1497 remains7a1309f1 and audit source matches. PR1309 unitary prefix norms and PR1530 dispatcher prefix invariants are distinct. Focused full-body reads found no matching formal bridge claim; metadata coverage does not establish global novelty." + } +} diff --git a/research/integral-retraction-monomial-bridge/VERIFY.json b/research/integral-retraction-monomial-bridge/VERIFY.json new file mode 100644 index 0000000000..d0c2dd8f53 --- /dev/null +++ b/research/integral-retraction-monomial-bridge/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/test_tooling.py" + ], + "timeout_seconds": 30, + "checks": "NON-KERNEL ONLY: unchanged producer parser controls and finite synthetic matrix/group arithmetic. Generic CI does not provision Lean; run the separate exact-version replay.py for kernel evidence." + } + ] +} diff --git a/research/integral-retraction-monomial-bridge/check_axioms.py b/research/integral-retraction-monomial-bridge/check_axioms.py new file mode 100644 index 0000000000..bc2500c714 --- /dev/null +++ b/research/integral-retraction-monomial-bridge/check_axioms.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Audit actual Lean #print axioms output. This is NOT a proof checker. + +Usage: python3 check_axioms.py SOURCE LOG [SOURCE LOG ...] +Stdlib only. Accepts no missing/duplicate queries or non-whitelisted axioms. +Only successful fresh Lean compilations should be supplied by replay.sh. +The parser also rejects error diagnostics; parsing is not proof checking. +""" +from __future__ import annotations +import json +import re +import sys +from pathlib import Path + +ALLOWED = frozenset({"Quot.sound", "propext", "Classical.choice"}) +QUERY = re.compile(r"^#print axioms ([A-Za-z_][A-Za-z_0-9.]*)\s*$", re.M) +RECORD = re.compile( + r"'([^']+)'\s+(?:does not depend on any axioms|" + r"depends on axioms:\s*\[([^\]]*)\])", re.M +) + + +def parse_records(text: str) -> dict[str, list[str]]: + # Even a complete-looking census cannot certify an error-bearing compilation. + if re.search(r"(?mi)^.*\berror:", text): + raise ValueError("Compiler error diagnostic in axiom log") + if re.search(r"(?i)declaration uses [\"'`]sorry[\"'`]", text): + raise ValueError("Incomplete-proof diagnostic in axiom log") + records: dict[str, list[str]] = {} + for match in RECORD.finditer(text): + name = match.group(1) + if name in records: + raise ValueError(f"Duplicate axiom record: {name}") + deps = sorted({a.strip().strip('`') for a in (match.group(2) or '').split(',') + if a.strip()}) + extra = set(deps) - ALLOWED + if extra: + raise ValueError(f"Disallowed axiom dependencies for {name}: {sorted(extra)}") + records[name] = deps + return records + + +def main(argv: list[str]) -> int: + if not argv or len(argv) % 2: + print(__doc__, file=sys.stderr) + return 2 + report: dict[str, list[str]] = {} + for src_arg, log_arg in zip(argv[0::2], argv[1::2]): + source = Path(src_arg).read_text(encoding="utf-8") + expected = QUERY.findall(source) + if not expected or len(set(expected)) != len(expected): + raise ValueError(f"Empty/duplicate axiom-query inventory: {src_arg}") + actual = parse_records(Path(log_arg).read_text(encoding="utf-8")) + missing = set(expected) - actual.keys() + unexpected = actual.keys() - set(expected) + if missing or unexpected: + raise ValueError(f"Axiom inventory mismatch for {src_arg}; " + f"missing={sorted(missing)}, unexpected={sorted(unexpected)}") + if report.keys() & actual.keys(): + raise ValueError("Duplicate declarations across supplied logs") + report.update(actual) + print(json.dumps({"allowed_axioms": sorted(ALLOWED), + "declaration_count": len(report), + "observed_dependencies": dict(sorted(report.items()))}, indent=2)) + return 0 + + +if __name__ == "__main__": + try: + raise SystemExit(main(sys.argv[1:])) + except (OSError, ValueError) as exc: + print(f"AXIOM AUDIT FAILED: {exc}", file=sys.stderr) + raise SystemExit(1) diff --git a/research/integral-retraction-monomial-bridge/fixtures/Positive.lean b/research/integral-retraction-monomial-bridge/fixtures/Positive.lean new file mode 100644 index 0000000000..8546a6ad2d --- /dev/null +++ b/research/integral-retraction-monomial-bridge/fixtures/Positive.lean @@ -0,0 +1,252 @@ +/- +SPDX-License-Identifier: Apache-2.0 +Locally kernel checked after source-only delivery; see REPLAY.json. +Independent synthetic tests; none is a hypothesis of the universal theorems. +-/ +import PR1497Bridge + +set_option autoImplicit false + +namespace PR1497.Fixtures + +-- m = 1, N = 2, d = 1. Both rows of W are nonzero; Q has a negative entry. +-- M = [-2, 1], P = [1; 2], Q = [3, -1], W = [1; 3]. +def M : Mat 1 2 := fun _ j => if j.val = 0 then -2 else 1 +def P : Mat 2 1 := fun i _ => if i.val = 0 then 1 else 2 +def Q : Mat 1 2 := fun _ j => if j.val = 0 then 3 else -1 +def W : Mat 2 1 := fun i _ => if i.val = 0 then 1 else 3 + +theorem fixtureIdentities : MatrixIdentities M P Q W := by + constructor + · funext i j + revert i j + simp only [Fin.forall_fin_succ, Fin.forall_fin_zero] <;> decide + · funext i j + revert i j + simp only [Fin.forall_fin_succ, Fin.forall_fin_zero] <;> decide + · funext i j + revert i j + simp only [Fin.forall_fin_succ, Fin.forall_fin_zero] <;> decide + +theorem nonzero_W : W 0 0 = 1 ∧ W 1 0 = 3 := by decide + +theorem nontrivial_residual : + matSub (eye 2) (matMul P Q) 0 0 = -2 ∧ + matSub (eye 2) (matMul P Q) 0 1 = 1 ∧ + matSub (eye 2) (matMul P Q) 1 0 = -6 ∧ + matSub (eye 2) (matMul P Q) 1 1 = 3 := by decide + +-- Flip the witness sign while retaining MP = 0 and QP = I. +def wrongW : Mat 2 1 := fun i r => -(W i r) + +theorem wrongW_rejected : ¬ MatrixIdentities M P Q wrongW := by + intro h + have hc := congrArg (fun A : Mat 2 2 => A 0 0) h.residual + change (-2 : Int) = 2 at hc + exact (by decide : (-2 : Int) ≠ 2) hc + +-- Drop MP: the other two identities can hold while MP fails. +def scalarOne : Mat 1 1 := fun _ _ => 1 +def scalarZero : Mat 1 1 := fun _ _ => 0 + +theorem missingMP_other_two : + matMul scalarOne scalarOne = eye 1 ∧ + matSub (eye 1) (matMul scalarOne scalarOne) = + matMul scalarZero scalarOne := by + constructor + · funext i j + revert i j + simp only [Fin.forall_fin_succ, Fin.forall_fin_zero] <;> decide + · funext i j + revert i j + simp only [Fin.forall_fin_succ, Fin.forall_fin_zero] <;> decide + +theorem missingMP_rejected : + ¬ MatrixIdentities scalarOne scalarOne scalarOne scalarZero := by + intro h + have hc := congrArg (fun A : Mat 1 1 => A 0 0) h.mp + change (1 : Int) = 0 at hc + exact (by decide : (1 : Int) ≠ 0) hc + +-- Drop QP: MP and the residual identity do not imply surjectivity. +theorem missingQP_other_two : + matMul scalarOne scalarZero = zeroMat 1 1 ∧ + matSub (eye 1) (matMul scalarZero scalarZero) = + matMul scalarOne scalarOne := by + constructor + · funext i j + revert i j + simp only [Fin.forall_fin_succ, Fin.forall_fin_zero] <;> decide + · funext i j + revert i j + simp only [Fin.forall_fin_succ, Fin.forall_fin_zero] <;> decide + +theorem missingQP_rejected : + ¬ MatrixIdentities scalarOne scalarZero scalarZero scalarOne := by + intro h + have hc := congrArg (fun A : Mat 1 1 => A 0 0) h.qp + change (0 : Int) = 1 at hc + exact (by decide : (0 : Int) ≠ 1) hc + +theorem fin_one (i : Fin 1) : i = 0 := by + apply Fin.eq_of_val_eq + omega + +-- A lawful multiplicative-group interface whose operation is integer addition. +-- It is NOT a field, nor claimed to be a field/unit API instantiation. +def signedAddGroup : CommGroup Int where + one := 0 + mul := (· + ·) + inv := Neg.neg + mul_assoc := Int.add_assoc + one_mul := Int.zero_add + mul_one := Int.add_zero + mul_comm := Int.add_comm + inv_mul := Int.add_left_neg + mul_inv := Int.add_right_neg + +def signedPoint : Fin 2 → Int := fun i => if i.val = 0 then 5 else 10 + +theorem negative_power_numeric : signedAddGroup.zpow 5 (-3) = -15 := by decide + +theorem signed_relation : MonomialBridge.Relations signedAddGroup M signedPoint := by + intro r + have hr := fin_one r + subst r + decide + +theorem signed_parameter : + MonomialBridge.parameters signedAddGroup Q signedPoint 0 = 5 := by decide + +theorem signed_reconstruction : + signedPoint = MonomialBridge.realization signedAddGroup P + (MonomialBridge.parameters signedAddGroup Q signedPoint) := + MonomialBridge.reconstruction signedAddGroup fixtureIdentities signedPoint signed_relation + +def wrongQ : Mat 1 2 := fun _ j => if j.val = 0 then 3 else 1 + +theorem wrong_parameter_sign : + MonomialBridge.parameters signedAddGroup wrongQ signedPoint 0 ≠ 5 := by decide + +-- A torsion group: XOR on Bool. This checks a case with no root uniqueness. +def xorGroup : CommGroup Bool where + one := false + mul := Bool.xor + inv := fun a => a + mul_assoc := by intro a b c; cases a <;> cases b <;> cases c <;> rfl + one_mul := by intro a; cases a <;> rfl + mul_one := by intro a; cases a <;> rfl + mul_comm := by intro a b; cases a <;> cases b <;> rfl + inv_mul := by intro a; cases a <;> rfl + mul_inv := by intro a; cases a <;> rfl + +def torsionPoint : Fin 2 → Bool := fun i => i.val == 0 + +theorem torsion_relation : MonomialBridge.Relations xorGroup M torsionPoint := by + intro r + have hr := fin_one r + subst r + decide + +theorem torsion_reconstruction : + torsionPoint = MonomialBridge.realization xorGroup P + (MonomialBridge.parameters xorGroup Q torsionPoint) := + MonomialBridge.reconstruction xorGroup fixtureIdentities torsionPoint torsion_relation + + +/-! Repair regressions: these call the repaired public interfaces, rather than + substituting numerical checks for the universal proof obligations. -/ + +theorem repeated_addition_step (n : Nat) (a : Int) : + intGroup.nsmul (n + 1) a = intGroup.add (intGroup.nsmul n a) a := rfl + +theorem synthetic_kernel (v : Row 2) : + MatrixBridge.Lattice (M := M) v ↔ rowMul v P = (rowGroup 1).zero := + MatrixBridge.lattice_eq_kernel fixtureIdentities v + +theorem synthetic_surjectivity : + ∀ z : Row 1, ∃ v : Row 2, rowMul v P = z := + MatrixBridge.phi_surjective fixtureIdentities + +theorem synthetic_quotient_roundtrip + (x : (matrixRetraction fixtureIdentities).LQuot) : + (MatrixBridge.quotientIso fixtureIdentities).backward.run + ((MatrixBridge.quotientIso fixtureIdentities).forward.run x) = x := + MatrixBridge.quotient_left_inverse fixtureIdentities x + +theorem synthetic_parameter_roundtrip (z : Row 1) : + (MatrixBridge.quotientIso fixtureIdentities).forward.run + ((MatrixBridge.quotientIso fixtureIdentities).backward.run z) = z := + MatrixBridge.quotient_right_inverse fixtureIdentities z + +theorem synthetic_saturation (k : Int) (hk : k ≠ 0) (v : Row 2) + (hv : MatrixBridge.Lattice (M := M) (scale k v)) : + MatrixBridge.Lattice (M := M) v := + MatrixBridge.lattice_saturated fixtureIdentities k hk v hv + +theorem signed_all_exponents (v : Row 2) : + monomial signedAddGroup signedPoint v = + monomial signedAddGroup + (MonomialBridge.parameters signedAddGroup Q signedPoint) (rowMul v P) := + MonomialBridge.reconstruction_all_exponents + signedAddGroup fixtureIdentities signedPoint signed_relation v + +theorem signed_converse (theta : Fin 1 → Int) : + MonomialBridge.Relations signedAddGroup M + (MonomialBridge.realization signedAddGroup P theta) := + MonomialBridge.converse_relations signedAddGroup fixtureIdentities theta + +theorem signed_recovery (theta : Fin 1 → Int) : + MonomialBridge.parameters signedAddGroup Q + (MonomialBridge.realization signedAddGroup P theta) = theta := + MonomialBridge.parameters_recover signedAddGroup fixtureIdentities theta + +theorem signed_residual_product (x : Fin 2 → Int) (i : Fin 2) : + signedAddGroup.div (x i) + (monomial signedAddGroup (MonomialBridge.parameters signedAddGroup Q x) (P i)) = + signedAddGroup.prod 1 + (fun r => signedAddGroup.zpow (monomial signedAddGroup x (M r)) (W i r)) := + MonomialBridge.residual_relations_formula signedAddGroup fixtureIdentities x i + +end PR1497.Fixtures + +/-! ## Complete axiom-query inventory (output requires actual Lean replay). -/ +set_option pp.fullNames true +#print axioms PR1497.Fixtures.M +#print axioms PR1497.Fixtures.P +#print axioms PR1497.Fixtures.Q +#print axioms PR1497.Fixtures.W +#print axioms PR1497.Fixtures.fixtureIdentities +#print axioms PR1497.Fixtures.nonzero_W +#print axioms PR1497.Fixtures.nontrivial_residual +#print axioms PR1497.Fixtures.wrongW +#print axioms PR1497.Fixtures.wrongW_rejected +#print axioms PR1497.Fixtures.scalarOne +#print axioms PR1497.Fixtures.scalarZero +#print axioms PR1497.Fixtures.missingMP_other_two +#print axioms PR1497.Fixtures.missingMP_rejected +#print axioms PR1497.Fixtures.missingQP_other_two +#print axioms PR1497.Fixtures.missingQP_rejected +#print axioms PR1497.Fixtures.fin_one +#print axioms PR1497.Fixtures.signedAddGroup +#print axioms PR1497.Fixtures.signedPoint +#print axioms PR1497.Fixtures.negative_power_numeric +#print axioms PR1497.Fixtures.signed_relation +#print axioms PR1497.Fixtures.signed_parameter +#print axioms PR1497.Fixtures.signed_reconstruction +#print axioms PR1497.Fixtures.wrongQ +#print axioms PR1497.Fixtures.wrong_parameter_sign +#print axioms PR1497.Fixtures.xorGroup +#print axioms PR1497.Fixtures.torsionPoint +#print axioms PR1497.Fixtures.torsion_relation +#print axioms PR1497.Fixtures.torsion_reconstruction +#print axioms PR1497.Fixtures.repeated_addition_step +#print axioms PR1497.Fixtures.synthetic_kernel +#print axioms PR1497.Fixtures.synthetic_surjectivity +#print axioms PR1497.Fixtures.synthetic_quotient_roundtrip +#print axioms PR1497.Fixtures.synthetic_parameter_roundtrip +#print axioms PR1497.Fixtures.synthetic_saturation +#print axioms PR1497.Fixtures.signed_all_exponents +#print axioms PR1497.Fixtures.signed_converse +#print axioms PR1497.Fixtures.signed_recovery +#print axioms PR1497.Fixtures.signed_residual_product diff --git a/research/integral-retraction-monomial-bridge/fixtures/RejectMissingMP.lean b/research/integral-retraction-monomial-bridge/fixtures/RejectMissingMP.lean new file mode 100644 index 0000000000..704c094b5f --- /dev/null +++ b/research/integral-retraction-monomial-bridge/fixtures/RejectMissingMP.lean @@ -0,0 +1,5 @@ +-- EXPECTED COMPILATION FAILURE: QP and the residual identity hold, but MP does not. +import fixtures.Positive +open PR1497 PR1497.Fixtures +example : matMul scalarOne scalarOne 0 0 = zeroMat 1 1 0 0 := by + decide diff --git a/research/integral-retraction-monomial-bridge/fixtures/RejectMissingQP.lean b/research/integral-retraction-monomial-bridge/fixtures/RejectMissingQP.lean new file mode 100644 index 0000000000..0f5657509f --- /dev/null +++ b/research/integral-retraction-monomial-bridge/fixtures/RejectMissingQP.lean @@ -0,0 +1,5 @@ +-- EXPECTED COMPILATION FAILURE: MP and the residual identity hold, but QP does not. +import fixtures.Positive +open PR1497 PR1497.Fixtures +example : matMul scalarZero scalarZero 0 0 = eye 1 0 0 := by + decide diff --git a/research/integral-retraction-monomial-bridge/fixtures/RejectWrongW.lean b/research/integral-retraction-monomial-bridge/fixtures/RejectWrongW.lean new file mode 100644 index 0000000000..3256ca3caa --- /dev/null +++ b/research/integral-retraction-monomial-bridge/fixtures/RejectWrongW.lean @@ -0,0 +1,5 @@ +-- EXPECTED COMPILATION FAILURE: a false residual entry, not a false new axiom. +import fixtures.Positive +open PR1497 PR1497.Fixtures +example : matSub (eye 2) (matMul P Q) 0 0 = matMul wrongW M 0 0 := by + decide diff --git a/research/integral-retraction-monomial-bridge/replay.py b/research/integral-retraction-monomial-bridge/replay.py new file mode 100644 index 0000000000..72792edacd --- /dev/null +++ b/research/integral-retraction-monomial-bridge/replay.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Portable mechanical replay of the pinned bridge and its original axiom parser. + +Andrey Mas, with Codex packaging assistance. Apache-2.0. +Requires an installed Lean; performs no installation or network operation. +""" +import hashlib +import json +import os +from pathlib import Path +import re +import shutil +import subprocess +import sys +import tempfile +import time + +VERSION = "4.30.0" +COMMIT = "d024af099ca4bf2c86f649261ebf59565dc8c622" +SOURCES = ("PR1497Bridge.lean", "fixtures/Positive.lean", + "fixtures/RejectWrongW.lean", "fixtures/RejectMissingMP.lean", + "fixtures/RejectMissingQP.lean", "check_axioms.py", "test_tooling.py") + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def run(argv, cwd, env, succeeds=True): + start = time.monotonic() + result = subprocess.run(argv, cwd=cwd, env=env, text=True, capture_output=True, timeout=120) + record = {"argv": [Path(argv[0]).name, *argv[1:]], "exit_code": result.returncode, + "seconds": round(time.monotonic() - start, 6), + "stdout": result.stdout, "stderr": result.stderr} + if succeeds and result.returncode: + print(json.dumps(record, indent=2), file=sys.stderr) + raise ValueError("replay command failed") + return record + + +def main(): + require(sys.version_info[:2] == (3, 12), "use Python 3.12") + package = Path(__file__).resolve().parent + pins = json.loads((package / "SOURCES.json").read_text())["delivered_files"] + require(set(pins) == set(SOURCES), "source inventory mismatch") + for name in SOURCES: + require(hashlib.sha256((package / name).read_bytes()).hexdigest() == pins[name], + "source hash mismatch: " + name) + selected = os.environ.get("LEAN") or shutil.which("lean") + require(selected, "set LEAN to an installed Lean 4.30.0 binary, or place it on PATH") + lean = str(Path(selected).resolve(strict=True)) + # Only the fresh scratch directory is added for the package-local Lean imports. + env = {"PATH": str(Path(lean).parent) + os.pathsep + "/usr/bin:/bin", "LANG": "C.UTF-8"} + receipt = {"status": "PASS", "lean_version": VERSION, "lean_commit": COMMIT, + "source_sha256": pins, "commands": []} + with tempfile.TemporaryDirectory(prefix="integral-retraction-replay-") as tmp: + scratch = Path(tmp) + (scratch / "fixtures").mkdir() + for name in SOURCES: + shutil.copyfile(package / name, scratch / name) + version = run([lean, "--short-version"], scratch, env) + commit = run([lean, "--githash"], scratch, env) + require(version["stdout"].strip() == VERSION, "Lean release mismatch") + require(commit["stdout"].strip() == COMMIT, "Lean commit mismatch") + env["LEAN_PATH"] = str(scratch) + pairs = [] + for module, label, count in (("PR1497Bridge", "universal", 159), + ("fixtures/Positive", "positive", 197)): + record = run([lean, "-o", module + ".olean", module + ".lean"], scratch, env) + output = record["stdout"] + record["stderr"] + require(not re.search(r"\berror(?:\([^)]*\))?:|sorryAx|declaration uses ['\"]sorry", output), + "Lean error or proof-placeholder diagnostic") + require((scratch / (module + ".olean")).is_file(), "missing compiled artifact") + receipt["commands"].append(record) + (scratch / (label + ".log")).write_text(output) + pairs += [module + ".lean", label + ".log"] + audit = run([sys.executable, "-I", "-B", "check_axioms.py", *pairs], scratch, env) + census = json.loads(audit["stdout"]) + require(census["declaration_count"] == count, "axiom query count mismatch") + receipt[label + "_axioms"] = census + for label in ("RejectWrongW", "RejectMissingMP", "RejectMissingQP"): + record = run([lean, "fixtures/" + label + ".lean"], scratch, env, succeeds=False) + output = record["stdout"] + record["stderr"] + errors = re.findall(r"\berror(?:\([^)]*\))?:", output) + require(record["exit_code"] != 0 and len(errors) == 1 + and 'Tactic `decide` proved that the proposition' in output and 'is false' in output, + "negative fixture did not fail only at its intended false proposition: " + label) + receipt["commands"].append(record) + # The unchanged script imports its sibling parser. The minimal environment + # excludes inherited PYTHONPATH; ordinary script-directory import is needed. + receipt["commands"].append(run([sys.executable, "-B", "test_tooling.py"], scratch, env)) + receipt["observed_axiom_union"] = sorted({a for values in receipt["positive_axioms"] + ["observed_dependencies"].values() for a in values}) + print(json.dumps(receipt, indent=2)) + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError, subprocess.SubprocessError) as exc: + sys.exit("FAIL_INTEGRAL_RETRACTION_REPLAY: " + str(exc)) diff --git a/research/integral-retraction-monomial-bridge/test_tooling.py b/research/integral-retraction-monomial-bridge/test_tooling.py new file mode 100644 index 0000000000..90f876a3d8 --- /dev/null +++ b/research/integral-retraction-monomial-bridge/test_tooling.py @@ -0,0 +1,123 @@ +#!/usr/bin/env python3 +"""Stdlib-only tests of log-auditing code and small fixture arithmetic. + +No Lean invocation, mocked compiler, theorem checking, or axiom receipts. +Axiom-format strings below are deliberately synthetic parser unit-test inputs. +Run: PYTHONDONTWRITEBYTECODE=1 python3 test_tooling.py +""" +from __future__ import annotations + +import contextlib +import io +import tempfile +import unittest +from pathlib import Path + +import check_axioms + + +def matmul(a: list[list[int]], b: list[list[int]]) -> list[list[int]]: + return [[sum(a[i][k] * b[k][j] for k in range(len(b))) + for j in range(len(b[0]))] for i in range(len(a))] + + +def matsub(a: list[list[int]], b: list[list[int]]) -> list[list[int]]: + return [[x - y for x, y in zip(ar, br)] for ar, br in zip(a, b)] + + +class ParserTests(unittest.TestCase): + def test_permitted_dependencies(self) -> None: + # These are toy strings, NOT compiler output from PR1497Bridge.lean. + text = ("'Toy.zero' does not depend on any axioms\n" + "'Toy.quot' depends on axioms: [Quot.sound, propext, Classical.choice]\n") + self.assertEqual(check_axioms.parse_records(text), { + 'Toy.zero': [], + 'Toy.quot': ['Classical.choice', 'Quot.sound', 'propext'], + }) + + def test_duplicate_record(self) -> None: + line = "'Toy.zero' does not depend on any axioms\n" + with self.assertRaises(ValueError): + check_axioms.parse_records(line + line) + + def test_disallowed_dependencies(self) -> None: + for dependency in ['Foreign.assumption', 'sorryAx', 'Lean.ofReduceBool']: + with self.subTest(dependency=dependency), self.assertRaises(ValueError): + check_axioms.parse_records(f"'Toy.bad' depends on axioms: [{dependency}]\n") + + def test_error_bearing_census(self) -> None: + text = ("Toy.lean:1:1: error: unsolved goals\n" + "'Toy.zero' does not depend on any axioms\n") + with self.assertRaises(ValueError): + check_axioms.parse_records(text) + + def test_incomplete_proof_warning(self) -> None: + text = ("Toy.lean:1:1: warning: declaration uses 'sorry'\n" + "'Toy.zero' does not depend on any axioms\n") + with self.assertRaises(ValueError): + check_axioms.parse_records(text) + + def test_complete_query_inventory(self) -> None: + with tempfile.TemporaryDirectory(prefix='pr1497-parser-unit-') as temp: + root = Path(temp) + src, log = root / 'Toy.lean.txt', root / 'synthetic.txt' + src.write_text('#print axioms Toy.zero\n', encoding='utf-8') + log.write_text("'Toy.zero' does not depend on any axioms\n", encoding='utf-8') + with contextlib.redirect_stdout(io.StringIO()): + self.assertEqual(check_axioms.main([str(src), str(log)]), 0) + + def test_missing_unexpected_duplicate_queries(self) -> None: + cases = [ + ('#print axioms Toy.zero\n', ''), + ('#print axioms Toy.zero\n', "'Toy.other' does not depend on any axioms\n"), + ('#print axioms Toy.zero\n#print axioms Toy.zero\n', + "'Toy.zero' does not depend on any axioms\n"), + ] + with tempfile.TemporaryDirectory(prefix='pr1497-parser-unit-') as temp: + root = Path(temp) + src, log = root / 'Toy.lean.txt', root / 'synthetic.txt' + for source, output in cases: + src.write_text(source, encoding='utf-8') + log.write_text(output, encoding='utf-8') + with self.subTest(source=source, output=output), self.assertRaises(ValueError): + check_axioms.main([str(src), str(log)]) + + +class FixtureArithmeticTests(unittest.TestCase): + def test_signed_nonzero_w_identities(self) -> None: + m, p, q, w = [[-2, 1]], [[1], [2]], [[3, -1]], [[1], [3]] + self.assertEqual(matmul(m, p), [[0]]) + self.assertEqual(matmul(q, p), [[1]]) + residual = matsub([[1, 0], [0, 1]], matmul(p, q)) + self.assertEqual(residual, [[-2, 1], [-6, 3]]) + self.assertEqual(residual, matmul(w, m)) + self.assertNotEqual(residual, matmul([[-1], [-3]], m)) + + def test_missing_identity_countermodels(self) -> None: + one, zero = [[1]], [[0]] + # M=P=Q=1, W=0: QP and residual hold, MP fails. + self.assertEqual(matmul(one, one), one) + self.assertEqual(matsub(one, matmul(one, one)), matmul(zero, one)) + self.assertNotEqual(matmul(one, one), zero) + # M=W=1, P=Q=0: MP and residual hold, QP fails. + self.assertEqual(matmul(one, zero), zero) + self.assertEqual(matsub(one, matmul(zero, zero)), matmul(one, one)) + self.assertNotEqual(matmul(zero, zero), one) + + def test_signed_and_torsion_points(self) -> None: + m, p, q = [-2, 1], [1, 2], [3, -1] + x = [5, 10] + self.assertEqual(sum(a * b for a, b in zip(x, m)), 0) + theta = sum(a * b for a, b in zip(x, q)) + self.assertEqual(theta, 5) + self.assertEqual([theta * a for a in p], x) + self.assertEqual(5 * (-3), -15) + self.assertNotEqual(3 * 5 + 10, 5) + b = [1, 0] # Bool XOR group, represented by integers modulo 2. + self.assertEqual(sum(a * c for a, c in zip(b, m)) % 2, 0) + t = sum(a * c for a, c in zip(b, q)) % 2 + self.assertEqual([t * a % 2 for a in p], b) + + +if __name__ == '__main__': + unittest.main(verbosity=2)