other

Inferential/UAD graph certificates UAD audit + P_meta + IC score

Lean spine source

formal/AlignmentProofSpine/CooperationGraph.lean

Declarations: P33_no_open_edges_no_large_component, inferentialEdgeOpen

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). 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