OAI/Computability/DegreeRigidity/Representation/
515 declarations, 0 contain sorry, 0 declared as axioms; 115 files
Files
- AmbientDegreeActual.lean 3 declarations
- AmbientDegreeBinding.lean 5 declarations
- AmbientDegreeSyntax.lean 7 declarations
- AmbientExtensionBody.lean 3 declarations
- ArithmeticRepresentation.lean 2 declarations
- Assembly.lean 10 declarations
- AutomorphismName.lean 12 declarations
- AutomorphismOutputSentence.lean 4 declarations
- AutomorphismUnion.lean 20 declarations
- BorelGeneric.lean 17 declarations
- Category.lean 5 declarations
- CategoryAvoidance.lean 3 declarations
- CategoryMachine.lean 15 declarations
- CategoryMain.lean 2 declarations
- CategoryReduction.lean 8 declarations
- CommonExtensionProgram.lean 3 declarations
- CommonGenericModels.lean 3 declarations
- CommonIdeal.lean 25 declarations
- CommonIdealBorel.lean 5 declarations
- CommonIdealSearch.lean 10 declarations
- CommonIdealSelection.lean 16 declarations
- CountableGroundGeneric.lean 1 declarations
- CoverageMain.lean 1 declarations
- Endpoints.lean 3 declarations
- FullNativePersistence.lean 4 declarations
- GenericAssembly.lean 1 declarations
- GenericCoding.lean 22 declarations
- GenericCodingBorel.lean 3 declarations
- GenericDescentDefinition.lean 1 declarations
- GenericFactor.lean 11 declarations
- GenericFiberIdeal.lean 4 declarations
- GenericFilterName.lean 12 declarations
- GenericIdentity.lean 10 declarations
- GenericOneRealNames.lean 1 declarations
- GenericPersistenceDescent.lean 3 declarations
- GenericRealColumnRealization.lean 2 declarations
- GenericRepresentation.lean 8 declarations
- GenericSourceTransfer.lean 3 declarations
- GenericTopology.lean 5 declarations
- GenericTotality.lean 4 declarations
- GenericTruth.lean 7 declarations
- GlobalArithmeticGenericProgram.lean 1 declarations
- GlobalJumpRestriction.lean 3 declarations
- GlobalLocality.lean 6 declarations
- GroundArithmeticGeneric.lean 1 declarations
- GroundDegreeCollapse.lean 1 declarations
- GroundDegreePresentation.lean 3 declarations
- GroundGenericRequirements.lean 1 declarations
- GroundInclusion.lean 7 declarations
- GroundIteratedTriple.lean 3 declarations
- GroundPrefixOverwrite.lean 2 declarations
- GroundSeedOrdinalHeight.lean 7 declarations
- HomogeneousDegreeExtension.lean 4 declarations
- IteratedGenericCommonIdeal.lean 2 declarations
- NativeGenericWitness.lean 3 declarations
- NativeModelCompatibility.lean 6 declarations
- NativePersistenceSyntax.lean 7 declarations
- OriginalRealCohenFactorization.lean 2 declarations
- OriginalRealDefinitionTransport.lean 2 declarations
- OriginalRealFullIteration.lean 1 declarations
- OriginalRealGeneratedModel.lean 1 declarations
- OriginalRealQuotientModel.lean 1 declarations
- OriginalRealUniformDefinition.lean 1 declarations
- OriginalRealUniformExtension.lean 1 declarations
- OwnDegreeExtensionMeaning.lean 1 declarations
- OwnProgramValue.lean 5 declarations
- OwnRealsConstruction.lean 6 declarations
- OwnRealsLevelDefinition.lean 3 declarations
- OwnSourceEquation.lean 2 declarations
- OwnStageSourceTheory.lean 2 declarations
- PairGenericSelection.lean 9 declarations
- ParameterCoveringModels.lean 8 declarations
- PrescribedArithmeticGenericProgram.lean 1 declarations
- PrescribedColumnPrefixProgram.lean 1 declarations
- PrescribedCoveringModel.lean 1 declarations
- PrescribedFirstUncountable.lean 1 declarations
- PrescribedGenericRestriction.lean 5 declarations
- PrescribedGroundOracleProgram.lean 1 declarations
- PrescribedModelRestriction.lean 3 declarations
- PrescribedOneRealNames.lean 2 declarations
- PrescribedOracleValue.lean 1 declarations
- PrescribedRealHullExtension.lean 1 declarations
- PrescribedUnrestrictedGroundProgram.lean 1 declarations
- RealCollapseReconstruction.lean 1 declarations
- RealGeneratedModel.lean 6 declarations
- RealGeneratedPart.lean 13 declarations
- RealHullColumnRealization.lean 2 declarations
- RealHullGenericTriple.lean 2 declarations
- RealHullIteration.lean 2 declarations
- RealHullPrescribedTruth.lean 1 declarations
- RealHullQuotient.lean 2 declarations
- Reduction.lean 1 declarations
- RepresentationEndgame.lean 2 declarations
- SameExtensionCommonIdeal.lean 1 declarations
- SameExtensionGenericTriple.lean 2 declarations
- SameExtensionIteration.lean 2 declarations
- SameRealBooleanFilter.lean 3 declarations
- SetAutomorphismReconstruction.lean 5 declarations
- SourceEquationTail.lean 5 declarations
- SourceIdentity.lean 6 declarations
- SourceTAbsolutenessEndpoint.lean 1 declarations
- SourceTArithmeticAbsoluteness.lean 4 declarations
- SourceTCountability.lean 3 declarations
- SourceTDependentChoice.lean 4 declarations
- SourceTGenericExistence.lean 2 declarations
- SourceTGenericPersistence.lean 4 declarations
- SourceTGenericPresentation.lean 1 declarations
- SourceTModelBridge.lean 3 declarations
- SourceTNativeAbsoluteness.lean 2 declarations
- SourceTNativeComparison.lean 5 declarations
- SourceTPersistentDecoding.lean 3 declarations
- SourceTPresentationComparison.lean 9 declarations
- SourceTTreeAbsoluteness.lean 7 declarations
- SourceTWellFounded.lean 4 declarations
- SourceTheory.lean 3 declarations