IndisputableMonolith.Gravity.Track1BCorrectedQuadratic

declarations in this module (17)

• def ReggeLocalQuadraticCorrespondence L84
• theorem edgeStencilLocalCorrespondence_iff L96
• def CanonicalPeriodicAxisStencilLocalCorrespondence L110
• theorem canonicalPeriodicMixedAxisStencilAction_nonneg L121
• theorem canonicalPeriodicMixedAxisStencilAction_smul L133
• theorem periodicEdgeStencilDirichletAction_smul L152
• theorem reggeLocalQuadraticCorrespondence_quadratic_unique L175
• theorem both_correspondences_force_equal_quadratics L270
• def AxisEdgeStencilQuadraticsDiffer L291
• theorem not_both_correspondences_of_quadratics_differ L303
• theorem normalized_regge_sub_half_quadratic_abs_le L321
• theorem axis_normalized_regge_bound_of_correspondence L358
• abbrev CanonicalPeriodicCorrectedTrack1BGateAtN5 L392
• theorem correctedTrack1BGateAtN5_closed L401
• theorem correctedMixedTargetAtN5_of_gate L405
• structure CorrectedTrack1BStatus L413
• def correctedTrack1BStatus L426