other

PAC

Lean spine source

Declarations: P33_no_open_edges_no_large_component, inferentialEdgeOpen

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P33_no_open_edges_no_large_component {V : Type}
    (G : CooperationGraph V) (hclosed : ∀ i j, ¬ G.Open i j) :
    ¬ G.componentLarge := by
  rintro ⟨i, j, hopen⟩
  exact hclosed i j hopen

def inferentialEdgeOpen (score threshold : Int) : Prop :=
  threshold < score