module module

`IndisputableMonolith.Verification.Item8ClosureTarget`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Physics.RunningCouplings module_import

declarations in this module (102)

inductive BpowSign L99
structure ResidualSignature L105
structure ResidualPair L114
structure RatioFamilyCoeffs L120
def leptonSignature L125
def upQuarkSignature L134
def downQuarkSignature L143
def ratioFamily L160
def predictedResiduals L172
theorem same_signature_same_prediction L178
def item8ClosureTarget L194
theorem consistency_of_ratioFamily L219
theorem consistency_necessary L235
structure RefinedCoeffs L257
def refinedFamily L262
def refinedPrediction L276
theorem refined_at_eta_zero L281
def refinedItem8ClosureTarget L286
def etaFromData L335
theorem etaL_gen12_identity L341
theorem etaL_gen23_identity L352
theorem eta_absorbs_consistency L365
theorem refinedFamily_neg_solvable L379
theorem refinedFamily_pos_solvable L417
theorem refinedFamily_neg_unique L460
theorem refinedFamily_pos_unique L515
theorem neg_cPos_irrelevant L564
theorem pos_cNeg_irrelevant L571
theorem refined_neg_sector_closure L584
structure SignClassCoeffs L622
def signClassFamily L631
theorem signClass_collapse_to_refined L647
def pdg_up L667
def pdg_charm L668
def pdg_top L669
def pdg_down L670
def pdg_strange L671
def pdg_bottom L672
def pdg_electron L673
def pdg_muon L674
def pdg_tau L675
def alphaStrong L679
def rungResidual L683
def upGen12Residual L686
def upGen23Residual L689
def downGen12Residual L692
def downGen23Residual L695
def leptonGen12Residual L698
def leptonGen23Residual L701
def upExact L706
def downExact L712
def leptonObserved L718
def item8Specialized L727
def allSectorTest L740
def refinedItem8Specialized L752
def refinedAllSectorTest L758
def leptonEta L773
def upQuarkEta L778
def downQuarkEta L782
def kappaLeptonCandidate L799
theorem kappaLeptonCandidate_pos L801
theorem kappaLeptonCandidate_ne_zero L805
theorem leptonLogAsym_pos L809
theorem leptonLogAsym_ne_zero L813
theorem leptonGen12Residual_pos L817
theorem leptonGen12Residual_ne_zero L835
theorem leptonGen23Residual_neg L839
theorem leptonCrossDiff_pos L860
theorem leptonCrossDiff_ne_zero L864
theorem leptonSectorClosure L871
def leptonAnchoredCNeg L887
def leptonAnchoredCoeffs L893
def alphaS6At L904
def alphaSAtTopThreshold L909
def alphaS5At L913
def alphaSAtBottomThreshold L918
def alphaS4At L922
def alphaSAtCharmThreshold L927
def alphaS3At L931
def alphaSPiecewise L936

… and 22 more