From 6e75a5a8aab52bda6a01de2bc6061b7eb55fe46d Mon Sep 17 00:00:00 2001 From: ValentinBredemestre Date: Sat, 10 Jan 2026 16:15:07 +0200 Subject: [PATCH 1/2] Remove sorry: prove solsInclLinSols_injective This proves injectivity of solsInclLinSols. --- PhysLean/QFT/AnomalyCancellation/Basic.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/PhysLean/QFT/AnomalyCancellation/Basic.lean b/PhysLean/QFT/AnomalyCancellation/Basic.lean index 7cdec4cf..0d3ab6c3 100644 --- a/PhysLean/QFT/AnomalyCancellation/Basic.lean +++ b/PhysLean/QFT/AnomalyCancellation/Basic.lean @@ -500,10 +500,13 @@ lemma solsInclQuadSols_injective (χ : ACCSystem) : def solsInclLinSols (χ : ACCSystem) : χ.Sols →[ℚ] χ.LinSols := MulActionHom.comp χ.quadSolsInclLinSols χ.solsInclQuadSols -@[sorryful] lemma solsInclLinSols_injective (χ : ACCSystem) : Function.Injective χ.solsInclLinSols := by - sorry + intro S T h + have h' : χ.solsInclQuadSols S = χ.solsInclQuadSols T := by + apply ACCSystemQuad.quadSolsInclLinSols_injective (χ := χ.toACCSystemQuad) + simpa [ACCSystem.solsInclLinSols, MulActionHom.comp_apply] using h + exact solsInclQuadSols_injective χ h' /-! From a281a38501a2c15e074ef948033a171f12b1a71a Mon Sep 17 00:00:00 2001 From: ValentinBredemestre Date: Sat, 10 Jan 2026 17:01:53 +0200 Subject: [PATCH 2/2] Keep sorryful: solsInclLinSols_injective This lemma currently depends on results that are still marked sorryful in the codebase. The `@[sorryful]` attribute is kept so that `sorry_lint` passes. It can be removed once the upstream dependencies are fully resolved. --- PhysLean/QFT/AnomalyCancellation/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/PhysLean/QFT/AnomalyCancellation/Basic.lean b/PhysLean/QFT/AnomalyCancellation/Basic.lean index 0d3ab6c3..6461a302 100644 --- a/PhysLean/QFT/AnomalyCancellation/Basic.lean +++ b/PhysLean/QFT/AnomalyCancellation/Basic.lean @@ -500,6 +500,7 @@ lemma solsInclQuadSols_injective (χ : ACCSystem) : def solsInclLinSols (χ : ACCSystem) : χ.Sols →[ℚ] χ.LinSols := MulActionHom.comp χ.quadSolsInclLinSols χ.solsInclQuadSols +@[sorryful] lemma solsInclLinSols_injective (χ : ACCSystem) : Function.Injective χ.solsInclLinSols := by intro S T h