Information

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

32 modules · 226 thm/lemma · 4780 lines

module	thm	lemma	def	lines	papers
`Information`	0	0	2	49	4
`Information.ChurchTuring`	7	0	4	252	—
`Information.ChurchTuringPhysicsStructure`	14	0	6	190	—
`Information.Compression`	5	2	15	252	—
`Information.CompressionPrior`	1	0	2	28	—
`Information.ComputationLimitsStructure`	17	0	9	207	—
`Information.EMLFromRecognition`	9	0	6	133	—
`Information.ErrorCorrectionBounds`	8	0	8	240	—
`Information.ErrorCorrectionCodesFromJCost`	3	0	2	61	—
`Information.FEPBridgeFromJCost`	9	0	4	151	—
`Information.HelmholtzDecomposition`	2	0	3	49	—
`Information.InformationIsLedger`	22	1	6	298	—
`Information.JCostNecessity`	2	0	0	58	—
`Information.LDPCCodeRateFromPhi`	6	0	3	112	—
`Information.LocalCache`	9	0	7	281	—
`Information.NESSConditionalIndependenceMeasure`	3	0	6	118	—
`Information.NetworkTopologyFromSigma`	3	0	2	61	—
`Information.NoCloning`	12	2	3	240	—
`Information.PhiHierarchyGrowth`	12	0	2	197	—
`Information.PhysicsComplexityStructure`	17	1	5	256	—
`Information.PolarCodeGapFromPhi`	3	0	3	66	—
`Information.QECThresholdFromPhiLadder`	3	0	2	54	—
`Information.QuantumChannelCapacityFromPhi`	3	0	2	90	—
`Information.QuantumErrorCorrection`	1	0	7	256	—
`Information.QuantumErrorCorrectionThreshold`	3	0	2	69	—
`Information.RecognitionBremermann`	7	0	2	77	—
`Information.RecognitionEntropy`	5	0	4	75	—
`Information.ShannonAsJCostLimit`	4	0	4	120	—
`Information.ShannonEntropy`	9	0	8	248	—
`Information.ShannonHighNLimit`	6	0	1	187	—
`Information.SimulationHypothesisStructure`	12	0	5	207	—
`Information.Thermodynamics`	3	0	5	98	—