OAI/NumberTheory/DirichletL/RowCompletion/BranchDecoding.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CanonicalRowCompletion.initialOrbit_reflection_inputs line 84
  2. lemma OAI.CanonicalRowCompletion.canonicalLabel_squarefree line 89
  3. lemma OAI.CanonicalRowCompletion.canonicalLabel_generator_ne_zero line 92
  4. lemma OAI.CanonicalRowCompletion.unitRowFamily_actual line 96
  5. theorem OAI.CanonicalRowCompletion.fixedShellModels_of_actual_fiber_identity line 102
  6. theorem OAI.CanonicalRowCompletion.finite_selected_branch_collection line 140
  7. theorem OAI.CompletedGauss.FreeReflection.fixedRayFiberFromRows_value line 192
  8. theorem OAI.CanonicalRowCompletion.ActualFiber.reflectedFiber_value line 220
  9. theorem OAI.CanonicalRowCompletion.ActualFiber.sourceStratumValue_eq_compressed line 246
  10. lemma OAI.CanonicalRowCompletion.ActualFiber.one_le_residualScale line 328
  11. lemma OAI.CanonicalRowCompletion.ActualFiber.residual_shell line 337
  12. def OAI.CanonicalRowCompletion.ActualFiber.sourceShapeFactor line 362
  13. def OAI.CanonicalRowCompletion.ActualFiber.sourceFixedCoefficient line 371
  14. def OAI.CanonicalRowCompletion.ActualFiber.compressedSourceTotal line 377
  15. theorem OAI.CanonicalRowCompletion.ActualFiber.completedT_eq_compressedSourceTotal line 386
  16. lemma OAI.CompletedGauss.residualLabelVia_nonresidual_equiv line 426
  17. lemma OAI.CanonicalRowCompletion.ActualFiber.activeModelPrimeEquiv_labels line 454
  18. lemma OAI.CanonicalRowCompletion.ActualFiber.reflectionSixLabel_encode_at line 468
  19. lemma OAI.CompletedGauss.FreeReflection.supportActivePoolEquiv_divisor line 486
  20. theorem OAI.CanonicalRowCompletion.ActualFiber.reflectedFiber_decoded_branch_exact line 511
  21. theorem OAI.CanonicalRowCompletion.ActualFiber.reflectedFiber_encoded_branch_exact line 594