module module

`IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

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

IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (22)

def correction_D_half L65
def correction_F_quarter L68
def correction_E_eighth L71
def correction_D_quad1 L74
def correction_D_quad2 L77
theorem D_half_at_3 L81
theorem F_quarter_at_3 L85
theorem E_eighth_at_3 L90
theorem D_quad1_at_3 L95
theorem D_quad2_at_3 L99
theorem F_quarter_eq_D_half L107
theorem F_quarter_not_alternative L115
def AxisAdditive L123
theorem axisAdditive_linear L127
structure AdmissibleCorrection L150
theorem admissible_unique L155
theorem D_half_admissible L180
theorem F_quarter_admissible L188
theorem E_eighth_not_axisAdditive L197
theorem D_quad1_not_axisAdditive L208
theorem D_quad2_not_axisAdditive L216
theorem tau_correction_unique_admissible L226