1Lean 4 formalization: contingent. elan/lake are not installed and the network allowlist may not permit the toolchain or Mathlib cache. Stage G makes one bounded attempt. Targets, in order: (F1) order independence of closure (P1), (F2) the 12-vertex upper-bound chronology for all n >= 12 (P7), (F3) the first-source boundary lemma (P8). If no toolchain is available this directory stays empty and the manuscript reports the formal scope as none.2