Lean 4 formalization of the Fricke involution W_N = !![0,-1;N,0] on Γ₀(N) and the operator it
induces on modular forms. Merged via #1.
Build: lake build SocrateAI → 3053 jobs, 0 errors, 0 sorry.
Axiom discipline: 16 headline theorems pinned by build-failing #guard_msgs in #print axioms
guards in FinalCheck.lean; every footprint is exactly [propext, Classical.choice, Quot.sound].
A deliberately-wrong negative control (scratch/GuardNegativeControl.lean) was verified to fail,
so the guards are known to be load-bearing rather than vacuous.
| Module | Content |
|---|---|
FrickeInvolution |
W_N ∈ GL(2,ℝ)⁺, W_N² = −N·I, conjugation frickeConj, W γ W⁻¹ ∈ Γ₀(N) |
FrickeSlash |
slash-invariance preserved → operator on SlashInvariantForm |
FrickeModular |
holomorphy + cusp-boundedness transported → operator on bundled ModularForm |
FrickeComposite |
(f∣W)∣W = (−1)^k N^(k−2) f |
dag/ carries the statement-dependency graph (11/15 proved, acyclic), a natural-language
description per node, and a validator enforcing that every node marked proved names an existing
declaration and depends only on proved nodes.
No priority is claimed. anthropics/fermats-last-theorem already contains Fricke and
Atkin–Lehner material in Lean 4, including atkinLehnerLin — a ℂ-linear operator on ModularForm
for the whole Atkin–Lehner family. This is an independent, Mathlib-idiomatic treatment, not a first.
See PRIOR_ART_FINDING.md in SocrateAI-Scientific-Communication.
Build caveat: lakefile.lean, lake-manifest.json and lean-toolchain are excluded from the
repo — they hard-code absolute paths to a local Mathlib package pool. Built against Lean 4.32.2 +
Mathlib 905b9581. A portable lakefile is outstanding work; this release is not yet
build-reproducible by a third party.