Audit.lean

1import BFPP23/-! Kernel dependency audit of every declaration in the BFPP namespace.4The allowlist is restricted to Lean's standard logical axioms.5-/67#print axioms BFPP.contractive_realization8#print axioms BFPP.BoundedFamily.supremum_nonexpansive9#print axioms BFPP.upperEnvelope_nonexpansive10#print axioms BFPP.Profile.subsolution_eq_zero11#print axioms BFPP.Profile.tail_mix12#print axioms BFPP.twoProfileSet_convex13#print axioms BFPP.twoProfileSet_isBounded14#print axioms BFPP.twoProfileSet_nonempty15#print axioms BFPP.TwoProfile.fixedPointFree_delay16#print axioms BFPP.isFSpace_of_hasBFPP17#print axioms BFPP.InseparableLevels.analyze_nonexpansive18#print axioms BFPP.InseparableLevels.contractive_realization19#print axioms BFPP.Profile.regularizeValue_continuous20#print axioms BFPP.Profile.positiveTail21#print axioms BFPP.Profile.center_add_positiveTail_dist22#print axioms BFPP.finite_synthesis_bounds_finset23#print axioms BFPP.stepCombination_denseRange24#print axioms BFPP.positiveSynthesis_exists25#print axioms BFPP.positiveSynthesis_unique26#print axioms BFPP.centeredSynthesis_dist27#print axioms BFPP.InseparablePair.synthesize_nonexpansive28#print axioms BFPP.InseparablePair.analyze_synthesize_le29#print axioms BFPP.InseparablePair.ballMap_fixedPointFree30#print axioms BFPP.InseparablePair.not_hasBFPP31#print axioms BFPP.countable_union_cozero32#print axioms BFPP.exists_first_bad_limit33#print axioms BFPP.not_hasBFPP_of_not_totallySeparated34#print axioms BFPP.exists_chainGap35#print axioms BFPP.exists_regular_cofinal_sequence36#print axioms BFPP.not_hasBFPP_of_zeroDimensional_not_ED37#print axioms BFPP.extremallyDisconnected_of_hasBFPP38#print axioms BFPP.exists_nonexpansive_fixedPointFree_of_not_ED39#print axioms BFPP.edSup_isLUB40#print axioms BFPP.exists_minimal_invariant_interval41#print axioms BFPP.fixedPoint_of_interval_balls42#print axioms BFPP.hasBFPP_iff_extremallyDisconnected43#print axioms BFPP.IsTCP.nonexpansive44#print axioms BFPP.encodedPropagator_isTCP45#print axioms BFPP.exists_transfinite_realization46#print axioms BFPP.exists_complex_fixedPointFree_of_not_ED47#print axioms BFPP.positiveSynthesis_measure_representation48#print axioms BFPP.synthesisMeasure_real_mass49#print axioms BFPP.exists_terminal_pointwise_supremum_of_not_ED50#print axioms BFPP.normalizedTerminal_norm51#print axioms BFPP.normalizedTerminal_not_continuous52#print axioms BFPP.exists_normalized_terminal_supremum53#print axioms BFPP.InseparablePair.synthesizeMap_convexIntegral_max_min54#print axioms BFPP.InseparablePair.synthesisMass_add_le_one55#print axioms BFPP.hasBFPP_iff_all_closedBalls56#print axioms BFPP.discrete_recurrence_nonexpansive5758open Lean Elab Command in59run_cmd do60  let env ← getEnv61  let allowed := #[``propext, ``Classical.choice, ``Quot.sound]62  let mut checked : Nat := 063  for (name, _) in env.constants.toList do64    if name.toString.startsWith "BFPP." then65      let axioms ← collectAxioms name66      for axiomName in axioms do67        unless allowed.contains axiomName do68          throwError "Unexpected axiom {axiomName} in {name}"69      checked := checked + 170  logInfo m!"Axiom audit passed for {checked} declarations in namespace BFPP."

SHA-256