Mathesis
Dhruv GuptaDhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z
ClaimMTH.C-2026-6019ArgumentMTH.R-2026-6019

The discrete Vorob'ev theorem: a cover's base structure is acyclic exactly when local pairwise consistency always forces a global structure, i.e. every pairwise-consistent family of nonempty local relations on it glues.

DeclHiddenChannelCapacity.acyclic_iff_forall_consistent_glues
∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (𝒞 : Finset (Finset ι)),
  HiddenChannelCapacity.Acyclic 𝒞 ↔
    ∀ (fam : List (HiddenChannelCapacity.LocalStruct ι fun x => ZMod 2)),
      List.map (fun x => x.team) fam = 𝒞.toList →
        HiddenChannelCapacity.Consistent fam → (∀ L ∈ fam, L.rel.Nonempty) → HiddenChannelCapacity.Glues fam
TopicGraphical models
Layout
ThesisStepDefinition
acyclic_iff_forall_consis…theoremglues_of_acyclictheoremrip_iff_ripCovertheoremfamCover_eq_listCovertheoremglues_of_riptheoremprojS_joinFamtheoremteam_subset_famCovertheoremprojS_image_restrict₂theoremmem_joinFamtheoremexists_restrict_eqtheoremimarg_imagetheoremglues_of_permtheoremexists_perm_map_eqtheoremconsistent_of_permtheoremexists_consistent_not_glu…theoremearFree_dichotomytheoremshared_nonempty_of_earFreetheoremisEarOf_of_simplicialtheorembndry_eq_inter_sharedtheoremmem_sharedtheoremdirac_strongtheoremsep_clique_steptheoremno_chord_of_minimaltheoremgetLast_getElemtheoremreachOn_transtheoremreachOn_symmtheoremreachOn_refltheoremreachOn_of_mem_walktheoremreachOn_extendtheoremexists_min_paththeoremexists_connectortheoremerase_separatestheoremreachOn_of_walktheoremisChain_droptheoremisChain_taketheoremhead_getElemtheoremgcast_listtheoremsymm'theoremcapstone_of_dichotomytheoremexists_earFree_core_chaintheoremclean_system_of_uncovered…theoremxorSum_eq_empty_ifftheoremmem_xorSumtheoremerase_union_erasetheoremcovered_of_card_le_twotheoremmem_coverUtheoremclean_system_of_chordless…theoremxorSumL_cyclePairstheoremxorSumL_zipWith_symmDifftheoremxorSumL_permtheorempair_eq_symmDifftheoremgetElem_ne_nexttheoremnodup_cyclePairstheoremcyclePairs_ne_emptytheoremclean_of_chordlessCycletheoremmod_succ_casestheoremgetElem_cyclePairstheoremlength_cyclePairstheoremadj_or_eq_of_cohostedtheoremcapstone_of_coretheoremclean_system_obstructiontheoremaffine_obstructiontheoremnot_glues_affFamtheoremparityOn_xorSumtheoremconsistent_affFamtheoremimarg_affLocaltheoremwsum_restrict₂theoremsysCoherent_pinnedtheoremxorSum_subsettheoremxorSumL_singletonstheoremxorSumL_appendtheoremxorSumL_niltheoremmap_snd_pintheoremmap_fst_pintheoremaffLocal_nonemptytheoremwsum_restricttheoremsysCoherent_hostedListtheoremxorSumL_eq_xorSumtheoremmap_snd_pairtheoremmap_fst_pairtheoremmem_affLocal_reltheoremexists_parity_solutiontheoremxorSumL_constheoremtransform_bookkeepingtheoremsymmDiff_emptytheoremparityOn_symmDifftheoremzmod2_add_selftheoremacyclic_iff_grahamReducib…theoremgrahamN_of_ripCovertheoremexists_ripCover_of_grahamNtheoremlistCover_eq_coverUtheoremAcyclicdefAdjdefClosedAtdefCoherentAtdefConformaldefConsistentdefCovereddefEarFreedefGluesdefGrahamNdefGrahamReducibledefIsChordlessCycledefIsCliquedefIsEarOfdefIsWalkOndefLocalStructstructureimargdefreldefteamdefRIPdefRIPCoverdefReachOndefSimpIndefSysCoherentdefaffFamdefaffLocaldefcoverUdefcyclePairsdefdecidableAcyclicdefdecidableIsEarOfdeffamCoverdefhostedListdefinstDecidableAdjdefinstDecidableCovereddefinstDecidableIsCliquedefjoinFamdeflistCoverdefparityOndefprojSdefshareddefwsumdefxorSumdefxorSumLdef
  1. DeclHiddenChannelCapacity.acyclic_iff_forall_consistent_gluesDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (𝒞 : Finset (Finset ι)),
  HiddenChannelCapacity.Acyclic 𝒞 ↔
    ∀ (fam : List (HiddenChannelCapacity.LocalStruct ι fun x => ZMod 2)),
      List.map (fun x => x.team) fam = 𝒞.toList →
        HiddenChannelCapacity.Consistent fam → (∀ L ∈ fam, L.rel.Nonempty) → HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.AcyclicHiddenChannelCapacity.ConsistentHiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.decidableAcyclic
    Uses
  2. DeclHiddenChannelCapacity.glues_of_acyclicDeclaration kindtheorem

    The order-free amalgamation theorem: an acyclic cover forces every pairwise-consistent family with duplicate-free teams to glue. The base structure, acyclicity, is decidable, so the sufficiency is machine-checkable.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {X : ι → Type u_2} [inst_1 : (i : ι) → DecidableEq (X i)] [inst_2 : Fintype ι]
  [(i : ι) → Fintype (X i)] [∀ (i : ι), Nonempty (X i)] (fam : List (HiddenChannelCapacity.LocalStruct ι X)),
  HiddenChannelCapacity.Consistent fam →
    (List.map (fun x => x.team) fam).Nodup →
      HiddenChannelCapacity.Acyclic (List.map (fun x => x.team) fam).toFinset → HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.AcyclicHiddenChannelCapacity.ConsistentHiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.RIPHiddenChannelCapacity.RIPCover
    Uses
    Used by
  3. DeclHiddenChannelCapacity.rip_iff_ripCoverDeclaration kindtheorem

    The family-level running intersection property reads only the teams.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {X : ι → Type u_2} (fam : List (HiddenChannelCapacity.LocalStruct ι X)),
  HiddenChannelCapacity.RIP fam ↔ HiddenChannelCapacity.RIPCover (List.map (fun x => x.team) fam)
    HiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.RIPHiddenChannelCapacity.RIPCoverHiddenChannelCapacity.famCoverHiddenChannelCapacity.listCover
    Uses
    Used by
  4. DeclHiddenChannelCapacity.famCover_eq_listCoverDeclaration kindtheorem
    ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : DecidableEq ι] (fam : List (HiddenChannelCapacity.LocalStruct ι X)),
  HiddenChannelCapacity.famCover fam = HiddenChannelCapacity.listCover (List.map (fun x => x.team) fam)
    HiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.famCoverHiddenChannelCapacity.listCover
    Used by
  5. DeclHiddenChannelCapacity.glues_of_ripDeclaration kindtheorem

    The amalgamation leg: over a running-intersection cover, a pairwise-consistent family glues: the base geometry forces the global structure.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {X : ι → Type u_2} [inst_1 : (i : ι) → DecidableEq (X i)] [inst_2 : Fintype ι]
  [(i : ι) → Fintype (X i)] [∀ (i : ι), Nonempty (X i)] (fam : List (HiddenChannelCapacity.LocalStruct ι X)),
  HiddenChannelCapacity.RIP fam → HiddenChannelCapacity.Consistent fam → HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.ConsistentHiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.RIPHiddenChannelCapacity.joinFamHiddenChannelCapacity.projS
    Uses
    Used by
  6. DeclHiddenChannelCapacity.projS_joinFamDeclaration kindtheorem

    The amalgamation theorem (positive Vorob'ev, certificate form): once the cover carries the running intersection property, the natural join of any pairwise-consistent family realizes every member exactly, so the base geometry licenses the global structure.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {X : ι → Type u_2} [inst_1 : (i : ι) → DecidableEq (X i)] [inst_2 : Fintype ι]
  [inst_3 : (i : ι) → Fintype (X i)] [∀ (i : ι), Nonempty (X i)] (fam : List (HiddenChannelCapacity.LocalStruct ι X)),
  HiddenChannelCapacity.RIP fam →
    HiddenChannelCapacity.Consistent fam →
      ∀ L ∈ fam, HiddenChannelCapacity.projS (HiddenChannelCapacity.joinFam fam) L.team = L.rel
    HiddenChannelCapacity.ConsistentHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.imargHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.RIPHiddenChannelCapacity.famCoverHiddenChannelCapacity.joinFamHiddenChannelCapacity.projS
    Uses
    Used by
  7. DeclHiddenChannelCapacity.team_subset_famCoverDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {X : ι → Type u_2} {fam : List (HiddenChannelCapacity.LocalStruct ι X)}
  {L : HiddenChannelCapacity.LocalStruct ι X}, L ∈ fam → L.team ⊆ HiddenChannelCapacity.famCover fam
    HiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.famCover
    Used by
  8. DeclHiddenChannelCapacity.projS_image_restrict₂Declaration kindtheorem

    The presheaf law: the restriction map carries the T-marginal onto the S-marginal. This is the compatibility any Čech-type complex over the marginal family consumes.

    ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → DecidableEq (X i)] (κ : Finset ((i : ι) → X i)) {S T : Finset ι}
  (hST : S ⊆ T), Finset.image (Finset.restrict₂ hST) (HiddenChannelCapacity.projS κ T) = HiddenChannelCapacity.projS κ S
    HiddenChannelCapacity.projS
    Used by
  9. DeclHiddenChannelCapacity.mem_joinFamDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {X : ι → Type u_2} [inst_1 : (i : ι) → DecidableEq (X i)] [inst_2 : Fintype ι]
  [inst_3 : (i : ι) → Fintype (X i)] {fam : List (HiddenChannelCapacity.LocalStruct ι X)} {f : (i : ι) → X i},
  f ∈ HiddenChannelCapacity.joinFam fam ↔ ∀ L ∈ fam, L.team.restrict f ∈ L.rel
    HiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.joinFam
    Used by
  10. DeclHiddenChannelCapacity.exists_restrict_eqDeclaration kindtheorem

    Any local configuration extends to a global one, on nonempty parts.

    ∀ {ι : Type u_1} {X : ι → Type u_2} [∀ (i : ι), Nonempty (X i)] (T : Finset ι) (g : (i : ↥T) → X ↑i),
  ∃ f, T.restrict f = g
    Used by
  11. DeclHiddenChannelCapacity.LocalStruct.imarg_imageDeclaration kindtheorem

    Sub-marginalizing an interface marginal composes.

    ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → DecidableEq (X i)] (L : HiddenChannelCapacity.LocalStruct ι X)
  {S T : Finset ι} (hS : S ⊆ T) (hT : T ⊆ L.team), Finset.image (Finset.restrict₂ hS) (L.imarg hT) = L.imarg ⋯
    HiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.imargHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.team
    Used by
  12. DeclHiddenChannelCapacity.glues_of_permDeclaration kindtheorem

    Gluing is permutation-invariant.

    ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → DecidableEq (X i)] [inst_1 : Fintype ι] [(i : ι) → Fintype (X i)]
  {fam fam' : List (HiddenChannelCapacity.LocalStruct ι X)},
  fam'.Perm fam → HiddenChannelCapacity.Glues fam' → HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.projS
    Used by
  13. DeclHiddenChannelCapacity.exists_perm_map_eqDeclaration kindtheorem

    A permutation of a mapped list lifts along the map.

    ∀ {α : Type u_3} {β : Type u_4} {g : α → β} {σ : List β} {l : List α},
  σ.Perm (List.map g l) → ∃ l', l'.Perm l ∧ List.map g l' = σ
    Used by
  14. DeclHiddenChannelCapacity.consistent_of_permDeclaration kindtheorem

    Pairwise consistency is permutation-invariant.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {X : ι → Type u_2} [inst_1 : (i : ι) → DecidableEq (X i)]
  {fam fam' : List (HiddenChannelCapacity.LocalStruct ι X)},
  fam'.Perm fam → HiddenChannelCapacity.Consistent fam → HiddenChannelCapacity.Consistent fam'
    HiddenChannelCapacity.ConsistentHiddenChannelCapacity.LocalStruct
    Used by
  15. DeclHiddenChannelCapacity.exists_consistent_not_glues_of_not_acyclicDeclaration kindtheorem

    The CAPSTONE: a non-acyclic cover hosts a pairwise-consistent family of nonempty local relations that no global structure realizes: the base structure carries what local consistency cannot.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (𝒞 : Finset (Finset ι)),
  ¬HiddenChannelCapacity.Acyclic 𝒞 →
    ∃ fam,
      List.map (fun x => x.team) fam = 𝒞.toList ∧
        HiddenChannelCapacity.Consistent fam ∧ (∀ L ∈ fam, L.rel.Nonempty) ∧ ¬HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.AcyclicHiddenChannelCapacity.ConsistentHiddenChannelCapacity.EarFreeHiddenChannelCapacity.GluesHiddenChannelCapacity.GrahamReducibleHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.team
    Uses
    Used by
  16. DeclHiddenChannelCapacity.earFree_dichotomyDeclaration kindtheorem

    The ear-free dichotomy: an ear-free cover is non-conformal or contains a chordless cycle. Dirac's lemma on the shared vertices produces a simplicial shared vertex, and the one-step GYO collapse turns it into an ear.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  HiddenChannelCapacity.EarFree 𝒞 → ¬HiddenChannelCapacity.Conformal 𝒞 ∨ ∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l
    HiddenChannelCapacity.AdjHiddenChannelCapacity.ConformalHiddenChannelCapacity.EarFreeHiddenChannelCapacity.IsChordlessCycleHiddenChannelCapacity.IsEarOfHiddenChannelCapacity.SimpInHiddenChannelCapacity.shared
    Uses
    Used by
  17. DeclHiddenChannelCapacity.shared_nonempty_of_earFreeDeclaration kindtheorem

    An ear-free cover has a shared vertex: every team has nonempty boundary.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)},
  HiddenChannelCapacity.EarFree 𝒞 → (HiddenChannelCapacity.shared 𝒞).Nonempty
    HiddenChannelCapacity.EarFreeHiddenChannelCapacity.IsEarOfHiddenChannelCapacity.coverUHiddenChannelCapacity.shared
    Uses
    Used by
  18. DeclHiddenChannelCapacity.isEarOf_of_simplicialDeclaration kindtheorem

    The one-step GYO collapse: in a conformal cover, a simplicial shared vertex yields an ear — every team containing it has boundary inside the team covering its closed shared neighborhood.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)},
  HiddenChannelCapacity.Conformal 𝒞 →
    ∀ {v : ι},
      v ∈ HiddenChannelCapacity.shared 𝒞 →
        (∀ x ∈ HiddenChannelCapacity.shared 𝒞,
            ∀ y ∈ HiddenChannelCapacity.shared 𝒞,
              HiddenChannelCapacity.Adj 𝒞 v x →
                HiddenChannelCapacity.Adj 𝒞 v y → x ≠ y → HiddenChannelCapacity.Adj 𝒞 x y) →
          ∃ T ∈ 𝒞, HiddenChannelCapacity.IsEarOf 𝒞 T
    HiddenChannelCapacity.AdjHiddenChannelCapacity.ConformalHiddenChannelCapacity.CoveredHiddenChannelCapacity.IsCliqueHiddenChannelCapacity.IsEarOfHiddenChannelCapacity.coverUHiddenChannelCapacity.instDecidableAdjHiddenChannelCapacity.shared
    Uses
    Used by
  19. DeclHiddenChannelCapacity.bndry_eq_inter_sharedDeclaration kindtheorem

    A team's boundary is its shared part.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)} {T : Finset ι},
  T ∈ 𝒞 → T ∩ HiddenChannelCapacity.coverU (𝒞.erase T) = T ∩ HiddenChannelCapacity.shared 𝒞
    HiddenChannelCapacity.coverUHiddenChannelCapacity.shared
    Uses
    Used by
  20. DeclHiddenChannelCapacity.mem_sharedDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)} {v : ι},
  v ∈ HiddenChannelCapacity.shared 𝒞 ↔ ∃ T ∈ 𝒞, ∃ T' ∈ 𝒞, T ≠ T' ∧ v ∈ T ∧ v ∈ T'
    HiddenChannelCapacity.coverUHiddenChannelCapacity.shared
    Uses
    Used by
  21. DeclHiddenChannelCapacity.dirac_strongDeclaration kindtheorem

    Dirac's lemma, strong form: in a chordless-cycle-free adjacency structure, every vertex set is a clique or contains two nonadjacent simplicial vertices.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  (¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l) →
    ∀ (S : Finset ι),
      (∀ x ∈ S, ∀ y ∈ S, x ≠ y → HiddenChannelCapacity.Adj 𝒞 x y) ∨
        ∃ u w,
          HiddenChannelCapacity.SimpIn 𝒞 S u ∧
            HiddenChannelCapacity.SimpIn 𝒞 S w ∧ u ≠ w ∧ ¬HiddenChannelCapacity.Adj 𝒞 u w
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsChordlessCycleHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOnHiddenChannelCapacity.SimpInHiddenChannelCapacity.instDecidableAdj
    Uses
    Used by
  22. DeclHiddenChannelCapacity.sep_clique_stepDeclaration kindtheorem

    The assembled-cycle contradiction: two length-minimal x-y connectors through disjoint, mutually non-adjacent sides cannot coexist with chordless-cycle-freeness when x and y are non-adjacent.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)},
  (¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l) →
    ∀ {QA QB : ι → Prop} {x y : ι},
      x ≠ y →
        ¬HiddenChannelCapacity.Adj 𝒞 x y →
          ¬QB x →
            ¬QB y →
              (∀ (v : ι), QA v → QB v → False) →
                (∀ (u v : ι), QA u → QB v → ¬HiddenChannelCapacity.Adj 𝒞 u v) →
                  ∀ (pA : List ι),
                    List.IsChain (HiddenChannelCapacity.Adj 𝒞) pA →
                      pA.Nodup →
                        pA.head? = some x →
                          pA.getLast? = some y →
                            (∀ v ∈ pA, v = x ∨ v = y ∨ QA v) →
                              (∀ (q : List ι),
                                  (List.IsChain (HiddenChannelCapacity.Adj 𝒞) q ∧
                                      q.Nodup ∧
                                        q.head? = some x ∧ q.getLast? = some y ∧ ∀ v ∈ q, v = x ∨ v = y ∨ QA v) →
                                    pA.length ≤ q.length) →
                                ∀ (pB : List ι),
                                  List.IsChain (HiddenChannelCapacity.Adj 𝒞) pB →
                                    pB.Nodup →
                                      pB.head? = some x →
                                        pB.getLast? = some y →
                                          (∀ v ∈ pB, v = x ∨ v = y ∨ QB v) →
                                            (∀ (q : List ι),
                                                (List.IsChain (HiddenChannelCapacity.Adj 𝒞) q ∧
                                                    q.Nodup ∧
                                                      q.head? = some x ∧
                                                        q.getLast? = some y ∧ ∀ v ∈ q, v = x ∨ v = y ∨ QB v) →
                                                  pB.length ≤ q.length) →
                                              False
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsChordlessCycleHiddenChannelCapacity.cyclePairs
    Uses
    Used by
  23. DeclHiddenChannelCapacity.no_chord_of_minimalDeclaration kindtheorem

    Minimality kills chords: a length-minimal constrained x-y path has no adjacency between positions at distance ≥ 2.

    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {Q : ι → Prop} {x y : ι} {p : List ι},
  List.IsChain (HiddenChannelCapacity.Adj 𝒞) p →
    p.head? = some x →
      p.getLast? = some y →
        (∀ v ∈ p, v = x ∨ v = y ∨ Q v) →
          (∀ (q : List ι),
              (List.IsChain (HiddenChannelCapacity.Adj 𝒞) q ∧
                  q.Nodup ∧ q.head? = some x ∧ q.getLast? = some y ∧ ∀ v ∈ q, v = x ∨ v = y ∨ Q v) →
                p.length ≤ q.length) →
            p.Nodup →
              ∀ {i j : ℕ} (hi : i < p.length) (hj : j < p.length), i + 2 ≤ j → ¬HiddenChannelCapacity.Adj 𝒞 p[i] p[j]
    HiddenChannelCapacity.Adj
    Uses
    Used by
  24. DeclHiddenChannelCapacity.getLast_getElemDeclaration kindtheorem
    ∀ {ι : Type u_1} {p : List ι} {y : ι}, p.getLast? = some y → ∀ (h0 : 0 < p.length), p[p.length - 1] = y
    Used by
  25. DeclHiddenChannelCapacity.reachOn_transDeclaration kindtheorem
    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v w : ι},
  HiddenChannelCapacity.ReachOn 𝒞 P u v → HiddenChannelCapacity.ReachOn 𝒞 P v w → HiddenChannelCapacity.ReachOn 𝒞 P u w
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Uses
    Used by
  26. DeclHiddenChannelCapacity.reachOn_symmDeclaration kindtheorem
    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v : ι},
  HiddenChannelCapacity.ReachOn 𝒞 P u v → HiddenChannelCapacity.ReachOn 𝒞 P v u
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Uses
    Used by
  27. DeclHiddenChannelCapacity.reachOn_reflDeclaration kindtheorem
    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u : ι}, P u → HiddenChannelCapacity.ReachOn 𝒞 P u u
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Used by
  28. DeclHiddenChannelCapacity.reachOn_of_mem_walkDeclaration kindtheorem

    Every vertex on a walk is reachable from its head.

    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v : ι} {p : List ι},
  HiddenChannelCapacity.IsWalkOn 𝒞 P p → p.head? = some u → v ∈ p → HiddenChannelCapacity.ReachOn 𝒞 P u v
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Uses
    Used by
  29. DeclHiddenChannelCapacity.reachOn_extendDeclaration kindtheorem
    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} {u v w : ι},
  HiddenChannelCapacity.ReachOn 𝒞 P u v → HiddenChannelCapacity.Adj 𝒞 v w → P w → HiddenChannelCapacity.ReachOn 𝒞 P u w
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Uses
    Used by
  30. DeclHiddenChannelCapacity.exists_min_pathDeclaration kindtheorem
    ∀ {ι : Type u_1} {Q : List ι → Prop}, (∃ p, Q p) → ∃ p, Q p ∧ ∀ (q : List ι), Q q → p.length ≤ q.length
    Used by
  31. DeclHiddenChannelCapacity.exists_connectorDeclaration kindtheorem

    A connector: an x-y path with interior inside Q, from adjacent entry points and interior reachability.

    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {Q : ι → Prop} {x y u₁ u₂ : ι},
  x ≠ y →
    HiddenChannelCapacity.Adj 𝒞 x u₁ →
      HiddenChannelCapacity.Adj 𝒞 y u₂ →
        HiddenChannelCapacity.ReachOn 𝒞 Q u₁ u₂ →
          ¬Q x →
            ¬Q y →
              ∃ p,
                List.IsChain (HiddenChannelCapacity.Adj 𝒞) p ∧
                  p.Nodup ∧ p.head? = some x ∧ p.getLast? = some y ∧ ∀ v ∈ p, v = x ∨ v = y ∨ Q v
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Uses
    Used by
  32. DeclHiddenChannelCapacity.erase_separatesDeclaration kindtheorem

    If x has no neighbor reachable from a off the separator, then erasing x still separates: the first x-occurrence on any violating path has its predecessor reachable from a and adjacent to x.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)} {S Sep : Finset ι} {a b x : ι},
  x ≠ a →
    (∀ (u : ι),
        u ∈ S \ Sep ∧ HiddenChannelCapacity.ReachOn 𝒞 (fun v => v ∈ S \ Sep) a u → ¬HiddenChannelCapacity.Adj 𝒞 x u) →
      ¬HiddenChannelCapacity.ReachOn 𝒞 (fun v => v ∈ S \ Sep) a b →
        ¬HiddenChannelCapacity.ReachOn 𝒞 (fun v => v ∈ S \ Sep.erase x) a b
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Uses
    Used by
  33. DeclHiddenChannelCapacity.reachOn_of_walkDeclaration kindtheorem

    Every chained walk contains a duplicate-free path with the same endpoints and vertices.

    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {P : ι → Prop} (p : List ι),
  HiddenChannelCapacity.IsWalkOn 𝒞 P p →
    ∀ {u v : ι}, p.head? = some u → p.getLast? = some v → HiddenChannelCapacity.ReachOn 𝒞 P u v
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsWalkOnHiddenChannelCapacity.ReachOn
    Uses
    Used by
  34. DeclHiddenChannelCapacity.isChain_dropDeclaration kindtheorem
    ∀ {ι : Type u_1} {R : ι → ι → Prop} {p : List ι}, List.IsChain R p → ∀ (n : ℕ), List.IsChain R (List.drop n p)
    Used by
  35. DeclHiddenChannelCapacity.isChain_takeDeclaration kindtheorem
    ∀ {ι : Type u_1} {R : ι → ι → Prop} {p : List ι}, List.IsChain R p → ∀ (n : ℕ), List.IsChain R (List.take n p)
    Used by
  36. DeclHiddenChannelCapacity.head_getElemDeclaration kindtheorem

    Positional form of the head.

    ∀ {ι : Type u_1} {p : List ι} {x : ι}, p.head? = some x → ∀ (h0 : 0 < p.length), p[0] = x
    Used by
  37. DeclHiddenChannelCapacity.gcast_listDeclaration kindtheorem
    ∀ {ι : Type u_1} (l : List ι) {s t : ℕ} (hs : s < l.length) (ht : t < l.length), s = t → l[s] = l[t]
    Used by
  38. DeclHiddenChannelCapacity.Adj.symm'Declaration kindtheorem
    ∀ {ι : Type u_1} {𝒞 : Finset (Finset ι)} {u v : ι}, HiddenChannelCapacity.Adj 𝒞 u v → HiddenChannelCapacity.Adj 𝒞 v u
    HiddenChannelCapacity.Adj
    Used by
  39. DeclHiddenChannelCapacity.capstone_of_dichotomyDeclaration kindtheorem

    The capstone, modulo the dichotomy: once every ear-free core is non-conformal or has a chordless cycle (the Dirac edge, URS D26 L6), every non-Graham-reducible cover hosts the base structure that licenses the verdict: a pairwise-consistent family of nonempty local relations that no global structure realizes.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (𝒞 : Finset (Finset ι)),
  ¬HiddenChannelCapacity.GrahamReducible 𝒞 →
    (∀ 𝒞' ⊆ 𝒞,
        HiddenChannelCapacity.EarFree 𝒞' →
          ¬HiddenChannelCapacity.Conformal 𝒞' ∨ ∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞' l) →
      ∃ fam,
        List.map (fun x => x.team) fam = 𝒞.toList ∧
          HiddenChannelCapacity.Consistent fam ∧ (∀ L ∈ fam, L.rel.Nonempty) ∧ ¬HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.ConformalHiddenChannelCapacity.ConsistentHiddenChannelCapacity.EarFreeHiddenChannelCapacity.GluesHiddenChannelCapacity.GrahamReducibleHiddenChannelCapacity.IsChordlessCycleHiddenChannelCapacity.IsEarOfHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.coverUHiddenChannelCapacity.xorSum
    Uses
    Used by
  40. DeclHiddenChannelCapacity.exists_earFree_core_chainDeclaration kindtheorem

    Chain extraction: a non-Graham-reducible cover has an ear-free core such that any vertex set inside the core's cover hosted anywhere in the cover is hosted inside the core.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  ¬HiddenChannelCapacity.GrahamReducible 𝒞 →
    ∃ 𝒞' ⊆ 𝒞,
      HiddenChannelCapacity.EarFree 𝒞' ∧ ∀ w ⊆ HiddenChannelCapacity.coverU 𝒞', (∃ V ∈ 𝒞, w ⊆ V) → ∃ W ∈ 𝒞', w ⊆ W
    HiddenChannelCapacity.EarFreeHiddenChannelCapacity.GrahamNHiddenChannelCapacity.GrahamReducibleHiddenChannelCapacity.IsEarOfHiddenChannelCapacity.coverUHiddenChannelCapacity.decidableIsEarOf
    Used by
  41. DeclHiddenChannelCapacity.clean_system_of_uncovered_cliqueDeclaration kindtheorem

    The clique datum: a cardinality-minimal non-covered clique yields a clean system. Minimality covers the erase-sets; non-coveredness is cleanliness; parity closes by counting.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  𝒞.Nonempty →
    ¬HiddenChannelCapacity.Conformal 𝒞 →
      ∃ 𝒲,
        𝒲.Nonempty ∧
          (∀ w ∈ 𝒲, w ≠ ∅) ∧
            (∀ w ∈ 𝒲, ∃ T ∈ 𝒞, w ⊆ T) ∧
              (∀ V ∈ 𝒞, ∀ w₁ ∈ 𝒲, ∀ w₂ ∈ 𝒲, w₁ ⊆ V → w₂ ⊆ V → w₁ = w₂) ∧ HiddenChannelCapacity.xorSum 𝒲 = ∅
    HiddenChannelCapacity.AdjHiddenChannelCapacity.ConformalHiddenChannelCapacity.CoveredHiddenChannelCapacity.IsCliqueHiddenChannelCapacity.coverUHiddenChannelCapacity.instDecidableCoveredHiddenChannelCapacity.instDecidableIsCliqueHiddenChannelCapacity.xorSumHiddenChannelCapacity.xorSumL
    Uses
    Used by
  42. DeclHiddenChannelCapacity.xorSum_eq_empty_iffDeclaration kindtheorem

    An F2 sum vanishes iff every incidence count is even.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {D : Finset (Finset ι)},
  HiddenChannelCapacity.xorSum D = ∅ ↔ ∀ (i : ι), ¬Odd {x ∈ D | i ∈ x}.card
    HiddenChannelCapacity.xorSum
    Uses
    Used by
  43. DeclHiddenChannelCapacity.mem_xorSumDeclaration kindtheorem

    Membership in an F2 sum is odd incidence.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {D : Finset (Finset ι)} {i : ι},
  i ∈ HiddenChannelCapacity.xorSum D ↔ Odd {x ∈ D | i ∈ x}.card
    HiddenChannelCapacity.xorSum
    Used by
  44. DeclHiddenChannelCapacity.erase_union_eraseDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {K : Finset ι} {i j : ι}, i ≠ j → K.erase i ∪ K.erase j = K
    Used by
  45. DeclHiddenChannelCapacity.covered_of_card_le_twoDeclaration kindtheorem

    Small cliques are covered: the empty set (nonempty cover), singletons, edges.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)},
  𝒞.Nonempty →
    ∀ {K : Finset ι},
      K ⊆ HiddenChannelCapacity.coverU 𝒞 →
        HiddenChannelCapacity.IsClique 𝒞 K → K.card ≤ 2 → HiddenChannelCapacity.Covered 𝒞 K
    HiddenChannelCapacity.AdjHiddenChannelCapacity.CoveredHiddenChannelCapacity.IsCliqueHiddenChannelCapacity.coverU
    Uses
    Used by
  46. DeclHiddenChannelCapacity.mem_coverUDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)} {v : ι},
  v ∈ HiddenChannelCapacity.coverU 𝒞 ↔ ∃ T ∈ 𝒞, v ∈ T
    HiddenChannelCapacity.coverU
    Used by
  47. DeclHiddenChannelCapacity.clean_system_of_chordlessCycleDeclaration kindtheorem

    The clean system of a chordless cycle, in finder form.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)} {l : List ι},
  HiddenChannelCapacity.IsChordlessCycle 𝒞 l →
    ∃ 𝒲,
      𝒲.Nonempty ∧
        (∀ w ∈ 𝒲, w ≠ ∅) ∧
          (∀ w ∈ 𝒲, ∃ T ∈ 𝒞, w ⊆ T) ∧
            (∀ V ∈ 𝒞, ∀ w₁ ∈ 𝒲, ∀ w₂ ∈ 𝒲, w₁ ⊆ V → w₂ ⊆ V → w₁ = w₂) ∧ HiddenChannelCapacity.xorSum 𝒲 = ∅
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsChordlessCycleHiddenChannelCapacity.cyclePairsHiddenChannelCapacity.xorSumHiddenChannelCapacity.xorSumL
    Uses
    Used by
  48. DeclHiddenChannelCapacity.xorSumL_cyclePairsDeclaration kindtheorem

    The cycle sum telescopes: consecutive pairs of a duplicate-free cyclic list sum to ∅ over F2 — every vertex lies in exactly two pairs.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List ι),
  l.Nodup → 2 ≤ l.length → HiddenChannelCapacity.xorSumL (HiddenChannelCapacity.cyclePairs l) = ∅
    HiddenChannelCapacity.cyclePairsHiddenChannelCapacity.xorSumL
    Uses
    Used by
  49. DeclHiddenChannelCapacity.xorSumL_zipWith_symmDiffDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (l₁ l₂ : List (Finset ι)),
  l₁.length = l₂.length →
    HiddenChannelCapacity.xorSumL (List.zipWith (fun x1 x2 => symmDiff x1 x2) l₁ l₂) =
      symmDiff (HiddenChannelCapacity.xorSumL l₁) (HiddenChannelCapacity.xorSumL l₂)
    HiddenChannelCapacity.xorSumL
    Uses
    Used by
  50. DeclHiddenChannelCapacity.xorSumL_permDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {l₁ l₂ : List (Finset ι)},
  l₁.Perm l₂ → HiddenChannelCapacity.xorSumL l₁ = HiddenChannelCapacity.xorSumL l₂
    HiddenChannelCapacity.xorSumL
    Uses
    Used by
  51. DeclHiddenChannelCapacity.pair_eq_symmDiffDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {a b : ι}, a ≠ b → {a, b} = symmDiff {a} {b}
    Used by
  52. DeclHiddenChannelCapacity.getElem_ne_nextDeclaration kindtheorem
    ∀ {ι : Type u_1} (l : List ι), l.Nodup → ∀ (h2 : 2 ≤ l.length) (i : ℕ) (hi : i < l.length), l[i] ≠ l[(i + 1) % l.length]
    Uses
    Used by
  53. DeclHiddenChannelCapacity.nodup_cyclePairsDeclaration kindtheorem

    Distinct positions carry distinct pairs: the pair list is duplicate-free.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List ι),
  l.Nodup → 3 ≤ l.length → (HiddenChannelCapacity.cyclePairs l).Nodup
    HiddenChannelCapacity.cyclePairs
    Uses
    Used by
  54. DeclHiddenChannelCapacity.cyclePairs_ne_emptyDeclaration kindtheorem

    Members of the cycle-pair list are nonempty.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {l : List ι},
  0 < l.length → ∀ {w : Finset ι}, w ∈ HiddenChannelCapacity.cyclePairs l → w ≠ ∅
    HiddenChannelCapacity.cyclePairs
    Uses
    Used by
  55. DeclHiddenChannelCapacity.clean_of_chordlessCycleDeclaration kindtheorem

    Chordlessness is cleanliness: no team hosts two distinct pairs of a chordless cycle.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {𝒞 : Finset (Finset ι)} {l : List ι},
  HiddenChannelCapacity.IsChordlessCycle 𝒞 l →
    ∀ V ∈ 𝒞,
      ∀ w₁ ∈ HiddenChannelCapacity.cyclePairs l, ∀ w₂ ∈ HiddenChannelCapacity.cyclePairs l, w₁ ⊆ V → w₂ ⊆ V → w₁ = w₂
    HiddenChannelCapacity.AdjHiddenChannelCapacity.IsChordlessCycleHiddenChannelCapacity.cyclePairs
    Uses
    Used by
  56. DeclHiddenChannelCapacity.mod_succ_casesDeclaration kindtheorem
    ∀ (n i : ℕ), i < n → (i + 1) % n = i + 1 ∧ i + 1 < n ∨ (i + 1) % n = 0 ∧ i + 1 = n
    Used by
  57. DeclHiddenChannelCapacity.getElem_cyclePairsDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List ι) (h0 : 0 < l.length) (i : ℕ)
  (h : i < (HiddenChannelCapacity.cyclePairs l).length),
  (HiddenChannelCapacity.cyclePairs l)[i] = {l[i], l[(i + 1) % l.length]}
    HiddenChannelCapacity.cyclePairs
    Uses
    Used by
  58. DeclHiddenChannelCapacity.length_cyclePairsDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List ι), (HiddenChannelCapacity.cyclePairs l).length = l.length
    HiddenChannelCapacity.cyclePairs
    Used by
  59. DeclHiddenChannelCapacity.adj_or_eq_of_cohostedDeclaration kindtheorem

    Co-hosted vertices are adjacent or equal.

    ∀ {ι : Type u_1} [DecidableEq ι] {𝒞 : Finset (Finset ι)} {V : Finset ι},
  V ∈ 𝒞 → ∀ {u v : ι}, u ∈ V → v ∈ V → HiddenChannelCapacity.Adj 𝒞 u v ∨ u = v
    HiddenChannelCapacity.Adj
    Used by
  60. DeclHiddenChannelCapacity.capstone_of_coreDeclaration kindtheorem

    The transfer: a clean system on a chained ear-free core is a clean system on the full cover — any team hosting two members routes them into a single core team.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (𝒞 𝒞' : Finset (Finset ι)),
  𝒞' ⊆ 𝒞 →
    (∀ w ⊆ HiddenChannelCapacity.coverU 𝒞', (∃ V ∈ 𝒞, w ⊆ V) → ∃ W ∈ 𝒞', w ⊆ W) →
      ∀ (𝒲 : Finset (Finset ι)),
        𝒲.Nonempty →
          (∀ w ∈ 𝒲, w ≠ ∅) →
            (∀ w ∈ 𝒲, ∃ T ∈ 𝒞', w ⊆ T) →
              (∀ V ∈ 𝒞', ∀ w₁ ∈ 𝒲, ∀ w₂ ∈ 𝒲, w₁ ⊆ V → w₂ ⊆ V → w₁ = w₂) →
                HiddenChannelCapacity.xorSum 𝒲 = ∅ →
                  ∃ fam,
                    List.map (fun x => x.team) fam = 𝒞.toList ∧
                      HiddenChannelCapacity.Consistent fam ∧
                        (∀ L ∈ fam, L.rel.Nonempty) ∧ ¬HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.ConsistentHiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.coverUHiddenChannelCapacity.xorSum
    Uses
    Used by
  61. DeclHiddenChannelCapacity.clean_system_obstructionDeclaration kindtheorem

    The clean-system obstruction, the unified consumption theorem of C-ENGINE: a base-side clean system (a nonempty hosted family of distinct nonempty supports with vanishing F2 sum, no team hosting two) licenses a verdict on local measurement, a pairwise-consistent family of nonempty local relations over the whole cover that no global structure realizes. Every witness rung (chordless cycles, even boundary data, landings, the H_k clique parities) differs only as a FINDER of such a base system.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (𝒞 𝒲 : Finset (Finset ι)),
  𝒲.Nonempty →
    (∀ w ∈ 𝒲, w ≠ ∅) →
      (∀ w ∈ 𝒲, ∃ V ∈ 𝒞, w ⊆ V) →
        (∀ V ∈ 𝒞, ∀ w₁ ∈ 𝒲, ∀ w₂ ∈ 𝒲, w₁ ⊆ V → w₂ ⊆ V → w₁ = w₂) →
          HiddenChannelCapacity.xorSum 𝒲 = ∅ →
            ∃ fam,
              List.map (fun x => x.team) fam = 𝒞.toList ∧
                HiddenChannelCapacity.Consistent fam ∧ (∀ L ∈ fam, L.rel.Nonempty) ∧ ¬HiddenChannelCapacity.Glues fam
    HiddenChannelCapacity.ClosedAtHiddenChannelCapacity.CoherentAtHiddenChannelCapacity.ConsistentHiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.affFamHiddenChannelCapacity.affLocalHiddenChannelCapacity.xorSum
    Uses
    Used by
  62. DeclHiddenChannelCapacity.affine_obstructionDeclaration kindtheorem

    The affine obstruction engine, packaged: from a base-side hosted odd dependency (over a closed coherent system) follows a verdict on local measurement, a family of nonempty local relations that is pairwise consistent yet realizes no global structure.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {teams : List (Finset ι)} {𝒲 : Finset (Finset ι)}
  {c : Finset ι → ZMod 2},
  teams ≠ [] →
    (∀ V ∈ teams, HiddenChannelCapacity.ClosedAt 𝒲 V) →
      (∀ V ∈ teams, HiddenChannelCapacity.CoherentAt 𝒲 c V) →
        ∀ D ⊆ 𝒲,
          HiddenChannelCapacity.xorSum D = ∅ →
            ∑ w ∈ D, c w = 1 →
              (∀ w ∈ D, ∃ V ∈ teams, w ⊆ V) →
                HiddenChannelCapacity.Consistent (HiddenChannelCapacity.affFam teams 𝒲 c) ∧
                  (∀ L ∈ HiddenChannelCapacity.affFam teams 𝒲 c, L.rel.Nonempty) ∧
                    ¬HiddenChannelCapacity.Glues (HiddenChannelCapacity.affFam teams 𝒲 c)
    HiddenChannelCapacity.ClosedAtHiddenChannelCapacity.CoherentAtHiddenChannelCapacity.ConsistentHiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.affFamHiddenChannelCapacity.affLocalHiddenChannelCapacity.xorSum
    Uses
    Used by
  63. DeclHiddenChannelCapacity.not_glues_affFamDeclaration kindtheorem

    The obstruction theorem: a hosted odd dependency (a base-side witness) forecloses every global structure; any global realizing all the local relations would satisfy every hosted constraint, and the dependency sums those satisfactions to 0 = 1.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {teams : List (Finset ι)} {𝒲 : Finset (Finset ι)}
  {c : Finset ι → ZMod 2},
  teams ≠ [] →
    (∀ V ∈ teams, HiddenChannelCapacity.CoherentAt 𝒲 c V) →
      ∀ D ⊆ 𝒲,
        HiddenChannelCapacity.xorSum D = ∅ →
          ∑ w ∈ D, c w = 1 →
            (∀ w ∈ D, ∃ V ∈ teams, w ⊆ V) → ¬HiddenChannelCapacity.Glues (HiddenChannelCapacity.affFam teams 𝒲 c)
    HiddenChannelCapacity.CoherentAtHiddenChannelCapacity.GluesHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.affFamHiddenChannelCapacity.affLocalHiddenChannelCapacity.parityOnHiddenChannelCapacity.projSHiddenChannelCapacity.wsumHiddenChannelCapacity.xorSum
    Uses
    Used by
  64. DeclHiddenChannelCapacity.parityOn_xorSumDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (D : Finset (Finset ι)) (f : ι → ZMod 2),
  HiddenChannelCapacity.parityOn (HiddenChannelCapacity.xorSum D) f = ∑ w ∈ D, HiddenChannelCapacity.parityOn w f
    HiddenChannelCapacity.parityOnHiddenChannelCapacity.xorSum
    Uses
    Used by
  65. DeclHiddenChannelCapacity.consistent_affFamDeclaration kindtheorem

    Closed coherent affine families are pairwise consistent: both interface marginals ARE the interface's visible system.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {teams : List (Finset ι)} {𝒲 : Finset (Finset ι)} {c : Finset ι → ZMod 2},
  (∀ V ∈ teams, HiddenChannelCapacity.ClosedAt 𝒲 V) →
    (∀ V ∈ teams, HiddenChannelCapacity.CoherentAt 𝒲 c V) →
      HiddenChannelCapacity.Consistent (HiddenChannelCapacity.affFam teams 𝒲 c)
    HiddenChannelCapacity.ClosedAtHiddenChannelCapacity.CoherentAtHiddenChannelCapacity.ConsistentHiddenChannelCapacity.LocalStructHiddenChannelCapacity.LocalStruct.imargHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.affFamHiddenChannelCapacity.affLocal
    Uses
    Used by
  66. DeclHiddenChannelCapacity.imarg_affLocalDeclaration kindtheorem

    The exact marginal computation: the interface marginal of a closed coherent local structure is exactly the local structure of the interface — the interface sees precisely the visible constraints.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V S : Finset ι} {𝒲 : Finset (Finset ι)} {c : Finset ι → ZMod 2} (hS : S ⊆ V),
  HiddenChannelCapacity.ClosedAt 𝒲 V →
    HiddenChannelCapacity.CoherentAt 𝒲 c V →
      (HiddenChannelCapacity.affLocal V 𝒲 c).imarg hS = (HiddenChannelCapacity.affLocal S 𝒲 c).rel
    HiddenChannelCapacity.ClosedAtHiddenChannelCapacity.CoherentAtHiddenChannelCapacity.LocalStruct.imargHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.affLocalHiddenChannelCapacity.hostedListHiddenChannelCapacity.parityOnHiddenChannelCapacity.wsum
    Uses
    Used by
  67. DeclHiddenChannelCapacity.wsum_restrict₂Declaration kindtheorem

    Transport of team parities along nested restriction: the value only reads the support.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V S w : Finset ι} (hS : S ⊆ V),
  w ⊆ S → ∀ (F : ↥V → ZMod 2), HiddenChannelCapacity.wsum S w (Finset.restrict₂ hS F) = HiddenChannelCapacity.wsum V w F
    HiddenChannelCapacity.parityOnHiddenChannelCapacity.wsum
    Uses
    Used by
  68. DeclHiddenChannelCapacity.sysCoherent_pinnedDeclaration kindtheorem

    The pinned system: hosted constraints of V plus a singleton pin at every S-coordinate of a visible-constraint-satisfying trace. Coherent, by closedness.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V S : Finset ι} {𝒲 : Finset (Finset ι)} {c : Finset ι → ZMod 2},
  HiddenChannelCapacity.ClosedAt 𝒲 V →
    HiddenChannelCapacity.CoherentAt 𝒲 c V →
      ∀ (g₀ : ι → ZMod 2),
        (∀ w ∈ 𝒲, w ⊆ S → HiddenChannelCapacity.parityOn w g₀ = c w) →
          HiddenChannelCapacity.SysCoherent
            (HiddenChannelCapacity.hostedList✝ V 𝒲 c ++ List.map (fun i => ({i}, g₀ i)) S.toList)
    HiddenChannelCapacity.ClosedAtHiddenChannelCapacity.CoherentAtHiddenChannelCapacity.SysCoherentHiddenChannelCapacity.hostedListHiddenChannelCapacity.parityOnHiddenChannelCapacity.xorSumHiddenChannelCapacity.xorSumL
    Uses
    Used by
  69. DeclHiddenChannelCapacity.xorSum_subsetDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V : Finset ι} {𝒲 D : Finset (Finset ι)},
  D ⊆ {x ∈ 𝒲 | x ⊆ V} → HiddenChannelCapacity.xorSum D ⊆ V
    HiddenChannelCapacity.xorSum
    Used by
  70. DeclHiddenChannelCapacity.xorSumL_singletonsDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {l : List ι},
  l.Nodup → HiddenChannelCapacity.xorSumL (List.map (fun x => {x}) l) = l.toFinset
    HiddenChannelCapacity.xorSumL
    Uses
    Used by
  71. DeclHiddenChannelCapacity.xorSumL_appendDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (a b : List (Finset ι)),
  HiddenChannelCapacity.xorSumL (a ++ b) = symmDiff (HiddenChannelCapacity.xorSumL a) (HiddenChannelCapacity.xorSumL b)
    HiddenChannelCapacity.xorSumL
    Uses
    Used by
  72. DeclHiddenChannelCapacity.xorSumL_nilDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι], HiddenChannelCapacity.xorSumL [] = ∅
    HiddenChannelCapacity.xorSumL
    Used by
  73. DeclHiddenChannelCapacity.map_snd_pinDeclaration kindtheorem
    ∀ {ι : Type u_1} (g₀ : ι → ZMod 2) (l : List ι), List.map Prod.snd (List.map (fun i => ({i}, g₀ i)) l) = List.map g₀ l
    Used by
  74. DeclHiddenChannelCapacity.map_fst_pinDeclaration kindtheorem
    ∀ {ι : Type u_1} (g₀ : ι → ZMod 2) (l : List ι),
  List.map Prod.fst (List.map (fun i => ({i}, g₀ i)) l) = List.map (fun x => {x}) l
    Used by
  75. DeclHiddenChannelCapacity.affLocal_nonemptyDeclaration kindtheorem

    Every local relation of a coherent system is nonempty.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V : Finset ι} {𝒲 : Finset (Finset ι)} {c : Finset ι → ZMod 2},
  HiddenChannelCapacity.CoherentAt 𝒲 c V → (HiddenChannelCapacity.affLocal V 𝒲 c).rel.Nonempty
    HiddenChannelCapacity.CoherentAtHiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.affLocalHiddenChannelCapacity.hostedListHiddenChannelCapacity.parityOnHiddenChannelCapacity.wsum
    Uses
    Used by
  76. DeclHiddenChannelCapacity.wsum_restrictDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V w : Finset ι},
  w ⊆ V → ∀ (f : ι → ZMod 2), HiddenChannelCapacity.wsum V w (V.restrict f) = HiddenChannelCapacity.parityOn w f
    HiddenChannelCapacity.parityOnHiddenChannelCapacity.wsum
    Used by
  77. DeclHiddenChannelCapacity.sysCoherent_hostedListDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V : Finset ι} {𝒲 : Finset (Finset ι)} {c : Finset ι → ZMod 2},
  HiddenChannelCapacity.CoherentAt 𝒲 c V → HiddenChannelCapacity.SysCoherent (HiddenChannelCapacity.hostedList✝ V 𝒲 c)
    HiddenChannelCapacity.CoherentAtHiddenChannelCapacity.SysCoherentHiddenChannelCapacity.hostedListHiddenChannelCapacity.xorSumHiddenChannelCapacity.xorSumL
    Uses
    Used by
  78. DeclHiddenChannelCapacity.xorSumL_eq_xorSumDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {l : List (Finset ι)},
  l.Nodup → HiddenChannelCapacity.xorSumL l = HiddenChannelCapacity.xorSum l.toFinset
    HiddenChannelCapacity.xorSumHiddenChannelCapacity.xorSumL
    Uses
    Used by
  79. DeclHiddenChannelCapacity.map_snd_pairDeclaration kindtheorem
    ∀ {ι : Type u_1} (c : Finset ι → ZMod 2) (l : List (Finset ι)),
  List.map Prod.snd (List.map (fun w => (w, c w)) l) = List.map c l
    Used by
  80. DeclHiddenChannelCapacity.map_fst_pairDeclaration kindtheorem
    ∀ {ι : Type u_1} (c : Finset ι → ZMod 2) (l : List (Finset ι)), List.map Prod.fst (List.map (fun w => (w, c w)) l) = l
    Used by
  81. DeclHiddenChannelCapacity.mem_affLocal_relDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] {V : Finset ι} {𝒲 : Finset (Finset ι)} {c : Finset ι → ZMod 2}
  {F : ↥V → ZMod 2},
  F ∈ (HiddenChannelCapacity.affLocal V 𝒲 c).rel ↔ ∀ w ∈ 𝒲, w ⊆ V → HiddenChannelCapacity.wsum V w F = c w
    HiddenChannelCapacity.LocalStruct.relHiddenChannelCapacity.LocalStruct.teamHiddenChannelCapacity.affLocalHiddenChannelCapacity.wsum
    Used by
  82. DeclHiddenChannelCapacity.exists_parity_solutionDeclaration kindtheorem

    The solvability core: a coherent list-presented parity system has a solution. Elementary Gaussian elimination, by induction on the list.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (L : List (Finset ι × ZMod 2)),
  HiddenChannelCapacity.SysCoherent L → ∃ f, ∀ p ∈ L, HiddenChannelCapacity.parityOn p.1 f = p.2
    HiddenChannelCapacity.SysCoherentHiddenChannelCapacity.parityOnHiddenChannelCapacity.xorSumL
    Uses
    Used by
  83. DeclHiddenChannelCapacity.xorSumL_consDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (w : Finset ι) (l : List (Finset ι)),
  HiddenChannelCapacity.xorSumL (w :: l) = symmDiff w (HiddenChannelCapacity.xorSumL l)
    HiddenChannelCapacity.xorSumL
    Used by
  84. DeclHiddenChannelCapacity.transform_bookkeepingDeclaration kindtheorem

    The Gaussian transform bookkeeping: transforming the x-containing entries by ∆ w₀ shifts the F2 sum by w₀ per transformed entry, and the constants by c₀ likewise.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (x : ι) (w₀ : Finset ι) (c₀ : ZMod 2) (sub : List (Finset ι × ZMod 2)),
  HiddenChannelCapacity.xorSumL
        (List.map Prod.fst (List.map (fun p => if x ∈ p.1 then (symmDiff p.1 w₀, p.2 + c₀) else p) sub)) =
      symmDiff (HiddenChannelCapacity.xorSumL (List.map Prod.fst sub))
        (if List.countP (fun p => decide (x ∈ p.1)) sub % 2 = 1 then w₀ else ∅) ∧
    (List.map Prod.snd (List.map (fun p => if x ∈ p.1 then (symmDiff p.1 w₀, p.2 + c₀) else p) sub)).sum =
      (List.map Prod.snd sub).sum + if List.countP (fun p => decide (x ∈ p.1)) sub % 2 = 1 then c₀ else 0
    HiddenChannelCapacity.xorSumL
    Uses
    Used by
  85. DeclHiddenChannelCapacity.symmDiff_emptyDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (a : Finset ι), symmDiff a ∅ = a
    Used by
  86. DeclHiddenChannelCapacity.parityOn_symmDiffDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (w w' : Finset ι) (f : ι → ZMod 2),
  HiddenChannelCapacity.parityOn (symmDiff w w') f =
    HiddenChannelCapacity.parityOn w f + HiddenChannelCapacity.parityOn w' f
    HiddenChannelCapacity.parityOn
    Uses
    Used by
  87. DeclHiddenChannelCapacity.zmod2_add_selfDeclaration kindtheorem
    ∀ (a : ZMod 2), a + a = 0
    Used by
  88. DeclHiddenChannelCapacity.acyclic_iff_grahamReducibleDeclaration kindtheorem

    The Graham bridge: acyclicity is exactly Graham reducibility.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  HiddenChannelCapacity.Acyclic 𝒞 ↔ HiddenChannelCapacity.GrahamReducible 𝒞
    HiddenChannelCapacity.AcyclicHiddenChannelCapacity.GrahamNHiddenChannelCapacity.GrahamReducibleHiddenChannelCapacity.RIPCover
    Uses
    Used by
  89. DeclHiddenChannelCapacity.grahamN_of_ripCoverDeclaration kindtheorem

    An RIP order eliminates from the front: its head is an ear and the tail remains RIP.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (order : List (Finset ι)),
  order.Nodup → HiddenChannelCapacity.RIPCover order → HiddenChannelCapacity.GrahamN order.length order.toFinset
    HiddenChannelCapacity.GrahamNHiddenChannelCapacity.IsEarOfHiddenChannelCapacity.RIPCoverHiddenChannelCapacity.coverUHiddenChannelCapacity.listCover
    Uses
    Used by
  90. DeclHiddenChannelCapacity.exists_ripCover_of_grahamNDeclaration kindtheorem

    An elimination run is a running-intersection order read forward.

    ∀ {ι : Type u_1} [inst : DecidableEq ι] (n : ℕ) (𝒞 : Finset (Finset ι)),
  HiddenChannelCapacity.GrahamN n 𝒞 → ∃ order, order.Nodup ∧ order.toFinset = 𝒞 ∧ HiddenChannelCapacity.RIPCover order
    HiddenChannelCapacity.GrahamNHiddenChannelCapacity.IsEarOfHiddenChannelCapacity.RIPCoverHiddenChannelCapacity.coverUHiddenChannelCapacity.listCover
    Uses
    Used by
  91. DeclHiddenChannelCapacity.listCover_eq_coverUDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List (Finset ι)),
  HiddenChannelCapacity.listCover l = HiddenChannelCapacity.coverU l.toFinset
    HiddenChannelCapacity.coverUHiddenChannelCapacity.listCover
    Used by
  92. DefinitionHiddenChannelCapacity.Acyclicdef

    Order-free acyclicity: some duplicate-free enumeration of the cover is a running-intersection order.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Prop
  93. DefinitionHiddenChannelCapacity.Adjdef

    Primal adjacency: distinct co-hosted vertices.

    {ι : Type u_1} → Finset (Finset ι) → ι → ι → Prop
  94. DefinitionHiddenChannelCapacity.ClosedAtdef

    Intra-team span closure: subset sums of the constraints hosted by V vanish or stay in the system.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Finset ι → Prop
  95. DefinitionHiddenChannelCapacity.CoherentAtdef

    Intra-team coherence: constants vanish on the dependencies hosted by V.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → (Finset ι → ZMod 2) → Finset ι → Prop
  96. DefinitionHiddenChannelCapacity.Conformaldef

    Conformality: every clique inside the cover is covered.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Prop
  97. DefinitionHiddenChannelCapacity.Consistentdef

    Pairwise consistency: any two members expose the same interface marginal.

    {ι : Type u_1} →
  [DecidableEq ι] →
    {X : ι → Type u_2} → [(i : ι) → DecidableEq (X i)] → List (HiddenChannelCapacity.LocalStruct ι X) → Prop
  98. DefinitionHiddenChannelCapacity.Covereddef

    A vertex set covered by a single team.

    {ι : Type u_1} → Finset (Finset ι) → Finset ι → Prop
  99. DefinitionHiddenChannelCapacity.EarFreedef

    An ear-free nonempty cover: the stuck core condition.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Prop
  100. DefinitionHiddenChannelCapacity.Gluesdef

    Gluing: some global structure realizes every member exactly.

    {ι : Type u_1} →
  {X : ι → Type u_2} → [(i : ι) → DecidableEq (X i)] → [Fintype ι] → List (HiddenChannelCapacity.LocalStruct ι X) → Prop
  101. DefinitionHiddenChannelCapacity.GrahamNdef

    Nondeterministic ear elimination, fueled.

    {ι : Type u_1} → [DecidableEq ι] → ℕ → Finset (Finset ι) → Prop
  102. DefinitionHiddenChannelCapacity.GrahamReducibledef

    Graham reducibility: ear elimination empties the cover; the cover's size is fuel enough since every elimination removes exactly one team.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Prop
  103. DefinitionHiddenChannelCapacity.IsChordlessCycledef

    A chordless cycle: duplicate-free, length ≥ 4, consecutive pairs hosted, and the only adjacencies among its vertices are the cyclically consecutive ones.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → List ι → Prop
  104. DefinitionHiddenChannelCapacity.IsCliquedef

    A clique of the primal graph.

    {ι : Type u_1} → Finset (Finset ι) → Finset ι → Prop
  105. DefinitionHiddenChannelCapacity.IsEarOfdef

    The ear condition: the team meets the union of the others inside a single other team (or there are no others).

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Finset ι → Prop
  106. DefinitionHiddenChannelCapacity.IsWalkOndef

    A walk constrained to P: chained adjacencies, every vertex satisfies P.

    {ι : Type u_1} → Finset (Finset ι) → (ι → Prop) → List ι → Prop
  107. DefinitionHiddenChannelCapacity.LocalStructstructure

    A local structure: a team of parts together with an ignorance structure on the team's marginal type.

    (ι : Type u_3) → (ι → Type u_4) → Type (max u_3 u_4)
  108. DefinitionHiddenChannelCapacity.LocalStruct.imargdef

    The interface marginal of a local structure over a sub-team.

    {ι : Type u_1} →
  {X : ι → Type u_2} →
    [(i : ι) → DecidableEq (X i)] →
      (L : HiddenChannelCapacity.LocalStruct ι X) → {S : Finset ι} → S ⊆ L.team → Finset ((i : ↥S) → X ↑i)
  109. DefinitionHiddenChannelCapacity.LocalStruct.reldef

    The admissible local configurations.

    {ι : Type u_3} → {X : ι → Type u_4} → (self : HiddenChannelCapacity.LocalStruct ι X) → Finset ((i : ↥self.team) → X ↑i)
  110. DefinitionHiddenChannelCapacity.LocalStruct.teamdef

    The team of parts this local structure constrains.

    {ι : Type u_3} → {X : ι → Type u_4} → HiddenChannelCapacity.LocalStruct ι X → Finset ι
  111. DefinitionHiddenChannelCapacity.RIPdef

    Running intersection property: each member meets the union of the later members inside a single later member (the head is the last-eliminated team).

    {ι : Type u_1} → [DecidableEq ι] → {X : ι → Type u_2} → List (HiddenChannelCapacity.LocalStruct ι X) → Prop
  112. DefinitionHiddenChannelCapacity.RIPCoverdef

    Team-level running intersection property: each team meets the union of the later teams inside a single later team.

    {ι : Type u_1} → [DecidableEq ι] → List (Finset ι) → Prop
  113. DefinitionHiddenChannelCapacity.ReachOndef

    Reachability within P: a duplicate-free walk with the given endpoints.

    {ι : Type u_1} → Finset (Finset ι) → (ι → Prop) → ι → ι → Prop
  114. DefinitionHiddenChannelCapacity.SimpIndef

    v is simplicial within the vertex set S: it lies in S and its 𝒞-neighbors inside S are pairwise adjacent.

    {ι : Type u_1} → Finset (Finset ι) → Finset ι → ι → Prop
  115. DefinitionHiddenChannelCapacity.SysCoherentdef

    Coherence of a list-presented parity system: constants vanish on every dependency.

    {ι : Type u_1} → [DecidableEq ι] → List (Finset ι × ZMod 2) → Prop
  116. DefinitionHiddenChannelCapacity.affFamdef

    The affine family over a cover: every team with its fitting constraints.

    {ι : Type u_1} →
  [DecidableEq ι] →
    List (Finset ι) →
      Finset (Finset ι) → (Finset ι → ZMod 2) → List (HiddenChannelCapacity.LocalStruct ι fun x => ZMod 2)
  117. DefinitionHiddenChannelCapacity.affLocaldef

    The team V with every constraint of the system that fits inside it: the uniform replication rule.

    {ι : Type u_1} →
  [DecidableEq ι] →
    Finset ι → Finset (Finset ι) → (Finset ι → ZMod 2) → HiddenChannelCapacity.LocalStruct ι fun x => ZMod 2
  118. DefinitionHiddenChannelCapacity.coverUdef

    The union of a finite set of teams.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Finset ι
  119. DefinitionHiddenChannelCapacity.cyclePairsdef

    The consecutive-pair supports of a cyclic vertex list.

    {ι : Type u_1} → [DecidableEq ι] → List ι → List (Finset ι)
  120. DefinitionHiddenChannelCapacity.decidableAcyclicdef

    Acyclicity is decidable — the payoff of the bridge.

    {ι : Type u_1} → [inst : DecidableEq ι] → (𝒞 : Finset (Finset ι)) → Decidable (HiddenChannelCapacity.Acyclic 𝒞)
  121. DefinitionHiddenChannelCapacity.decidableIsEarOfdef
    {ι : Type u_1} →
  [inst : DecidableEq ι] → (𝒞 : Finset (Finset ι)) → (T : Finset ι) → Decidable (HiddenChannelCapacity.IsEarOf 𝒞 T)
  122. DefinitionHiddenChannelCapacity.famCoverdef

    The union of a family's teams.

    {ι : Type u_1} → [DecidableEq ι] → {X : ι → Type u_2} → List (HiddenChannelCapacity.LocalStruct ι X) → Finset ι
  123. DefinitionHiddenChannelCapacity.hostedListdef

    The hosted constraints of V, as a list system.

    {ι : Type u_1} → [DecidableEq ι] → Finset ι → Finset (Finset ι) → (Finset ι → ZMod 2) → List (Finset ι × ZMod 2)
  124. DefinitionHiddenChannelCapacity.instDecidableAdjdef
    {ι : Type u_1} → [DecidableEq ι] → (𝒞 : Finset (Finset ι)) → (u v : ι) → Decidable (HiddenChannelCapacity.Adj 𝒞 u v)
  125. DefinitionHiddenChannelCapacity.instDecidableCovereddef
    {ι : Type u_1} →
  [DecidableEq ι] → (𝒞 : Finset (Finset ι)) → (K : Finset ι) → Decidable (HiddenChannelCapacity.Covered 𝒞 K)
  126. DefinitionHiddenChannelCapacity.instDecidableIsCliquedef
    {ι : Type u_1} →
  [DecidableEq ι] → (𝒞 : Finset (Finset ι)) → (K : Finset ι) → Decidable (HiddenChannelCapacity.IsClique 𝒞 K)
  127. DefinitionHiddenChannelCapacity.joinFamdef

    The natural join of a family: all global configurations passing every local test.

    {ι : Type u_1} →
  [DecidableEq ι] →
    {X : ι → Type u_2} →
      [(i : ι) → DecidableEq (X i)] →
        [Fintype ι] → [(i : ι) → Fintype (X i)] → List (HiddenChannelCapacity.LocalStruct ι X) → Finset ((i : ι) → X i)
  128. DefinitionHiddenChannelCapacity.listCoverdef

    The union of a list of teams.

    {ι : Type u_1} → [DecidableEq ι] → List (Finset ι) → Finset ι
  129. DefinitionHiddenChannelCapacity.parityOndef

    Parity of a global configuration over a support.

    {ι : Type u_1} → Finset ι → (ι → ZMod 2) → ZMod 2
  130. DefinitionHiddenChannelCapacity.projSdef

    The marginal of a multipartite relation over a sub-team S: the image under Finset.restrict.

    {ι : Type u_1} →
  {X : ι → Type u_2} →
    [(i : ι) → DecidableEq (X i)] → Finset ((i : ι) → X i) → (S : Finset ι) → Finset ((i : ↥S) → X ↑i)
  131. DefinitionHiddenChannelCapacity.shareddef

    The shared vertices of a cover.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Finset ι
  132. DefinitionHiddenChannelCapacity.wsumdef

    Parity of a team configuration over the team part of a support.

    {ι : Type u_1} → [DecidableEq ι] → (V : Finset ι) → Finset ι → (↥V → ZMod 2) → ZMod 2
  133. DefinitionHiddenChannelCapacity.xorSumdef

    F2 sum of a finite collection of supports.

    {ι : Type u_1} → [DecidableEq ι] → Finset (Finset ι) → Finset ι
  134. DefinitionHiddenChannelCapacity.xorSumLdef

    F2 sum of a list of supports.

    {ι : Type u_1} → [DecidableEq ι] → List (Finset ι) → Finset ι
DOIMTH.R-2026-6019
Cite

Verification

Replay
accepted
Axioms
Classical.choiceQuot.soundpropext
Statement identity
not-applicable
Substrate
Lean 4 kernel v4.31.0
Dictionary pin
design-lab@5802df4 · initial
Frozen export
787331969522
Verified
2026-09-24T00:00:00Z