OAI/Combinatorics/ParityLifts/LiftCounts.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.liftProjection line 14
  2. abbrev OAI.ParityWL.Variables line 29
  3. instance OAI.ParityWL.variablesFintype line 31
  4. def OAI.ParityWL.LiftEquations line 36
  5. def OAI.ParityWL.Solutions line 42
  6. instance OAI.ParityWL.solutionsFintype line 45
  7. def OAI.ParityWL.zeroSolution line 51
  8. def OAI.ParityWL.solutionHom line 54
  9. def OAI.ParityWL.homSolutionsEquiv line 61
  10. def OAI.ParityWL.homogeneousTranslate line 75
  11. lemma OAI.ParityWL.solutions_card_eq_of_nonempty line 103
  12. lemma OAI.ParityWL.solutions_card_le line 111
  13. lemma OAI.ParityWL.solutions_card_eq_iff line 121
  14. def OAI.ParityWL.homCount line 134
  15. lemma OAI.ParityWL.homCount_lift line 138
  16. theorem OAI.ParityWL.homCount_lift_le line 146

    Source documentation

    Noncancellation for every uncolored homomorphism, not just typed witnesses.

    theorem homCount_lift_le (b : A → Bit) :
    homCount F (liftGraph T G τ b) ≤ homCount F (liftGraph T G τ (fun _ => 0)) := by
…

    Mentions: OAI.ParityWL.Bit, OAI.ParityWL.homCount, OAI.ParityWL.liftGraph

  17. lemma OAI.ParityWL.homCount_lift_eq_iff line 153
  18. theorem OAI.ParityWL.homCount_lift_strict_iff line 162

    Source documentation

    A strict uncolored count gap comes from an inconsistent projected system.

    theorem homCount_lift_strict_iff (b : A → Bit) :
    homCount F (liftGraph T G τ b) < homCount F (liftGraph T G τ (fun _ => 0)) ↔
      ∃ φ : F →g G, ¬ Nonempty (Solutions T G F τ φ b) := by
…

    Mentions: OAI.ParityWL.Bit, OAI.ParityWL.homCount, OAI.ParityWL.liftGraph, OAI.ParityWL.Solutions

  19. abbrev OAI.ParityWL.EquationRow line 178
  20. def OAI.ParityWL.constraintMap line 180
  21. def OAI.ParityWL.constraintRHS line 200
  22. lemma OAI.ParityWL.liftEquations_iff line 205
  23. lemma OAI.ParityWL.bit_zero_or_one line 231
  24. theorem OAI.ParityWL.binary_alternative line 236

    Source documentation

    Linear-algebra separation without a rank assumption.

    theorem binary_alternative (L : E →ₗ[Bit] H) (c : H) :
    (¬ ∃ z, L z = c) ↔
      ∃ f : H →ₗ[Bit] Bit, (∀ z, f (L z) = 0) ∧ f c = 1 := by
…

    Mentions: OAI.ParityWL.Bit