IndisputableMonolith.QFT.CasimirRecognitionBoundary

declarations in this module (16)

• structure BoundaryModeInventory L27
• def modeInventoryDeficit L35
• def inventoryRatio L39
• def renormalizedBoundaryCost L43
• theorem inventoryRatio_pos L47
• theorem renormalizedBoundaryCost_nonneg L53
• theorem renormalizedBoundaryCost_eq_zero_of_balanced L59
• theorem deficit_pos_iff L67
• theorem inventoryRatio_gt_one_of_deficit_pos L73
• theorem renormalizedBoundaryCost_pos_of_deficit_pos L82
• def pressureFromCostGradient L93
• theorem attractive_of_positive_cost_gradient L97
• structure EMRecognitionBoundaryBridge L106
• theorem bridge_attractive_of_positive_gradient L116
• structure RecognitionBoundaryCert L124
• def recognitionBoundaryCert L137