IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation

declarations in this module (34)

• def faceCount L103
• def faceVertexCount L106
• theorem faceVertexCount_D3 L109
• theorem faceCount_D3 L112
• def deltaStructural L121
• def deltaAxisAdditive L125
• theorem deltaStructural_D3 L130
• theorem deltaAxisAdditive_D3 L135
• theorem delta_D3_derived L143
• theorem deltaStructural_alt_D3 L159
• theorem deltaStructural_eq_half_D3 L165
• theorem faceVertexRatio_D3 L185
• theorem D3_has_2D_faces L191
• def continuousMeasure3D L208
• def discreteMeasure2DFace L211
• theorem discreteMeasure_eq_4 L214
• def eMuContribution L218
• def muTauContribution L222
• theorem muTauContribution_eq L226
• theorem discrete_continuous_duality L236
• theorem vertices_are_anchors L267
• inductive CellDim L295
• def cellCount L303
• def anchorsPerCell L310
• def localCoeff L317
• theorem localCoeff_vertex L320
• theorem localCoeff_edge L324
• theorem localCoeff_face L328
• theorem localCoeff_cube L332
• theorem localCoeff_eq_three_halves_iff L339
• theorem localCoeff_face_ne_edge L377
• theorem localCoeff_face_ne_cube L382
• theorem edge_over_cube_vertices_eq_face_over_face_vertices L389
• theorem delta_derived_not_calibrated L404