IndisputableMonolith.Gravity.Analysis.Regge4DSchlaefliPathwise

declarations in this module (76)

• abbrev SqEdges4 L51
• def localEdge L55
• def localHinge L56
• def flatSqEdges L57
• theorem flatSqEdges_eq_seed L59
• def hingeBoundarySlots L62
• theorem hingeBoundarySlots_zero L75
• def hingeFlatEdgeSq L80
• def hingeAreaFlat L84
• lemma heron_eval L88
• lemma sqrt_one_quarter L92
• lemma sqrt_half L96
• lemma sqrt_three_quarter L101
• theorem hingeAreaFlat_0 L107
• theorem hingeAreaFlat_1 L113
• theorem hingeAreaFlat_2 L119
• theorem hingeAreaFlat_3 L125
• theorem hingeAreaFlat_4 L131
• theorem hingeAreaFlat_5 L137
• theorem hingeAreaFlat_6 L143
• theorem hingeAreaFlat_7 L149
• theorem hingeAreaFlat_8 L155
• theorem hingeAreaFlat_9 L161
• theorem hingeAreaFlat_pos L167
• def flatSchlaefliSummandQ L184
• def flatSchlaefliSummand L205
• abbrev flatSchlaefliSummandReal L207
• lemma univ10 L209
• lemma sum10 L213
• theorem freudenthal4SimplexFlatSchlaefli L222
• theorem freudenthal4SimplexFlatSchlaefli_real L228
• theorem seed_hinge_is_zero L234
• lemma seed_summand_mul_angle L236
• theorem flatSchlaefliSummand_seed_eq_area_angleKernel L241
• def flatHingeData L281
• def flatSchlaefliData L285
• theorem flatSchlaefliIdentity L292
• theorem flat_schlaefliN_kills L304
• def freudenthal4SimplexFlatSchlaefliPresent L310
• theorem freudenthal4SimplexFlatSchlaefliPresent_true L312
• def seedDihedralAngle L319
• theorem cosDihedral_flat_ne_endpoints L321
• theorem arccos_chain_factor_flat L335
• theorem coordPath_at_seed L343
• theorem hasDerivAt_seedDihedralAngle_coord L350
• def affineThroughFlat L376
• theorem affineThroughFlat_zero L379
• theorem coordPath_eq_affine L384
• def flatAngleJacobian L396
• theorem flatAngleJacobian_seed L399
• def flatDirectionalAngleDeriv L407
• lemma mul_div_cancel_area L410
• theorem freudenthal4SimplexFlatDirectionalSchlaefli L422
• theorem freudenthal4SimplexFlatDirectionalSchlaefli_coord L447
• def freudenthal4SimplexFlatDirectionalSchlaefliPresent L457
• theorem freudenthal4SimplexFlatDirectionalSchlaefliPresent_true L459
• def hingeVertexPerm L469
• def hingeVertexPermInv L482
• def pullEdgeSlot L495
• def remappedSqEdges L517
• theorem remappedSqEdges_seed_id L520
• theorem remappedSqEdges_zero L524
• theorem remapped_seed_dihedral_eq L527
• structure Nondeg4Simplex L533
• theorem nondeg_flat L540
• def seedCosDihedral L548
• def freudenthal4SimplexPathwiseSchlaefliPresent L551
• theorem freudenthal4SimplexPathwiseSchlaefliPresent_false L553
• def Freudenthal4SimplexPathwiseSchlaefliTarget L557
• theorem Freudenthal4SimplexPathwiseSchlaefliTarget_open L560
• def PathwiseFlatRemainder L567
• theorem pathwiseFlatRemainder_flat_zero L576
• theorem pathwiseFlatRemainder_directional_zero L600
• structure Regge4DSchlaefliPathwiseStatus L608
• def regge4DSchlaefliPathwiseStatus L617
• theorem regge4DSchlaefliPathwiseStatus_flags L626