IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration

declarations in this module (209)

• def Track2ManyBodyEndpoint L48
• theorem track2_many_body_endpoint_holds L63
• def Track1SchlaefliReductionEndpoint L69
• theorem track1_schlaefli_reduction_endpoint_holds L74
• def Track1Disp0BaseVertexReductionEndpoint L81
• theorem track1_disp0_base_vertex_reduction_endpoint_holds L87
• def Track1Disp0StationaryReductionEndpoint L93
• theorem track1_disp0_stationary_reduction_endpoint_holds L98
• def Track1DispStationaryReductionEndpoint L105
• theorem track1_disp_stationary_reduction_endpoint_holds L111
• def Track1SevenStationarityEndpoint L118
• theorem track1_seven_stationarity_endpoint_holds L123
• def Track1ForallDispStationarityPackagingEndpoint L130
• theorem track1_forall_disp_stationarity_packaging_endpoint_holds L135
• def Track1ForallDispStationarityEndpoint L142
• theorem track1_forall_disp_stationarity_endpoint_holds L147
• def track1ForallDispStationarityEndpointProjectionCount L152
• theorem track1ForallDispStationarityEndpointProjectionCount_eq_one L154
• def Track1TotalSymmetryStationarityReductionEndpoint L159
• theorem track1_total_symmetry_stationarity_reduction_endpoint_holds L165
• def track1TotalSymmetryStationarityReductionEndpointProjectionCount L170
• theorem track1TotalSymmetryStationarityReductionEndpointProjectionCount_eq_one L172
• def Track1TotalSymmetryStationarityEndpoint L177
• theorem track1_total_symmetry_stationarity_endpoint_holds L183
• def track1TotalSymmetryStationarityEndpointProjectionCount L188
• theorem track1TotalSymmetryStationarityEndpointProjectionCount_eq_one L190
• def Track1ConformalSchlaefliEndpoint L200
• theorem track1_conformal_schlaefli_endpoint_holds L206
• def Track1ConformalSchlaefliLocalExpansionEndpoint L213
• theorem track1_conformal_schlaefli_local_expansion_endpoint_holds L219
• def Track1ConformalSchlaefliNearZeroExpansionEndpoint L226
• theorem track1_conformal_schlaefli_near_zero_expansion_endpoint_holds L230
• def Track1ConformalSchlaefliNearZeroLocalReductionEndpoint L237
• theorem track1_conformal_schlaefli_near_zero_local_reduction_endpoint_holds L244
• def Track1ConformalSchlaefliNearZeroChainRuleEndpoint L251
• theorem track1_conformal_schlaefli_near_zero_chain_rule_endpoint_holds L255
• def Track1ConformalSchlaefliNearZeroClosedFormEndpoint L261
• theorem track1_conformal_schlaefli_near_zero_closed_form_endpoint_holds L265
• def Track1ConformalSchlaefliNearZeroLocalEndpoint L271
• theorem track1_conformal_schlaefli_near_zero_local_endpoint_holds L275
• def Track1ConformalSchlaefliNearZeroStationarityEndpoint L282
• theorem track1_conformal_schlaefli_near_zero_stationarity_endpoint_holds L287
• def Track1LocalCorrespondenceReducedToMixedLengthEndpoint L294
• theorem track1_local_correspondence_reduced_to_mixed_length_endpoint_holds L299
• def Track1MixedLengthAuditObstructionEndpoint L307
• theorem track1_mixed_length_audit_obstruction_endpoint_holds L311
• def Track1MixedAxisStencilReductionEndpoint L317
• theorem track1_mixed_axis_stencil_reduction_endpoint_holds L322
• def Track1MixedAxisCoeffCertEndpoint L330
• theorem track1_mixed_axis_coeff_cert_endpoint_holds L334
• def Track1MixedAxisRow100CoeffCertEndpoint L342
• theorem track1_mixed_axis_row100_coeff_cert_endpoint_holds L346
• def Track1MixedAxisOriginPropCoeffCertEndpoint L353
• theorem track1_mixed_axis_origin_prop_coeff_cert_endpoint_holds L357
• def Track1MixedAxisTranslationReductionEndpoint L365
• theorem track1_mixed_axis_translation_reduction_endpoint_holds L369
• def Track1MixedAxisStencilRhsTranslationEndpoint L376
• theorem track1_mixed_axis_stencil_rhs_translation_endpoint_holds L380
• def Track1MixedAxisLhsTranslationReductionEndpoint L387
• theorem track1_mixed_axis_lhs_translation_reduction_endpoint_holds L391
• def Track1MixedAxisEdgeLhsTranslationReductionEndpoint L399
• theorem track1_mixed_axis_edge_lhs_translation_reduction_endpoint_holds L403
• def Track1MixedAxisEdgeLhsTranslationEndpoint L410
• theorem track1_mixed_axis_edge_lhs_translation_endpoint_holds L414
• def Track1MixedAxisLhsTranslationEndpoint L421
• theorem track1_mixed_axis_lhs_translation_endpoint_holds L425
• def Track1MixedAxisFullResidualCoeffCertEndpoint L431
• theorem track1_mixed_axis_full_residual_coeff_cert_endpoint_holds L435
• def Track1MixedAxisRhsSoundnessEndpoint L441
• theorem track1_mixed_axis_rhs_soundness_endpoint_holds L445
• def Track1MixedAxisExplicitFiberLhsSoundnessEndpoint L451
• theorem track1_mixed_axis_explicit_fiber_lhs_soundness_endpoint_holds L455
• def Track1MixedAxisExplicitFiberAxisSoundnessEndpoint L461
• theorem track1_mixed_axis_explicit_fiber_axis_soundness_endpoint_holds L465
• def Track1MixedAxisExplicitFiberAxisStencilTargetEndpoint L470
• theorem track1_mixed_axis_explicit_fiber_axis_stencil_target_endpoint_holds L474
• def Track1MixedAxisCorrectedAxisStencilTargetEndpoint L479
• theorem track1_mixed_axis_corrected_axis_stencil_target_endpoint_holds L483
• def Track1MixedAxisCoeffSoundnessToExplicitFiberEndpoint L491
• theorem track1_mixed_axis_coeff_soundness_to_explicit_fiber_endpoint_holds L496

… and 129 more