IndisputableMonolith.Gravity.SevenGaps.StationarityBridgeClosure

declarations in this module (23)

• theorem supplies L122
• theorem stationaryLogRatio_total_strain L137
• theorem stationaryRatio_cubic L156
• def recognitionRatioBridge_ofStationarity L208
• theorem ofStationarity_xRatio_def L227
• theorem ofStationarity_log_xRatio L239
• theorem ofStationarity_log_xRatio_eq_minimizer_strain L251
• theorem ofStationarity_minimizer_grounding L267
• theorem ofStationarity_log_xRatio_pos L283
• theorem ofStationarity_log_xRatio_neg L295
• theorem linear_deficit_family_not_isAdmissible L328
• def quadraticSourceFamily L372
• theorem quadraticSourceFamily_isAdmissible L386
• theorem quadraticSourceFamily_deficit_ne_zero L409
• theorem quadraticSourceFamily_logRatio_pos L421
• theorem quadraticSourceFamily_source_dominated L443
• theorem concreteBridge_hdom L469
• def concreteStationarityBridge L486
• theorem concreteStationarityBridge_nonvacuous L498
• theorem concreteStationarityBridge_logRatio_signed L524
• structure StationarityBridgeClosureStatus L566
• def stationarityBridgeClosureStatus L575
• theorem stationarityBridgeClosureStatus_flags L581