scripts.cost_unit_axiom_audit

   1/-
   2Kernel audit for the cost-unit slice, run against the public tree.
   3
   4The two papers claim that the classification of the anchor-free cost ledger and the
   5leastness of `J` over it carry no project-local axioms, and that the six exponentials
   6theorem enters as an explicit hypothesis rather than as an axiom. `#print axioms` is
   7the check: each declaration below must report only `propext`, `Classical.choice` and
   8`Quot.sound`, the three axioms of the ambient proof assistant. A named hypothesis is
   9invisible to this command by construction, which is the point of stating it in the type.
  10
  11Run: `lake env lean scripts/cost_unit_axiom_audit.lean`
  12-/
  13import IndisputableMonolith.Cost.GaugeOrbitClassification
  14import IndisputableMonolith.Cost.UnitFromMinimality
  15import IndisputableMonolith.Cost.MonotoneMultiplicativePower
  16import IndisputableMonolith.Cost.FunctionalEquation
  17
  18#print axioms IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost.GaugeOrbitIsSignedPowerFamily_of_sixExponentials
  19#print axioms IndisputableMonolith.Cost.MonotonePower.exists_exponent
  20
  21-- The nondegeneracy dichotomy. None of these takes the six exponentials hypothesis, so a
  22-- clean report here is the whole claim: the condition that separates the degenerate solution
  23-- from every other one is decided inside the kernel from the ledger alone.
  24#print axioms IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost.vanishes_at_two_iff_trace_two
  25#print axioms IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost.vanishes_at_two_iff_flat
  26#print axioms IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost.charges_positively_at_two
  27#print axioms IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost.strict_somewhere_iff_charges_at_two
  28#print axioms IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost.charges_at_two_iff_not_signGauge
  29#print axioms IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost.signGauge_sees_orientation_only
  30
  31#print axioms IndisputableMonolith.Cost.UnitFromMinimality.jcost_lt_pow
  32#print axioms IndisputableMonolith.Cost.UnitFromMinimality.anchor_is_minimality_over_powers
  33#print axioms IndisputableMonolith.Cost.FunctionalEquation.law_of_logic_forces_jcost
  34#print axioms IndisputableMonolith.Cost.FunctionalEquation.hasLogCurvature_full_filter_forces_zero
  35