IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG

declarations in this module (24)

• def TypedResidual_gap5_background_weight_blocker L68
• def TypedResidual_gap5_dynamic_bracket L76
• def TypedResidual_gap5_phaseSpaceDependentDirac L80
• def TypedResidual_gap5_dynamic_continuum_smearing_residual L84
• def TypedResidual_gap5_dynamic_bracket_shape_continuum L90
• def TypedResidual_gap5_dirac_algebra_continuum_limit L102
• def TypedResidual_gap5_hkt_rigidity_frozen L114
• def TypedResidual_gap5_hkt_one_site_falsification L118
• def TypedResidual_gap5_hkt_dyn_target_defined L124
• def TypedResidual_gap5_hkt_rigidity L133
• def TypedResidual_gap5_dynamicDirac_and_hkt L138
• theorem typedResidual_gap5_background_weight_blocker L143
• theorem concreteDynamicInverseMetric_not_constant_witness L147
• theorem typedResidual_gap5_dynamic_bracket_closed L152
• theorem typedResidual_gap5_phaseSpaceDependentDirac_closed L157
• theorem typedResidual_gap5_dynamic_continuum_smearing_closed L162
• theorem typedResidual_gap5_dynamic_bracket_shape_continuum_closed L167
• theorem typedResidual_gap5_dirac_algebra_continuum_limit_closed L173
• theorem typedResidual_gap5_hkt_one_site_falsification_closed L180
• theorem typedResidual_gap5_hkt_dyn_target_defined_banked L186
• structure Gap5ResidualDAGStatus L192
• def gap5ResidualDAGStatus L204
• theorem gap5ResidualDAGStatus_flags L216
• theorem gap5_closed_after_residual_dag L232