IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4D

declarations in this module (36)

• theorem actually L14
• theorem frobId_axisTTPlus L80
• theorem frobId_axisTTCross L85
• theorem waveId_symbolDir L90
• theorem axisTTPlus_isTT_symbolDir L98
• theorem axisTTCross_isTT_symbolDir L106
• theorem dict_m2_axisTTPlus_symbolDir L120
• theorem dict_m2_axisTTCross_symbolDir L126
• theorem geom_m2_axisTTPlus_symbolDir L138
• theorem geom_m2_axisTTCross_symbolDir L142
• theorem geom_m2_decoyGauge_symbolDir L146
• theorem geom_ne_dict_axisTTPlus L154
• theorem geom_ne_dict_axisTTCross L161
• theorem dict_eq_two_geom_axisTTPlus L168
• theorem dict_eq_two_geom_axisTTCross L174
• theorem factor_pinned_axisTTPlus L184
• theorem factor_pinned_axisTTCross L191
• theorem factor_one_fails L199
• theorem factor_four_fails L207
• theorem doubled_fold_is_the_named_object L217
• theorem two_distinct_bookkeeping_factors L227
• theorem ehFace_axisTTPlus_symbolDir L238
• theorem ehFace_eq_four_times_geom L248
• theorem reggeFace_between L256
• theorem vanishing_witness_admits_every_factor L275
• theorem decoyGauge_admits_every_factor L284
• theorem tt_witness_is_informative L292
• theorem banked_coefficient_is_not_the_certificate_value L301
• theorem the_numerals_coincide L310
• def FoldTimesTwoEqDictionaryM2 L323
• def FoldTimesTwoEqDictionaryAtBankedWitnesses L332
• theorem foldTimesTwoEqDictionaryAtBankedWitnesses_holds L338
• def FoldDictionaryFactorDischarged L345
• theorem foldDictionaryFactorDischarged_holds L358
• def ConvergenceReachesDictionaryNotTheHingeMoment L365
• theorem convergenceReachesDictionaryNotTheHingeMoment_holds L372