OAI/Computability/DegreeRigidity/OrdinalCodes/
676 declarations, 0 contain sorry, 0 declared as axioms; 105 files
Files
- CanonicalAdditionSyntax.lean 8 declarations
- CanonicalOmegaSyntax.lean 5 declarations
- CanonicalRealsSyntax.lean 3 declarations
- CodeBranchCertificates.lean 6 declarations
- CodeBranchLevels.lean 2 declarations
- CodeOperationCertificates.lean 3 declarations
- IndexJoin.lean 8 declarations
- IndexMatrix.lean 10 declarations
- IndexPresentation.lean 11 declarations
- IndexTuples.lean 11 declarations
- IndexedOrder.lean 8 declarations
- LargestOrdinalSyntax.lean 8 declarations
- LevelInlinedDefinition.lean 3 declarations
- LevelOrdinalHeight.lean 4 declarations
- LevelSubsetDefinition.lean 2 declarations
- LimitOmegaCertificates.lean 2 declarations
- LimitOmegaGraphSyntax.lean 4 declarations
- NaturalAdditionTrace.lean 8 declarations
- NaturalDefinitions.lean 12 declarations
- NaturalIterationFormula.lean 5 declarations
- NaturalIterationTrace.lean 6 declarations
- NaturalMultiplicationFormula.lean 3 declarations
- NaturalPairingFormula.lean 5 declarations
- NaturalPrimitiveRecursion.lean 5 declarations
- NaturalProjectionFormula.lean 2 declarations
- NaturalRealRelation.lean 7 declarations
- NaturalTermFormula.lean 6 declarations
- NumericBinding.lean 4 declarations
- NumericDefSystem.lean 9 declarations
- NumericDomain.lean 10 declarations
- NumericFamilySupport.lean 5 declarations
- NumericHierarchy.lean 6 declarations
- NumericParameters.lean 23 declarations
- NumericStage.lean 4 declarations
- NumericTruth.lean 5 declarations
- NumericalAutomorphism.lean 3 declarations
- NumericalCohenProductSets.lean 3 declarations
- NumericalCohenSets.lean 6 declarations
- NumericalExtension.lean 3 declarations
- NumericalIdeal.lean 7 declarations
- OmegaCertificateCollection.lean 2 declarations
- OmegaGraphRestriction.lean 4 declarations
- OmegaGraphSyntax.lean 4 declarations
- OmegaModelArithmetic.lean 6 declarations
- OmegaModelAxiomTransport.lean 6 declarations
- OmegaModelCollapse.lean 15 declarations
- OmegaModelCore.lean 14 declarations
- OmegaModelCoreClosure.lean 12 declarations
- OmegaModelSyntax.lean 6 declarations
- OmegaPowerCertificates.lean 9 declarations
- OmegaPowerDefinability.lean 4 declarations
- OmegaPowerGraph.lean 5 declarations
- OmegaPowerStage.lean 7 declarations
- OmegaPowerSyntax.lean 9 declarations
- OmegaRecursionSchemas.lean 5 declarations
- OmegaStageSyntax.lean 7 declarations
- OrdinalCodeBranch.lean 8 declarations
- OrdinalCodeDomains.lean 5 declarations
- OrdinalCodeOperations.lean 11 declarations
- OrdinalConstruction.lean 2 declarations
- OrdinalCut.lean 13 declarations
- OrdinalDecoderDomains.lean 5 declarations
- OrdinalEntryBinding.lean 9 declarations
- OrdinalEntryDecoder.lean 3 declarations
- OrdinalInputSyntax.lean 8 declarations
- OrdinalOrderPresentation.lean 3 declarations
- OrdinalOrderType.lean 11 declarations
- OrdinalOrderTypeLevels.lean 2 declarations
- OrdinalOrderTypeSyntax.lean 11 declarations
- OrdinalPaddingSyntax.lean 4 declarations
- OrdinalPairCode.lean 10 declarations
- OrdinalPairSyntax.lean 6 declarations
- OrdinalProductClosure.lean 5 declarations
- OrdinalProductPresentation.lean 10 declarations
- OrdinalProductReplacement.lean 6 declarations
- OrdinalProductSets.lean 10 declarations
- OrdinalProductSyntax.lean 12 declarations
- OrdinalSumClosure.lean 7 declarations
- OrdinalSumLevels.lean 2 declarations
- OrdinalSumPresentation.lean 15 declarations
- OrdinalSumSets.lean 19 declarations
- OrdinalSumSyntax.lean 14 declarations
- OrdinalVectorRecovery.lean 2 declarations
- OrdinalVectorSyntax.lean 5 declarations
- PaddedOmegaBoundary.lean 3 declarations
- ProductCertificateCollection.lean 3 declarations
- RankDefinability.lean 3 declarations
- RankGraphConstruction.lean 7 declarations
- RankOrdinal.lean 4 declarations
- RankRecursion.lean 12 declarations
- Recurrence.lean 14 declarations
- SelectorOrdinalEnumeration.lean 1 declarations
- SuccessorOmegaCertificates.lean 1 declarations
- SumCertificateLevels.lean 1 declarations
- SumCertificates.lean 4 declarations
- SumComparison.lean 8 declarations
- TrimmedBoundaryCertificates.lean 4 declarations
- TrimmedOrderDomains.lean 6 declarations
- TrimmedPaddedSum.lean 1 declarations
- TrimmedPresentation.lean 2 declarations
- TrimmedProductGraph.lean 4 declarations
- TrimmedSumDomains.lean 5 declarations
- TrimmedSumGraph.lean 4 declarations
- VectorCodeCertificates.lean 8 declarations
- VectorCodeLevels.lean 3 declarations