Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

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

Arguments

DOI	Author	Date
MTH.R-2026-6019	Dhruv Gupta	2026-09-24T00:00:00Z

DOIMTH.C-2026-6019

Cite

Verification

Library: ZPM.Measurements.HC.Dirac
Statement digest: 64ea316dd7aa
First verified: 2026-09-24T00:00:00Z