module
module
IndisputableMonolith.Complexity.NonNaturalness
show as:
view Lean formalization →
used by (2)
depends on (4)
declarations in this module (16)
-
def
FalsePointFraction -
theorem
falsePointFraction_nonneg -
theorem
falsePointFraction_le_one -
theorem
const_true_zero_fraction -
theorem
const_false_full_fraction -
def
ComplexityProperty -
structure
IsLarge -
structure
IsConstructive -
structure
IsUseful -
structure
IsNatural -
def
HighDepthProp -
theorem
high_depth_empty -
theorem
high_depth_not_large -
theorem
jfrust_not_natural -
structure
NonNaturalnessCert -
def
nonNaturalnessCert