OAI/Combinatorics/ParityLifts/Witnesses.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.WeightedWitness.coordinate_neighbors line 17
2. lemma OAI.ParityWL.WeightedWitness.tag_sum line 30
3. theorem OAI.ParityWL.WeightedWitness.no_tags line 66

   Source documentation

   A genuine dual certificate makes the source-indexed tag system inconsistent.

   theorem WeightedWitness.no_tags (w : WeightedWitness T F a b)
       (z : (x : W) → T.neighborSet (a x) → Bit)
       (hz : ∀ x, ∑ u, z x u = b (a x))
       (he : ∀ x y (h : F.Adj x y),
         z x ⟨a y, a.map_adj h⟩ = z y ⟨a x, a.map_adj h.symm⟩) : False := by
   …

   Mentions: OAI.ParityWL.WeightedWitness, OAI.ParityWL.Bit

4. theorem OAI.ParityWL.weightedWitness_inconsistent line 90
5. theorem OAI.ParityWL.homCount_lift_strict_iff_witness line 96
6. lemma OAI.ParityWL.BaseArc.type_adj line 114
7. lemma OAI.ParityWL.BaseArc.adj line 122
8. def OAI.ParityWL.choiceMap line 128
9. lemma OAI.ParityWL.choiceMap_type line 157
10. theorem OAI.ParityWL.successful_template_count_gap line 163

    Source documentation

    The explicit noncancelling source is the uncolored template itself.

    theorem successful_template_count_gap (ht : 0 < t) (hs : C.Successful) :
        homCount (template t) (starLift C) < homCount (template t) (zeroLift C) := by
    …

    Mentions: OAI.ParityWL.homCount, OAI.ParityWL.template, OAI.ParityWL.starLift, OAI.ParityWL.zeroLift