OAI/Computability/UniqueGames/PCP/
4503 declarations, 0 contain sorry, 0 declared as axioms; 104 files
Files
- Addresses.lean 51 declarations
- AlphabetGraphLemmas.lean 124 declarations
- AlphabetReductionLemmas.lean 70 declarations
- AlphabetRetractionLemmas.lean 86 declarations
- AlphabetTableBoundsLemmas.lean 94 declarations
- AmplificationIteration.lean 11 declarations
- AssignmentTester.lean 68 declarations
- BinaryParityReduction.lean 12 declarations
- Body.lean 22 declarations
- CayleySampling.lean 12 declarations
- CayleyTailCount.lean 24 declarations
- ClauseVerifierLemmas.lean 111 declarations
- CleanupLemmas.lean 70 declarations
- Clone100.lean 26 declarations
- Clone100Encoding.lean 15 declarations
- Clone100Triples.lean 11 declarations
- CloudRoundingLemmas.lean 62 declarations
- CodeComposition.lean 25 declarations
- CompareLoop.lean 20 declarations
- DriverLemmas.lean 27 declarations
- EmitRows.lean 27 declarations
- Emitter.lean 40 declarations
- ExpanderRowControlLemmas.lean 48 declarations
- ExpanderTableEnumeration.lean 31 declarations
- ExpanderTables.lean 28 declarations
- ExpandersLemmas.lean 60 declarations
- FinalBooleanVerifier.lean 35 declarations
- FinalConstantsLemmas.lean 44 declarations
- FinalTableFormula.lean 12 declarations
- FoldedEquationLemmas.lean 65 declarations
- FourierResponseLemmas.lean 25 declarations
- GenericGraphTables.lean 67 declarations
- GraphTables.lean 67 declarations
- HonestTestLemmas.lean 62 declarations
- InitialGraphLemmas.lean 126 declarations
- Initialization.lean 15 declarations
- InputLemmas.lean 83 declarations
- LoopInitializationLemmas.lean 32 declarations
- LoopState.lean 24 declarations
- MachineRawInitialTable.lean 6 declarations
- NameCompaction.lean 38 declarations
- OverlayLemmas.lean 96 declarations
- PortTableEncoding.lean 12 declarations
- PortTableLookup.lean 10 declarations
- PoweringLabelsLemmas.lean 128 declarations
- PoweringOpinionTables.lean 24 declarations
- PoweringOpinionsLemmas.lean 43 declarations
- PoweringPortReindexLemmas.lean 53 declarations
- PoweringTableLayout.lean 19 declarations
- PoweringTableSemanticsLemmas.lean 59 declarations
- PoweringTablesLemmas.lean 83 declarations
- Preprocessing.lean 33 declarations
- PreprocessingInternalRows.lean 25 declarations
- PreprocessingLazyWords.lean 22 declarations
- PreprocessingOverlayTables.lean 24 declarations
- PreprocessingOverlayWords.lean 21 declarations
- PreprocessingPaddingOffsets.lean 8 declarations
- PreprocessingPaddingTables.lean 35 declarations
- PreprocessingPaddingWords.lean 16 declarations
- PreprocessingRegularLoopWordsLemmas.lean 44 declarations
- PreprocessingRegularSoundness.lean 13 declarations
- PreprocessingRegularTablesLemmas.lean 50 declarations
- PreprocessingRegularWords.lean 25 declarations
- PreprocessingTableSpectral.lean 8 declarations
- PreprocessingTablesLemmas.lean 56 declarations
- QueriesLemmas.lean 40 declarations
- RawInitialMachineBody.lean 4 declarations
- RawInitialMachineCleanup.lean 4 declarations
- RawInitialMachineFinish.lean 16 declarations
- RawInitialMachineLoop.lean 5 declarations
- RawInitialMachineLoopData.lean 13 declarations
- RawInitialMachinePhases.lean 9 declarations
- RawInitialMachineReadClause.lean 10 declarations
- RawInitialMachineRows.lean 19 declarations
- RawInitialMachineStart.lean 14 declarations
- RawInitialTablesLemmas.lean 89 declarations
- RoundSize.lean 21 declarations
- RuntimeModel.lean 32 declarations
- Setup.lean 14 declarations
- SourceAddressArithmeticLemmas.lean 43 declarations
- SourceContextClear.lean 32 declarations
- SourceContextLoad.lean 46 declarations
- SourceDescriptorEmissionLemmas.lean 89 declarations
- SourceFieldArrayLemmas.lean 74 declarations
- SourceGapLemmas.lean 106 declarations
- SourceHeaderAccumulate.lean 12 declarations
- SourceHeaderCounts.lean 85 declarations
- SourceHonestLemmas.lean 82 declarations
- SourceIncidence.lean 13 declarations
- SourceLoopInitLemmas.lean 61 declarations
- SourceMachine.lean 27 declarations
- SourceNoiseParameterLemmas.lean 91 declarations
- SourceOccurrences.lean 74 declarations
- SourceQueryLoopLemmas.lean 71 declarations
- SourceQueryOrderLemmas.lean 141 declarations
- SourceRuntimeSpace.lean 13 declarations
- SourceSignaturePrepareLemmas.lean 86 declarations
- SourceTupleBody.lean 59 declarations
- SourceTupleBound.lean 25 declarations
- Table.lean 26 declarations
- TableGapReductionLemmas.lean 23 declarations
- TableIteration.lean 26 declarations
- VertexPadding.lean 32 declarations
- ZigzagGraphsLemmas.lean 93 declarations