module module

`IndisputableMonolith.Derivations.MassToLight`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (21)

structure via L20
def phi L57
def phi_power L60
lemma phi_gt_one L64
lemma phi_lt_two L71
lemma phi_gt_1_6 L81
lemma phi_lt_1_7 L90
theorem phi_10_bounds L99
theorem phi_13_bounds L107
theorem ml_is_phi_power L123
def cycleLength L183
def massPhase L186
def lightPhase L189
theorem phase_ratio_from_topology L192
theorem ml_from_phase_ratio L197
theorem ml_consistent_with_observation L204
theorem ml_is_derived_not_input L221
def H_MLUncertaintyIsDiscrete L243
theorem ml_uncertainty_is_discrete L249
def H_MLFollowsPhiStructure L262
theorem ml_follows_phi_structure L267