/-
  Blueskyisms.lean — a formalization of the Tractatus Logico-Blueskyicus.
  Generated by gen-lean.mjs from data/propositions.json. Core Lean 4, no Mathlib.

  Each proposition is its index in `nums`. An edge (a, b) in `supports` reads
  "a supports b". Every theorem below is a closed computation on a finite graph,
  so `decide` closes it.
-/

namespace Blueskyisms

/-- Proposition numbers, in the order of the book. -/
def nums : List String := [
  "1",
  "1.1",
  "1.2",
  "2",
  "2.1",
  "2.1.1",
  "2.1.2",
  "2.2",
  "2.3",
  "2.3.1",
  "3",
  "4",
  "5",
  "5.1",
  "6",
  "6.1",
  "7",
  "7.1",
  "8",
  "8.1",
  "8.2",
  "9",
  "10",
  "11",
  "12",
  "13",
  "13.1",
  "14",
  "15",
  "16"
]

def supports : List (Nat × Nat) := [(1, 0), (2, 0), (3, 0), (4, 3), (5, 4), (7, 3), (8, 3), (9, 8), (10, 11), (11, 10), (12, 14), (13, 12), (18, 3), (19, 18), (21, 3), (22, 2), (23, 8), (24, 9), (28, 0), (29, 0)]
def tensions : List (Nat × Nat) := [(4, 10), (7, 2), (11, 2), (13, 1), (14, 1), (17, 16), (21, 12), (22, 17), (25, 11), (27, 7)]
def qualifies : List (Nat × Nat) := [(6, 4), (8, 12), (15, 14), (16, 2), (20, 18), (26, 25), (28, 8)]

/-- Remove duplicates, keeping first occurrences. -/
def dedup (xs : List Nat) : List Nat :=
  xs.foldl (fun acc x => if acc.contains x then acc else acc ++ [x]) []

/-- One round of following `supports` edges outward from a set. -/
def step (s : List Nat) : List Nat :=
  dedup (s ++ supports.filterMap fun (e : Nat × Nat) => if s.contains e.1 then some e.2 else none)

/-- Iterate `step`. The graph has 30 nodes, so 30 rounds always reach the fixpoint. -/
def closure : Nat → List Nat → List Nat
  | 0, s => s
  | n + 1, s => closure n (step s)

/-- `reaches a b`: a chain of supports leads from a to b. -/
def reaches (a b : Nat) : Bool := (closure 30 [a]).contains b

/-- Proposition 1, "The timeline is everything that suffers", is the root. -/
def root : Nat := 0

/-- A proposition is grounded when a chain of supports leads to the root. -/
def grounded (a : Nat) : Bool := reaches a root

/-- The root has no outgoing support: nothing holds it up. -/
theorem root_unsupported : supports.filter (fun e => e.1 == root) = [] := by decide

/-- Exactly these propositions are grounded in 1. -/
theorem grounded_set :
    (List.range 30).filter grounded = [0, 1, 2, 3, 4, 5, 7, 8, 9, 18, 19, 21, 22, 23, 24, 28, 29] := by decide

/-- Exactly these propositions are never grounded: their support runs into a dead end. -/
theorem ungrounded_set :
    (List.range 30).filter (fun a => !grounded a) = [6, 10, 11, 12, 13, 14, 15, 16, 17, 20, 25, 26, 27] := by decide

/-- 6 (The Discourse Cycle) is not grounded: the chain from it never touches the root. -/
theorem discourse_ungrounded : grounded 14 = false := by decide

/-- Mutual support, no way out: 3, 4 support each other in a loop. -/
theorem circular_set :
    (List.range 30).filter (fun a =>
      (List.range 30).any fun b => a != b && reaches a b && reaches b a) = [10, 11] := by decide

/-- The Circular Citation, formally: 3 and 4 each support the other. -/
theorem circular_citation : reaches 10 11 = true ∧ reaches 11 10 = true := by decide

/-- The ontology is not a tree: 30 propositions, 20 supports, 10 tensions, 7 qualifications. -/
theorem sizes : nums.length = 30 ∧ supports.length = 20 ∧ tensions.length = 10 ∧ qualifies.length = 7 := by decide

end Blueskyisms