module
module
IndisputableMonolith.Gravity.SevenGaps.Gap2LabeledWeightBridge
show as:
view Lean formalization →
depends on (2)
declarations in this module (18)
-
class
of -
def
Zlabeled -
theorem
labeledSum_eq_classMass_sum -
theorem
classMass_gibbs_eq_mu -
theorem
gibbsZ_eq_Zq -
theorem
gibbs_fiberExcess_vanishes -
theorem
Z_eq_Zlabeled_mu -
theorem
classMass_mu_eq_orbit_mul_mu -
theorem
muZ_eq_Zq_of_trivial_orbits -
theorem
gibbs_ne_mu_of_nontrivial_orbit -
structure
BridgeStatus -
def
bridgeStatus -
theorem
status_bridge -
theorem
status_gibbs_matches -
theorem
status_excess -
theorem
status_Z_is_mu -
theorem
status_intent_open -
theorem
bridge_grounded