Masses

Masses modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.

45 modules · 505 thm/lemma · 7344 lines

module	thm	lemma	def	lines	papers
`Masses.AlphaGScoreCard`	12	0	3	226	—
`Masses.Anchor`	10	0	10	210	—
`Masses.AnchorDerivation`	6	0	6	111	—
`Masses.AnchorPolicy`	0	0	10	102	—
`Masses.Assumptions`	0	0	1	33	—
`Masses.BaselineDerivation`	24	0	11	320	—
`Masses.Basic`	0	1	2	21	—
`Masses.BosonVerification`	7	0	6	109	—
`Masses.ChargedLeptonMassScoreCard`	6	0	0	61	—
`Masses.CoherenceExponent`	18	0	5	141	—
`Masses.ElectroweakMasses`	9	3	8	145	—
`Masses.Exponent.Gauge`	0	3	1	27	—
`Masses.GapFunctionForcing`	5	6	2	252	—
`Masses.HeavyQuarkFullClosureObstruction`	5	0	9	83	—
`Masses.JCostPerturbation`	88	0	1	1634	—
`Masses.KernelTypes`	0	0	2	35	—
`Masses.LeptonMassLadder`	7	0	3	95	—
`Masses.LeptonSubLeadingForcing`	10	0	3	134	—
`Masses.Manifest`	0	0	1	20	—
`Masses.MassHierarchy`	5	0	1	68	2
`Masses.MassLaw`	3	0	2	82	—
`Masses.MassRatiosProved`	4	0	0	99	—
`Masses.MuRatioScoreCard`	6	2	2	142	—
`Masses.NeutrinoYardstick`	5	0	4	89	—
`Masses.NumericalPredictions`	14	2	0	201	—
`Masses.QuarkAbsoluteBridgeScoreCard`	14	0	1	171	—
`Masses.QuarkAnchorDerivation`	11	0	3	76	—
`Masses.QuarkSchemeReconciliation`	7	0	2	165	—
`Masses.QuarkScoreCard`	19	0	1	236	—
`Masses.QuarkVerification`	10	0	6	174	—
`Masses.RSBridge.Anchor`	5	0	10	188	—
`Masses.Ribbons`	1	0	17	146	—
`Masses.Ribbons.Tick`	0	0	0	17	—
`Masses.Ribbons.Word`	0	0	0	21	—
`Masses.RungConstructor.Basic`	0	0	2	43	—
`Masses.RungConstructor.Motif`	0	0	13	117	—
`Masses.RungConstructor.Proofs`	43	0	0	137	—
`Masses.SDGTForcing`	16	0	6	165	—
`Masses.SMVerification`	15	0	10	178	—
`Masses.SectorDependentTorsion`	48	0	25	315	—
`Masses.SectorParams`	0	0	0	3	2
`Masses.SectorPrimitive`	0	0	1	25	—
`Masses.StepValueEnumeration`	11	0	3	262	—
`Masses.TopQuarkMassScoreCard`	6	0	1	62	—
`Masses.Verification`	23	15	14	403	—

full source mirrored from github.com/jonwashburn/shape-of-logic