pith. machine review for the scientific record. sign in

Foundation

From one distinction to a forced arithmetic. The core derivation chain: existence, distinction, recognition lattice, φ, dimension, time, universal forcing.

223 modules · 1765 thm/lemma · 39385 lines
module thm lemma def lines papers
Foundation.AbsoluteFloorClosure 6 0 0 83 1080
Foundation.AlexanderDuality 6 0 2 183 1616
Foundation.AlexanderDualityProof 6 0 2 105 4
Foundation.AlphaCoordinateFixation 6 7 2 257 519
Foundation.AlphaDerivationExplicit 2 0 5 66 59
Foundation.ArithmeticFromLogic 58 0 11 720 1214
Foundation.ArithmeticOf 4 0 13 258 4
Foundation.ArrowOfTime 8 0 3 104 138
Foundation.Atomicity 4 11 8 444 60
Foundation.AxiomDischargePlan 7 0 0 389 5
Foundation.BlackBodyRadiationDeep 4 0 1 62 21
Foundation.BranchSelection 11 0 5 221 377
Foundation.Breath1024 0 0 7 61 43
Foundation.CKMHierarchyFromPhiLadder 9 0 10 281
Foundation.CKMLambdaFromPhiLadder 4 0 3 80 5
Foundation.CategoricalLogicRealization 1 0 4 110
Foundation.CausalPropagationOrdering 11 0 3 199
Foundation.ClosedObservableFramework 5 0 1 153
Foundation.CoherenceExponentUniqueness 9 0 6 94
Foundation.ComplexFromLogic 16 0 5 148
Foundation.ConstantDerivations 11 0 9 319 16
Foundation.CostAxioms 12 1 2 372 1
Foundation.CostFirstExistence 3 0 2 108
Foundation.CostFromDistinction 19 0 1 419
Foundation.CoupledRecognitionCores 31 9 18 627
Foundation.DAlembert.AnalyticBridge 21 1 2 807
Foundation.DAlembert.Counterexamples 1 6 4 130
Foundation.DAlembert.CurvatureGate 11 0 9 273
Foundation.DAlembert.DegreeExclusion 1 7 0 155
Foundation.DAlembert.EntanglementGate 12 0 5 242
Foundation.DAlembert.FactorizationForcing 2 0 0 80
Foundation.DAlembert.FourthGate 10 0 2 348
Foundation.DAlembert.FullUnconditional 14 0 3 498
Foundation.DAlembert.Inevitability 8 0 3 516 181
Foundation.DAlembert.LedgerFactorization 5 0 2 164
Foundation.DAlembert.NecessityGates 2 1 1 77
Foundation.DAlembert.Proof 5 0 1 253
Foundation.DAlembert.RightAffineFromFactorization 6 0 0 260
Foundation.DAlembert.Stability 8 4 10 370
Foundation.DAlembert.TriangulatedProof 14 0 1 266 1
Foundation.DAlembert.Ultimate 5 0 3 164
Foundation.DAlembert.Unconditional 7 0 0 230
Foundation.DAlembert.WLOGAlphaOne 8 4 2 145 1
Foundation.Determinism 4 0 1 141
Foundation.DimensionForcing 32 0 8 470 458
Foundation.DimensionalConstraints.CostLayer 1 0 0 74
Foundation.DiracEquationFromJCost 4 0 2 73
Foundation.DiscreteLogicRealization 4 0 4 85
Foundation.DiscretenessForcing 16 0 3 539 37
Foundation.DistinguishabilityFromSpecifiability 4 0 2 103
Foundation.DomainBootstrap 2 0 6 176
Foundation.EightTick 7 0 6 142 10
Foundation.ExclusivityProof 3 0 0 109
Foundation.ExistenceUniquenessFromCost 4 0 1 77
Foundation.FreudenthalTriangulationCert 7 0 9 78
Foundation.Gap45Degeneracy 8 0 1 67
Foundation.GaugeFromCube 25 0 16 450 1
Foundation.GaugeGroupCube 5 0 5 66
Foundation.GeneralizedDAlembert 25 0 10 699 6
Foundation.GeneralizedDAlembert.SecondDerivative 2 0 0 44
Foundation.GeneralizedDAlembert.SmoothnessTop 1 0 0 28
Foundation.GlobalCoIdentityConstraint 10 0 3 324
Foundation.GodelDissolution 9 0 6 296
Foundation.GrowthBounds 6 1 0 161
Foundation.Hamiltonian 2 0 9 125 4
Foundation.HamiltonianEmergence 5 0 5 166 1
Foundation.HierarchyDissolution 4 0 0 65
Foundation.HierarchyDynamics 9 0 1 268 2
Foundation.HierarchyEmergence 3 0 1 133 140
Foundation.HierarchyForcing 8 0 2 155 9
Foundation.HierarchyMinimality 2 0 0 39
Foundation.HierarchyRealization 6 0 1 187
Foundation.HierarchyRealizationFromScale 4 0 1 110
Foundation.HierarchyRealizationObstruction 9 0 3 126
Foundation.Inequalities 12 0 0 128 1
Foundation.InevitabilityEquivalence 7 0 6 240
Foundation.InevitabilityStructure 3 0 19 321 10
Foundation.InitialCondition 8 0 3 166
Foundation.IntegersFromLogic 28 0 13 464
Foundation.IntegrationGap 11 0 6 141 1
Foundation.JCostConvexityInLogSpace 9 0 3 100
Foundation.JCostCoshIdentity 5 0 1 68 1
Foundation.JCostGeometry 18 0 5 228 2
Foundation.JCostHessianC7 4 0 3 75
Foundation.LatticeIsotropyBound 4 0 1 48
Foundation.LawOfExistence 16 0 4 203 74
Foundation.LedgerCanonicality 0 0 1 108 36
Foundation.LedgerForcing 17 0 10 355 38
Foundation.LocalityFromLedger 5 0 0 108
Foundation.LogicAsFunctionalEquation 7 0 7 381 116
Foundation.LogicAsFunctionalEquation.AnalyticCounterexample 2 0 2 61
Foundation.LogicAsFunctionalEquation.BooleanRatioBridge 3 0 3 78
Foundation.LogicAsFunctionalEquation.Canonicality 7 0 0 107
Foundation.LogicAsFunctionalEquation.CountOnceComparison 4 0 4 89
Foundation.LogicAsFunctionalEquation.DirectProof 5 0 1 163
Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison 8 0 0 104
Foundation.LogicAsFunctionalEquation.LinearLogicBridge 3 0 2 94
Foundation.LogicAsFunctionalEquation.MainTheorem 5 0 0 64
Foundation.LogicAsFunctionalEquation.NoHiddenState 2 0 0 50
Foundation.LogicAsFunctionalEquation.OperativeDomain 3 0 1 51
Foundation.LogicAsFunctionalEquation.PositiveRatioForcing 4 0 1 64
Foundation.LogicAsFunctionalEquation.QuarticLogCounterexample 4 0 2 85
Foundation.LogicAsFunctionalEquation.RealityStructure 7 0 0 98
Foundation.LogicComplexCompat 5 0 3 96
Foundation.LogicFromCost 10 0 6 343
Foundation.LogicRealTranscendentals 14 0 9 121
Foundation.LogicRealization 5 0 3 183 1
Foundation.MagnitudeOfMismatch 6 0 1 150
Foundation.ModularLogicRealization 7 0 6 119
Foundation.MultiChannelJCost 4 0 2 86
Foundation.MultiplicativeRecognizerL4 7 0 4 234 1
Foundation.NeutralSector 3 0 1 78
Foundation.NoetherTheoremDeep 4 0 3 71
Foundation.NonTrivialityFromDistinguishability 13 0 2 227
Foundation.ObserverForcing 13 0 4 271
Foundation.ObserverFromRecognition 10 0 4 174 1
Foundation.OntologyPredicates 32 0 11 540
Foundation.OperatorCore.CoupledRecognitionCores 0 0 0 32
Foundation.OptionAEmpiricalActionPlan 12 0 4 139
Foundation.OptionAEmpiricalDeliverables 10 0 4 131
Foundation.OptionAEmpiricalPipeline 12 0 4 131
Foundation.OptionAEmpiricalProgram 10 0 4 143
Foundation.OptionAEmpiricalProtocol 15 0 5 159
Foundation.OptionAEmpiricalQueue 24 0 8 205
Foundation.OptionAEmpiricalReadiness 7 0 4 87
Foundation.OptionAEmpiricalSchedule 8 0 2 105
Foundation.OptionAFalsifierRegistry 22 0 6 275
Foundation.OrderedLogicRealization 4 0 3 90
Foundation.OscillatoryDynamicsDeep 5 0 3 80
Foundation.ParticleGenerations 4 0 1 71
Foundation.PathIntegralDeep 4 0 2 73
Foundation.PhiEmergence 17 0 6 228
Foundation.PhiForcing 18 0 4 258 89
Foundation.PhiForcingDerived 7 2 3 266 1
Foundation.PhysicsLogicRealization 3 0 5 101
Foundation.PinchAlgebra 4 0 0 74
Foundation.PolynomialityFromLogic 2 0 2 188
Foundation.PostingExtensivity 10 0 1 200
Foundation.PreLogicalCost 2 0 5 73
Foundation.PreTemporalForcingOrder 21 0 7 194
Foundation.PrimitiveDistinction 10 0 5 333 2
Foundation.QRFT.FermionKineticCert 4 0 3 75
Foundation.QRFT.GaugeTreeAmplitudesCert 6 0 2 87
Foundation.QRFT.HiggsPotentialFromRecognitionVacuum 4 0 2 80
Foundation.QRFT.SMLagrangianSkeleton 7 0 3 106
Foundation.QRFT.YukawaCouplingFromJCost 3 0 2 70
Foundation.QuantumLedger 12 0 8 232
Foundation.QuarkColors 5 0 1 66
Foundation.RHatFixedPoint 6 0 0 97
Foundation.RHatFromJCostGradient 3 0 2 92
Foundation.RSCoupledAxis 4 0 3 88
Foundation.RationalsFromLogic 25 0 13 437
Foundation.RealityFromDistinction 3 0 0 157 2976
Foundation.RealityTerminalCategory 4 0 4 104 1
Foundation.RealsFromLogic 28 0 5 225
Foundation.RecognitionForcing 11 0 5 207
Foundation.RecognitionLattice3 4 0 3 36
Foundation.RecognitionLatticeFromRecognizer 10 0 11 231 2
Foundation.RecognizerInducesLogic 2 0 1 259 1
Foundation.RecoveredTowerAxiomAudit 0 0 0 131
Foundation.SMGaugeAlgebra 5 0 5 77
Foundation.SelfBootstrapDistinguishability 7 0 0 88 3
Foundation.SimplicialFoundationSummary 0 0 1 21
Foundation.SimplicialLedger 3 0 6 107 7
Foundation.SimplicialLedger.ContinuumBridge 10 0 10 327
Foundation.SimplicialLedger.ContinuumTheorem 5 0 0 186
Foundation.SimplicialLedger.CubicDeficitDischarge 12 0 6 325
Foundation.SimplicialLedger.CubicSimplicialEquivalence 8 0 1 274
Foundation.SimplicialLedger.EdgeLengthFromPsi 9 0 4 334
Foundation.SimplicialLedger.InteriorFlat 4 0 7 254
Foundation.SimplicialLedger.LorentzEmergence 6 0 4 256
Foundation.SimplicialLedger.NonlinearBridge 13 0 4 381
Foundation.SimplicialLedger.SimplicialDeficitDischarge 6 0 1 199
Foundation.SpecialRelativityDeep 4 0 2 82
Foundation.SpectralEmergence 40 0 11 575
Foundation.SpinStatistics 9 0 3 132
Foundation.StillnessGenerative 33 0 5 477
Foundation.SubstitutivityForcing 3 0 0 53
Foundation.ThermodynamicLawsFromJCost 5 0 2 81
Foundation.ThreeSubstrateValidationCert 7 0 4 78
Foundation.TimeAsOrbit 12 0 8 199
Foundation.TimeEmergence 7 0 7 182
Foundation.TopologicalConservation 16 0 8 271
Foundation.TopologicalVeto 8 0 0 125
Foundation.UniversalForcing 1 0 5 68
Foundation.UniversalForcing.AdmissibleClass 2 0 5 141
Foundation.UniversalForcing.AxiomAudit 0 0 0 96
Foundation.UniversalForcing.BiologyRealization 2 0 4 77
Foundation.UniversalForcing.CategoricalRealization 0 0 2 31
Foundation.UniversalForcing.ContinuousRealization 0 0 2 35
Foundation.UniversalForcing.DiscreteRealization 0 0 2 31
Foundation.UniversalForcing.EthicsRealization 2 0 4 79
Foundation.UniversalForcing.Invariance.TwoCases 0 0 1 36
Foundation.UniversalForcing.Invariance.Universal 1 0 2 43
Foundation.UniversalForcing.MetaphysicalRealization 0 0 2 49
Foundation.UniversalForcing.ModularRealization 2 0 4 92
Foundation.UniversalForcing.MusicRealization 2 0 4 78
Foundation.UniversalForcing.NarrativeRealization 2 0 4 78
Foundation.UniversalForcing.NaturalNumberObject 3 0 6 302 2
Foundation.UniversalForcing.OrderRealization 2 0 4 82
Foundation.UniversalForcing.Strict.AxiomAudit 0 0 6 96
Foundation.UniversalForcing.Strict.Biology 2 0 6 69
Foundation.UniversalForcing.Strict.Categorical 2 0 3 60
Foundation.UniversalForcing.Strict.CategoricalMathlib 5 0 1 121
Foundation.UniversalForcing.Strict.DiscreteBoolean 2 0 5 73
Foundation.UniversalForcing.Strict.Ethics 2 0 6 68
Foundation.UniversalForcing.Strict.Invariance 1 0 2 42
Foundation.UniversalForcing.Strict.MathlibNNO 3 0 0 55
Foundation.UniversalForcing.Strict.Metaphysical 0 0 2 52
Foundation.UniversalForcing.Strict.Modular 2 0 3 62
Foundation.UniversalForcing.Strict.Music 2 0 7 70
Foundation.UniversalForcing.Strict.Narrative 2 0 6 67
Foundation.UniversalForcing.Strict.Ordered 2 0 3 55
Foundation.UniversalForcing.Strict.PositiveRatio 0 0 3 65
Foundation.UniversalForcing.Strict.RichDomainCosts 13 0 5 218
Foundation.UniversalForcing.StrictRealization 3 0 5 120
Foundation.UniversalForcingAudit 0 0 0 116
Foundation.UniversalForcingSelfReference 8 0 3 276
Foundation.UniversalInstantiationFromDistinction 8 0 6 207
Foundation.VariationalDynamics 24 0 8 633
Foundation.VoiceForcing 11 0 5 179
Foundation.WightmanAxiomsStatus 4 0 1 57
Foundation.WindingCharges 24 0 9 454

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