2607.19268v1 / BootsRoyle/Audit.lean

all files

import BootsRoyle

/-!
Running this file prints Lean's axiom audit for representative top-level
results.  The output contains only the ordinary foundations used by mathlib
(`propext`, `Quot.sound`, and `Classical.choice`), and no project axiom.
-/

#print axioms BootsRoyle.exists_l1_normalized_perronVector
#print axioms BootsRoyle.adjacencySpectralRadius_strictMono_of_connected
#print axioms BootsRoyle.PerronData.lambda_eq_four_add_excess_sub_cubicWeight
#print axioms BootsRoyle.PerronData.sum_degreeExcess_eq
#print axioms BootsRoyle.selectedFace_averaging