Pith. sign in

Verification

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

183 modules · 825 thm/lemma · 22886 lines
module thm lemma def lines papers
Verification.AlphaCorrectionAnalysis 5 0 6 190 -
Verification.AlphaResolutionPass2 13 0 5 207 -
Verification.AnchorNonCircularityCert 8 0 6 250 -
Verification.AnchorsRescaleEqvCert 0 0 0 51 -
Verification.Audit 0 0 0 14 -
Verification.BandsInvariantCert 0 0 0 37 -
Verification.BornRuleDerivationCert 0 0 0 41 -
Verification.BornRuleRouteB 13 0 2 209 -
Verification.BridgeCore 2 0 4 114 -
Verification.CKMCert 0 0 1 50 -
Verification.CPMBridge.Constants.Probability 0 3 1 43 -
Verification.CPMBridge.Exports 1 0 0 31 -
Verification.CPMBridge.Initiality 2 0 2 74 -
Verification.CPT 0 0 0 15 -
Verification.CPT.Core 3 0 3 95 -
Verification.CPT.EpsilonCertification 2 0 1 58 -
Verification.CPT.Exports 18 0 0 242 -
Verification.CPT.ForcedFactorization 10 0 3 296 -
Verification.CPT.Optimality 5 0 1 105 -
Verification.CPT.Pipeline 4 0 1 94 -
Verification.CPT.RankCertification 5 0 2 107 -
Verification.CPT.WindowIdentifiability 5 0 4 91 -
Verification.CalibrationCert 0 0 0 74 -
Verification.CalibrationPolicy 0 0 10 195 -
Verification.CassiniStrongFieldLikelihood 7 0 5 130 -
Verification.CminDerivationCert 0 0 0 71 -
Verification.Concertina 0 0 0 1 -
Verification.ConvexityCert 0 0 0 70 -
Verification.CoshPropertiesCert 0 0 0 74 -
Verification.CoshStrictConvexCert 0 0 0 56 -
Verification.CostUniquenessCert 0 0 0 42 -
Verification.CprojDerivationCert 0 0 0 66 -
Verification.CubeGeometryCert 3 0 0 144 -
Verification.CurvatureSpaceCert 0 0 0 92 -
Verification.DAlembertSymmetryCert 0 0 0 78 -
Verification.DarkEnergyWPlanckLikelihood 7 0 6 138 -
Verification.Dimension 6 0 7 152 -
Verification.DimensionCRT 5 0 1 86 -
Verification.DimensionKepler 1 0 1 77 -
Verification.DimensionLinking 9 0 3 106 -
Verification.DimensionalRigidity 4 0 4 84 -
Verification.EHTM87StrongFieldLikelihood 10 0 8 171 -
Verification.EMAlphaCert 0 0 0 82 -
Verification.EPTAPTALikelihood 8 0 7 154 -
Verification.EulerLagrangeCert 0 0 0 59 -
Verification.Exclusivity.DimensionlessForcing 3 0 2 100 -
Verification.Exclusivity.Framework 3 1 7 309 -
Verification.Exclusivity.HierarchyTheorem 2 0 0 65 -
Verification.Exclusivity.NontrivialityShim 0 0 0 17 -
Verification.Exclusivity.Observables 4 0 11 272 -
Verification.Exclusivity.ParameterSurface 4 0 4 146 -
Verification.Exclusivity.PredictionMap 6 0 6 139 -
Verification.Exclusivity.RCLDerivation 5 0 1 140 -
Verification.ExclusivityCert 0 0 0 93 -
Verification.Exports 1 0 0 12 -
Verification.FalsifierLikelihoodRegister 4 0 5 133 -
Verification.FalsifierRegisterDatasets 22 0 13 388 -
Verification.FibSubstCert 0 0 0 82 -
Verification.GWTC3PosteriorManifest 10 0 9 167 -
Verification.GWTC3RingdownDS1Mode10MDampingFamily 10 0 16 161 -
Verification.GWTC3RingdownFamilyComparison 9 0 8 149 -
Verification.GWTC3RingdownFamilyGuard 13 0 8 172 -
Verification.GWTC3RingdownFilenameTaxonomy 11 0 13 142 -
Verification.GWTC3RingdownGuardedFamilyScripts 9 0 5 139 -
Verification.GWTC3RingdownHDF5SampleSchema 9 0 13 150 -
Verification.GWTC3RingdownHDF5SampleSummary 11 0 18 152 -
Verification.GWTC3RingdownKerr2200MDampingFamily 11 0 16 178 -
Verification.GWTC3RingdownKerr22010MDampingFamily 11 0 16 152 -
Verification.GWTC3RingdownLikelihoodSelector 8 0 8 132 -
Verification.GWTC3RingdownOneMemberDampingStatistic 8 0 14 122 -
Verification.GWTC3RingdownOneMemberRSStatistic 8 0 13 137 -
Verification.GWTC3RingdownSharedRunner 6 0 6 97 -
Verification.GWTC3RingdownStatus 8 0 7 147 -
Verification.GWTC3RingdownZipSchema 9 0 10 138 -
Verification.Gap45DimensionCert 0 0 0 76 -
Verification.GaugeInvarianceCert 0 0 0 18 -
Verification.GenerationTorsionCert 0 0 0 91 -
Verification.GravityS2StrongFieldLikelihood 7 0 6 135 -
Verification.HonestClosureCert 1 0 0 147 -
Verification.HubbleTensionCert 0 0 0 112 -
Verification.ILGAPrioriPredictionCert 7 7 4 430 -
Verification.ILGCoercivityCert 2 0 0 108 -
Verification.Item8ClosureTarget 25 0 71 1069 -
Verification.JcostAxiomsCert 0 0 0 74 -
Verification.JcostConvexityCert 0 0 0 54 -
Verification.JcostCoshFormCert 0 0 0 68 -
Verification.JcostCoshIdentityCert 0 0 0 61 -
Verification.JcostMinimumCert 0 0 0 65 -
Verification.JcostNonnegCert 0 0 0 51 -
Verification.JcostSatisfiesJensenCert 0 0 1 92 -
Verification.JcostStrictCert 0 0 0 58 -
Verification.JcostStrictConvexCert 0 0 0 54 -
Verification.JcostStrictPosCert 0 0 0 51 -
Verification.JcostSymmetryCert 0 0 0 53 -
Verification.JlogAMGMCert 0 0 0 67 -
Verification.JlogCoshCert 0 0 0 58 -
Verification.JlogDerivCert 0 0 0 56 -
Verification.JlogNonnegCert 0 0 0 54 -
Verification.JlogStrictConvexCert 0 0 0 55 -
Verification.JlogZeroCert 0 0 0 56 -
Verification.KernelMatchCert 0 0 0 26 -
Verification.KnetDerivationCert 0 0 0 63 -
Verification.Knobs 0 0 1 21 -
Verification.KnobsCount 3 0 2 58 -
Verification.LeastActionCert 0 0 1 106 -
Verification.LedgerHum 5 1 16 321 -
Verification.LedgerUniquenessCert 0 0 0 72 -
Verification.LeptonCoefficientPerturbation 9 2 0 151 -
Verification.MassComparison 12 0 30 397 -
Verification.MassLawCert 0 0 0 35 -
Verification.Measurement.DataProvenance 0 0 8 268 -
Verification.MeasurementBridgeCert 0 0 0 43 -
Verification.MetricCurvatureCert 0 0 0 20 -
Verification.MetricFromUnitsCert 0 3 4 93 -
Verification.NANOGravPTALikelihood 8 0 7 152 -
Verification.Necessity.ConservationNecessity 8 4 7 287 -
Verification.Necessity.FibSubst 0 13 6 133 -
Verification.Necessity.PhiNecessity 2 3 1 121 -
Verification.Necessity.RecognitionNecessity 16 2 3 368 -
Verification.NeutrinoBaselineChoiceSet 27 0 15 280 -
Verification.NeutrinoReferenceIndexCheck 1 0 0 37 -
Verification.NyquistObstructionCert 2 0 0 105 -
Verification.ODECoshUniqueCert 0 0 0 94 -
Verification.ODEFoundationCert 0 0 0 83 -
Verification.OmegaLambdaPlanckLikelihood 7 0 5 133 -
Verification.OneLtPhiCert 0 0 0 76 -
Verification.PDGComparison 8 0 20 205 -
Verification.PhiAlternativesFailCert 0 0 0 53 -
Verification.PhiBoundsCert 0 0 0 58 -
Verification.PhiDecimalBoundsCert 0 0 0 52 -
Verification.PhiIrrationalityCert 0 0 0 48 -
Verification.PhiNeZeroCert 0 0 0 75 -
Verification.PhiNonDegenerateCert 0 0 0 52 -
Verification.PhiPinnedCert 0 0 0 28 -
Verification.PhiPositivityCert 0 0 0 55 -
Verification.PhiPowerBoundsCert 0 0 0 62 -
Verification.PhiSelfSimilarityCert 0 0 0 56 -
Verification.PhiSquaredCert 0 0 0 51 -
Verification.Preregistered.AlphaInv.Measurement_CODATA2022 0 0 1 24 -
Verification.Preregistered.AlphaInv.Prediction 2 0 1 36 -
Verification.Preregistered.AlphaInv.Test 1 0 0 26 -
Verification.Preregistered.AlphaS.Measurement_PDG2022 0 0 1 24 -
Verification.Preregistered.AlphaS.Prediction 1 0 1 29 -
Verification.Preregistered.AlphaS.Test 1 0 0 32 -
Verification.Preregistered.Core 0 0 2 43 -
Verification.Preregistered.Hubble.Measurement_2022 0 0 3 27 -
Verification.Preregistered.Hubble.Prediction 0 0 2 31 -
Verification.Preregistered.Hubble.Test 3 0 0 87 -
Verification.ProbabilityNormalizationCert 1 4 1 106 -
Verification.QuarkCoordinateUnification 4 0 5 119 -
Verification.QuarkForwardPipeline 18 0 9 292 -
Verification.QuarkSectorAudit 5 0 3 173 -
Verification.RGTransportPolicyIdentity 3 0 2 62 -
Verification.ReciprocalSymmetryEvenCert 0 0 0 67 -
Verification.RecognitionClosureNonVacuityCert 0 0 0 46 -
Verification.RecognitionStabilityAudit 0 0 0 23 -
Verification.RecognitionStabilityAudit.BackEnd 3 0 1 117 -
Verification.RecognitionStabilityAudit.Cayley 5 1 3 135 -
Verification.RecognitionStabilityAudit.Core 1 0 3 120 -
Verification.RecognitionStabilityAudit.FrontEnd 2 0 3 165 -
Verification.RecognitionStabilityAudit.RL 29 0 2 329 -
Verification.RecognitionStabilityAudit.RL.Attr 0 0 0 68 -
Verification.RecognitionStabilityAudit.RStoRL 7 0 34 554 -
Verification.Rendered 0 0 3 42 -
Verification.T5.ConstraintForcing 10 0 6 261 -
Verification.T5.LedgerCost 4 7 3 406 -
Verification.T5UniqueCert 1 0 0 51 -
Verification.T6T8SpineAudit 10 0 0 144 -
Verification.Tier8Cert 0 0 0 57 -
Verification.Track6FalsifierSensitivity 9 0 7 191 -
Verification.TwoOutcomeBornCert 2 2 4 104 -
Verification.UniqueCalibrationCert 0 0 0 36 -
Verification.UnitNormalizationZeroCert 0 0 0 61 -
Verification.UnitsFromAnchorsRescaleCert 0 1 2 97 -
Verification.UnitsRescaledLawsCert 0 0 0 57 -
Verification.VariationalFoundationCert 1 0 1 33 -
Verification.WallpaperClassificationBridge 6 0 5 185 -
Verification.WallpaperEndogenousBridge 10 0 3 113 -
Verification.WallpaperSufficiencyMassPath 5 0 0 69 -
Verification.YardstickAssignmentChoiceSet 59 0 19 1007 -
Verification.YardstickAssignmentPrinciple 21 0 1 255 -
Verification.ZMapConstraintPass2 3 0 1 72 -
Verification.ZMapTopologicalDerivation 33 0 19 512 -

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