Materials modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
Materials.AdditiveManufacturingDefectsFromConfigDim
Materials.BCSPairingFromPhiLadder
Materials.BCSSuperconductorFromJCost
Materials.BatteryChemistryFromPhiLadder
Materials.CeramicClassesFromConfigDim
Materials.CompositeFailureModesFromConfigDim
Materials.CorrosionMechanismsFromConfigDim
Materials.CreepRegimesFromConfigDim
Materials.FatigueFractureMechanicsFromJCost
Materials.FatigueThresholdFromJCost
Materials.FractureMechanicsFromJCost
Materials.FractureToughnessFromJCost
Materials.GlassTransitionFromJCost
Materials.HighTcSuperconductorFromPhiLadder
Materials.HydrideSCOptimization
Materials.MagnetismTypesFromConfigDim
Materials.MetamaterialBandGapFromPhiLadder
Materials.PhiLadderPhononResonance
Materials.RoomTSuperconductorCandidate
Materials.SemiconductorDopantTypesFromConfigDim
Materials.SuperconductorVortexFromJCost
Materials.ThermalConductivityRegimesFromPhiLadder
full source mirrored from github.com/jonwashburn/shape-of-logic