IndisputableMonolith.Foundation.DAlembert.CurvatureGate

declarations in this module (21)

• def G_of_F L38
• def H_of_F L41
• def Gquad L46
• def Gcosh L49
• def Gspher L52
• def SatisfiesHyperbolicODE L57
• def SatisfiesFlatODE L61
• def SatisfiesSphericalODE L65
• theorem Gquad_satisfies_flat L71
• theorem Gcosh_satisfies_hyperbolic L90
• theorem Gspher_satisfies_spherical L104
• theorem Gquad_not_hyperbolic L124
• theorem Gcosh_not_flat L140
• theorem Gspher_nonpositive L155
• theorem Gspher_negative_at_pi L162
• def IsNonNegativeG L167
• theorem Gspher_violates_nonnegativity L170
• inductive CurvatureType L179
• theorem curvature_gate_main L195
• theorem curvature_gate_dichotomy L225
• theorem curvature_gate_summary L249