IndisputableMonolith.Gravity.FreudenthalAxisStencilCoeffCert · Recognition explainer

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration module_import
IndisputableMonolith.Gravity.Track1BCorrectedQuadratic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance module_import

declarations in this module (115)

abbrev Vertex5 L23
abbrev PeriodicEdge5 L24
def addFin5 L26
def negFin5 L29
theorem addFin5_zero_left L32
theorem addFin5_neg_self L37
theorem addFin5_neg_add_self L42
theorem addFin5_self_add_neg L48
def translateVertex5 L54
def negVertex5 L57
def relativeVertex5 L60
def translateEdge5 L63
theorem translateVertex5_neg_left L66
theorem translateVertex5_neg_right L72
def translateVertex5Equiv L78
def translateEdge5Equiv L84
def subOneMod5 L96
def subBit5 L99
theorem subBit5_addFin5 L102
def matchingBaseCell5 L107
theorem matchingBaseCell5_spec L111
def selectedCell5 L116
theorem selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell L119
theorem matchingBaseCell5_translate L128
theorem selectedCell5_translate L137
theorem addVertexBits_translate5 L143
theorem translateEdge5_endpoints L153
def sqEdgeRat L165
def snormRat L173
theorem sqEdgeRat_cast_eq_freudenthalTetSqEdges L211
theorem snormRat_cast_eq_freudenthalSchlaefliTable L217
theorem freudenthalLocalPairDisp_eq_of_mem L223
theorem periodicDispSqEdge_eq_freudenthalTetSqEdges_of_mem L231
def sameUnordered L245
theorem sameUnordered_translate L248
def scaledPairLocalVertexCoeff L256
theorem scaledPairLocalVertexCoeff_translate L267
def mixedAxisEdgeLhsCoeff L276
theorem mixedAxisEdgeLhsCoeff_translate L283
def mixedAxisLhsCoeff L297
theorem mixedAxisLhsCoeff_eq_sum_edge L300
def axisStencilResidualCoeff L303
def mixedAxisResidualCoeff L311
def originVertex L314
theorem translateVertex5_origin_left L317
theorem relativeVertex5_origin_eq_self L322
theorem relativeVertex5_self_eq_origin L329
def FullResidualCoeffCert L337
def MixedAxisLhsCoeffTranslationInvariant L343
def MixedAxisEdgeLhsCoeffTranslationInvariant L351
theorem mixedAxisLhsCoeff_translationInvariant_of_edge L357
def rowMixedAxisLhsCoeffTranslationInvariant L381
def AxisStencilResidualCoeffTranslationInvariant L388
def MixedAxisResidualCoeffTranslationInvariant L396
def axisStencilResidualCoeffTranslationInvariantCheck L401
theorem axisStencilResidualCoeffTranslationInvariantCheck_eq_true L406
theorem axisStencilResidualCoeff_translationInvariant L410
theorem mixedAxisResidualCoeff_translationInvariant_of_lhs L420
def originResidualCoeffsZero L431
theorem originResidualCoeffsZero_eq_true L434
theorem originResidualCoeffCert L438
theorem fullResidualCoeffCert_of_translationInvariant L442
theorem fullResidualCoeffCert_of_lhs_translationInvariant L449
theorem fullResidualCoeffCert_of_edge_lhs_translationInvariant L455
theorem mixedAxisEdgeLhsCoeff_translationInvariant L461
theorem mixedAxisLhsCoeff_translationInvariant L466
theorem fullResidualCoeffCert L470
abbrev P5 L477
abbrev VertexPotential5 L480
def potentialAtVertex5 L483
theorem freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_selectedCell5 L488
def vertex5Code L509
theorem vertex5Code_injective L512
def vertex5CanonLE L519
theorem unorderedDiagonalMonomialExpansionAtN5 L527
theorem unorderedCrossMonomialExpansionAtN5 L551
theorem unorderedSameUnorderedMonomialExpansionAtN5 L636
theorem scaledPairLocalVertexCoeffExpansionAtN5 L677
theorem scaledPairLocalVertexCoeffEndpointSumExpansionAtN5 L796
def scaledPairEndpointExpansionValueAtN5 L854

… and 35 more