RRF

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

32 modules · 165 thm/lemma · 4271 lines

module	thm	lemma	def	lines	papers
`RRF.Core`	0	0	0	38	—
`RRF.Core.DisplayChannel`	4	0	3	81	—
`RRF.Core.Glossary`	0	0	4	88	—
`RRF.Core.Octave`	1	0	6	127	—
`RRF.Core.Recognition`	4	0	2	73	—
`RRF.Core.Strain`	2	0	10	120	—
`RRF.Core.Vantage`	5	0	6	107	—
`RRF.Foundation`	0	0	0	68	—
`RRF.Foundation.Consciousness`	8	0	5	220	—
`RRF.Foundation.Constants`	7	0	11	190	—
`RRF.Foundation.Gravity`	6	0	10	166	—
`RRF.Foundation.Ledger`	5	0	12	218	—
`RRF.Foundation.MetaPrinciple`	9	0	1	198	—
`RRF.Foundation.SelfReference`	4	0	8	219	—
`RRF.Foundation.UltimateIsomorphism`	6	0	2	162	—
`RRF.Foundation.VantageCategory`	7	0	10	284	—
`RRF.Hypotheses`	0	0	0	36	—
`RRF.Hypotheses.EightTick`	4	0	10	130	—
`RRF.Hypotheses.PhiLadder`	8	0	4	153	—
`RRF.Hypotheses.TauGate`	0	0	7	141	—
`RRF.Models`	1	0	0	26	—
`RRF.Models.Quadratic`	10	0	6	120	—
`RRF.Models.Trivial`	7	0	7	93	—
`RRF.Physics.ElectronMass.Defs`	1	0	11	93	—
`RRF.Physics.LeptonGenerations`	4	0	0	110	—
`RRF.Physics.LeptonGenerations.Defs`	0	0	8	68	—
`RRF.Physics.LeptonGenerations.Necessity`	15	14	0	352	—
`RRF.Physics.QuarkMasses`	11	1	13	264	—
`RRF.Theorems`	0	0	0	32	—
`RRF.Theorems.MonotoneArgmin`	7	0	1	93	—
`RRF.Theorems.OctaveTransfer`	7	0	1	100	—
`RRF.Theorems.OrderPreservation`	7	0	1	101	—