2607.20408v1 / Repro/Audit.lean

all files

import Repro.CentralClaim
import Repro.PaperErrors

/-!
# Kernel-assumption audit

The `#print axioms` commands below are part of the reproducible verification
trace.  Each theorem should report only standard logical principles already used
by mathlib (`propext`, `Classical.choice`, and/or `Quot.sound`), never a
project-specific assumption.
-/

#print axioms ExtremeValues.extreme_values_of_quadratic_dirichlet_L
#print axioms ExtremeValues.extreme_lower_bound_of_resonance
#print axioms ExtremeValues.jacobiCharacter_apply_nat
#print axioms ExtremeValues.jacobiCharacter_isQuadratic
#print axioms PaperErrors.g2_product_sign_counterexample
#print axioms PaperErrors.chiNegFour_gammaFactor