module module

`IndisputableMonolith.Physics.CooperPair`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import
IndisputableMonolith.Foundation.EightTick module_import

declarations in this module (13)

theorem time_reversed_pair_zero_cost L29
theorem pairing_lowers_cost L38
theorem cooper_criterion L51
def bcs_gap L67
theorem bcs_gap_positive L71
def bcs_Tc L81
theorem bcs_Tc_positive L85
theorem universal_bcs_ratio L93
theorem ratio_approx_3_52 L104
theorem meissner_effect_structural L115
def london_depth L125
theorem london_depth_positive L128
theorem isotope_effect L140