module module

`IndisputableMonolith.Foundation.ScaleHomogeneityNoGo`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

declarations in this module (31)

structure ScaleAction L49
def IsJointScaleInvariantSelector L62
def IsScaleInvariant L67
theorem no_scaleInvariantSelector_forces_value L75
theorem forcingSelector_not_jointScaleInvariant L90
def PositivitySelector L100
theorem positivitySelector_jointScaleInvariant L102
theorem positivitySelector_does_not_force_value L112
structure ScaleHomogeneityNoGoCert L121
theorem scaleHomogeneityNoGoCert L138
def pairScaleAction L153
def pairRatio L159
theorem pairRatio_scaleInvariant L161
theorem pair_witness L170
def vecScaleAction L180
def probWeight L187
theorem probWeight_scaleInvariant L190
theorem vec_witness L204
structure ScaledConfigSpace L235
def IsInvariantSelector L251
theorem selected_amplitudes_eq_zero_or_all_pos L256
theorem no_forced_positive_amplitude L277
def quadrantSpace L294
def quadrantSelector L305
theorem quadrantSelector_invariant L307
def quadrantPoint21 L322
theorem quadrantPoint21_selected L325
theorem quadrantPoint21_amplitude L329
theorem quadrant_witness L331
theorem quadrant_ratio_pinned L343
theorem quadrant_ratio_scaleInvariant L350