2607.19283v1 / ENOTV/Audit.lean

all files

import ENOTV.Representation

/-!
# Kernel audit

These commands make Lean print the logical footprint of all versions of the
central theorem.  The output contains only mathlib's standard logical
principles (`propext`, `Classical.choice`, and `Quot.sound`); the three
mathematical inputs are ordinary explicit arguments of the theorem.
-/

#print axioms ENOTV.eno_tv_parity_dichotomy
#print axioms ENOTV.eno_tv_parity_dichotomy_paper
#print axioms ENOTV.eno_tv_parity_dichotomy_literal