OAI/NumberTheory/OrdinaryCorrelations/HighTrace/RootCode.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.rootCode line 23
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.rootCode_decode line 30
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.farRootBudget line 38
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.farTestSize line 39
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.farTestSize_nonneg line 40
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.selectedIndex line 49
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.template line 51
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.root_relabel line 54
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.selected_relabel line 55
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.expression_relabel line 57
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.formed line 67
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.root_bound line 71
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.admissible line 77
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.template_admissible line 95