module module

`IndisputableMonolith.CondensedMatter.JCostPhaseTransition`

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 (10)

def J_cost L11
def phi_critical_energy L14
def sc_gap_scale L17
def T_critical L20
theorem J_cost_minimum_at_one L22
theorem J_cost_positive_away_from_one L26
theorem J_cost_symmetric L36
theorem phi_critical_value L39
theorem phi_critical_numeric L43
theorem sc_prediction L59