Deduplicate redundant proofs: closed-range cokernel argument and diagonal-operator self-adjointness - #15
Merged
Conversation
… (M3a/M3b) Add the "Compact perturbations of the identity" subsection (Riesz-Schauder Fredholm theorem and its supporting lemmas) and the new "Fourier-coefficient recursion" section covering periodIntegral_eq_of_periodic, the holSection/ holCoeff machinery, and the exact dimension count dim H^0(L_k) = k, dim H^1(L_k) = 0. Update the theta-sections status note and chapter intro accordingly. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Examples/Shift.lean proved finrank_quotient_range_eq_orthogonal by hand for H over ℂ, while CompactOperators.lean's isFredholm_one_sub independently derived the same underlying fact (quotient by a closed-range submodule is linearly equivalent to its orthogonal complement) inline, for general RCLike 𝕜. Extract the shared fact as Submodule.quotientEquivOrthogonal (plus the finrank and FiniteDimensional-transfer corollaries) in CompactOperators.lean, generalized to RCLike 𝕜, and have both call sites reuse it. Also backfills scripts/axiom_report.lean, which never picked up CompactOperators.lean's tracked declarations (IsCompactOperator.adjoint, isFredholm_one_sub, etc.) after the chiral-fredholm merge. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Circle.lean and Torus.lean each proved, by hand, that their respective diagonal Dirac operator (scalar eigenvalues vs. 2x2 Hermitian spinor blocks) is self-adjoint on its maximal H^1 domain, via an essentially identical argument: symmetry from the blocks being Hermitian, domain density via testing against single-mode basis vectors, and the adjoint-domain inclusion by testing the adjoint relation against the same vectors. Extract this as a generic construction in DiagonalOperator.lean (lpDiag.diracDomain/diracDirac/diracDirac_isSelfAdjoint, parametrized by any family of symmetric blocks B i : G i ->l[k] G i), and have both Circle.lean and Torus.lean instantiate it instead of duplicating the proof. All public names and statements are preserved exactly (diracDomain, mem_diracDomain_iff, diracDirac, diracDirac_apply, diracDirac_isSelfAdjoint), so every downstream theorem (resolvent compactness, representation, grading, index_eq_zero) is unaffected -- verified axiom-clean, and the regenerated axiom report is byte-identical to the existing golden file. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
It was declared at the top of the whole lpDiag.diracDirac section, so every earlier lemma (diracDomain, diracDirac_apply, diracDirac_isFormalAdjoint, etc., none of which touch lp.single) picked it up as an unused hypothesis. Move it down to right before single_mem_diracDomain, where it's first actually needed, and add the now-possible omit clauses for CompleteSpace on lemmas that don't need adjoint/density machinery either. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
open scoped Classical (my previous fix) is itself flagged by the project's own style linter: it silently fills in decidability for every declaration that follows, which can hide statements that would be better off explicit. The linter's own suggestion is the right fix: declarations whose *statement* mentions lp.single (single_mem_diracDomain, diracDirac_single) take [DecidableEq alpha] as an explicit hypothesis; declarations that only need it inside their *proof* (dense_diracDomain, diracDirac_isSelfAdjoint) use the `classical` tactic instead, so the hypothesis never leaks into their type. diracDirac_le_adjoint needed neither, once decidability isn't pulled in via a blanket `variable`. No remaining linter warnings in the file; axiom report unchanged (Classical. choice was already a dependency everywhere in this development). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…red lemma The Torus.lean domain/self-adjointness refactor shifted every later declaration by ~98 lines; the new import in DiagonalOperator.lean shifted diagL/norm_diagL_le/ isCompactOperator_diagL by 1. Also adds a row for the new shared lpDiag.diracDirac_isSelfAdjoint lemma that Circle.lean and Torus.lean now both instantiate. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
JonBannon
changed the title
…ations The file/section-level summaries said this proves "the Hilbert-space case of the classical Riesz-Schauder theorem," but the classical theorem's conclusion includes index 0, which isFredholm_one_sub explicitly does not prove (its own docstring already says so). Reword the summaries to match: only the structural Fredholm-ness part (finite kernel, closed range, finite codimension) is proved. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
\and rendered fine in the PDF but plastex's web template dropped the word entirely, showing "Jon Bannon Michael R. Douglas". Spell it out literally so both renderers agree. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Follow-up to a redundancy sweep across
main: two genuine instances of the same mathematical fact being proved independently in more than one place, now consolidated into shared lemmas.Submodule.quotientEquivOrthogonal(+finrank_quotient_eq_finrank_orthogonal,finiteDimensional_quotient_of_finiteDimensional_orthogonal) inCompactOperators.lean:Examples/Shift.leanproved this fact by hand forHoverℂ, whileisFredholm_one_subindependently derived the same underlying fact inline for generalRCLike 𝕜. Extracted once, generalized, both call sites now reuse it.lpDiag.diracDomain/diracDirac/diracDirac_isSelfAdjointinDiagonalOperator.lean:Examples/Circle.lean(scalar eigenvalues) andExamples/Torus.lean(2×2 Hermitian spinor blocks) each proved, by hand, that their diagonal Dirac operator is self-adjoint on its maximalH¹domain via an essentially identical argument (symmetry from Hermitian blocks, domain density via single-mode basis vectors, adjoint-domain inclusion by testing against the same vectors). Generalized to any family of symmetric blocksB i : G i →ₗ[𝕜] G i; both files now instantiate it instead of duplicating the proof.Also:
[DecidableEq α]lint warnings inDiagonalOperator.leanproperly — per the project's own style linter, declarations whose statement needslp.singlekeep it as an explicit hypothesis; declarations that only need it inside their proof use theclassicaltactic instead.scripts/axiom_report.lean, which never picked upCompactOperators.lean's tracked declarations after an earlier merge.CompactOperators.lean's Riesz–Schauder content and the newFourierHolomorphic.lean(M3a/M3b: the exact dimension countdim H⁰(L_k) = k,dim H¹(L_k) = 0), which had landed onmainwithout blueprint coverage.file:linereferences inaudit/FAITHFULNESS.md(theTorus.leanrefactor shifted ~14 declaration lines by ~98; a new import inDiagonalOperator.leanshifted 3 more by 1) and added a row for the new sharedlpDiag.diracDirac_isSelfAdjointlemma.What did not change
All public names and statements are preserved exactly (
diracDomain,mem_diracDomain_iff,diracDirac,diracDirac_apply,diracDirac_isSelfAdjoint,fredholmIndex_shift,isFredholm_one_sub), so no downstream theorem needed any change — resolvent compactness, the algebra representations, grading,index_eq_zeroall build unchanged. The regenerated axiom report is byte-identical to the existing golden file.Checklist
Build & correctness
lake build SpectralTriplesis clean (no errors, no warnings).sorryand no newaxiom(search the diff).#print axiomsshows onlypropext,Classical.choice,Quot.sound.Assurance sync
scripts/axiom_report.leanlists every new/renamed headline declaration (and drops removed ones) — also backfilled the pre-existing gap forCompactOperators.lean.lake env lean scripts/axiom_report.lean > audit/axiom-report.txt— byte-identical to the prior committed version (no behavior change, only proof reorganization).audit/FAITHFULNESS.mdupdated: fixed stalefile:linereferences shifted by this PR's refactor, added a row for the new shared lemma.Definition changes
Test plan
lake buildclean across the whole project.lake env lean scripts/axiom_report.leanoutput is byte-identical to the committedaudit/axiom-report.txt.lpDiag.diracDirac_isSelfAdjoint,Circle.diracDirac_isSelfAdjoint,Torus.diracDirac_isSelfAdjoint,Torus.index_eq_zero,Shift.fredholmIndex_shift,Fredholm.isFredholm_one_sub) — all[propext, Classical.choice, Quot.sound].🤖 Generated with Claude Code