LEAN AXIOM REPORT
=================
Command: lake env lean Freudenthal/AxiomCheck.lean
Toolchain: Lean 4.30.0, Mathlib tag v4.30.0
Exit status: 0

'Freudenthal.all_edge_star_certificates_verified' depends on axioms: [propext]
'Freudenthal.exact_edge_config_catalogue_verified' depends on axioms: [propext]
'Freudenthal.exact_reference_norm_bounds_verified' depends on axioms: [propext]
'Freudenthal.exact_reference_norm_factorization_verified' depends on axioms: [propext]
'Freudenthal.exact_p4_two_cube_macro_patch_verified' depends on axioms: [propext]
'Freudenthal.assembleProtected_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Freudenthal.edgePatch_disjoint_of_same_colour' depends on axioms: [propext, Classical.choice, Quot.sound]
'Freudenthal.edgeColour_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'Freudenthal.protectedDependencyDepth_eq' does not depend on any axioms
'Freudenthal.referenceCubeEdges_card' does not depend on any axioms
'Freudenthal.tetrahedronEdgeCount' does not depend on any axioms
'Freudenthal.greedyColourBound_eq' does not depend on any axioms
'Freudenthal.correctedPatchOverlapBound_eq' does not depend on any axioms
'Freudenthal.rawLiftingSquaredConstant_value' depends on axioms: [propext]
'Freudenthal.degree_four_reference_bound' depends on axioms: [propext]
'Freudenthal.degree_five_reference_bound' depends on axioms: [propext]
'Freudenthal.scaling_exponents_cancel' depends on axioms: [propext]
'Freudenthal.raw_edge_star_finite_audit' depends on axioms: [propext, Classical.choice, Quot.sound]
