-- ============================================================================
-- Section 5.5: Absorbing Boundary & Topological Scar Permanence
-- Standalone Lean 4 Core Formalization (Zero Axioms, Zero External Dependencies)
-- ============================================================================

def Edge (V : Type) := V × V

def GraphEdges (V : Type) := Edge V → Prop

def InAny3Cycle {V : Type} (E : GraphEdges V) (e : Edge V) : Prop :=
  ∃ u v w : V, E (u, v) ∧ E (v, w) ∧ E (w, u) ∧ 
  (e = (u, v) ∨ e = (v, w) ∨ e = (w, u))

def IsScarEdge {V : Type} (E : GraphEdges V) (e : Edge V) : Prop :=
  E e ∧ ¬ InAny3Cycle E e

def LegalDeletionGrammar {V : Type} (E : GraphEdges V) (D : GraphEdges V) : Prop :=
  ∀ e, D e → InAny3Cycle E e

def IsAbsorbingConfiguration {V : Type} (A_edges D : GraphEdges V) : Prop :=
  (∀ e, ¬ A_edges e) ∧ (∀ e, ¬ D e)

/--
THEOREM 1: Absorbing State Stationarity
Proves that when both proposal sets vanish (A = ∅ and D = ∅), the transition
operator reduces strictly to the identity map: E_{t+1} = E_t.
-/
theorem absorbing_state_stationary {V : Type}
    (E A_edges D : GraphEdges V)
    (h_abs : IsAbsorbingConfiguration A_edges D) :
    ∀ e, ((E e ∨ A_edges e) ∧ ¬ (D e)) ↔ E e := by
  intro e
  rcases h_abs with ⟨hA, hD⟩
  constructor
  · intro ⟨h_or, _⟩
    cases h_or with
    | inl hE => exact hE
    | inr heA => exact False.elim (hA e heA)
  · intro hE
    refine ⟨Or.inl hE, hD e⟩

/--
THEOREM 2: Move Grammar Enforces Scar Immunity
Proves that any scar edge (an edge not in any 3-cycle) is mathematically excluded
from the legal deletion proposal set D under the Move Grammar rule.
-/
theorem scar_edges_immune_to_deletion {V : Type}
    (E D : GraphEdges V)
    (h_grammar : LegalDeletionGrammar E D)
    (e : Edge V)
    (h_scar : IsScarEdge E e) :
    ¬ D e := by
  intro hD
  have h_in_cycle := h_grammar e hD
  exact h_scar.2 h_in_cycle

/--
THEOREM 3: Acyclic DAG Deletion Quiescence
Proves that on any Directed Acyclic Graph containing zero 3-cycles, the legal deletion set is empty (D = ∅).
-/
theorem acyclic_dag_deletion_empty {V : Type}
    (E D : GraphEdges V)
    (h_grammar : LegalDeletionGrammar E D)
    (h_dag : ∀ e, ¬ InAny3Cycle E e) :
    ∀ e, ¬ D e := by
  intro e hD
  have h_in := h_grammar e hD
  exact h_dag e h_in

/--
THEOREM 4: Monotone Subgraph Expansion Under Acyclic Evolution
Proves that when deletions are quiescent on a DAG, the scheduler transition
is an exact monotonic subgraph expansion: E_t ⊆ E_{t+1}.
-/
theorem acyclic_scheduler_monotonic_expansion {V : Type}
    (E A_edges D : GraphEdges V)
    (h_grammar : LegalDeletionGrammar E D)
    (h_dag : ∀ e, ¬ InAny3Cycle E e) :
    ∀ e, E e → ((E e ∨ A_edges e) ∧ ¬ D e) := by
  intro e he
  have h_not_D : ¬ D e := acyclic_dag_deletion_empty E D h_grammar h_dag e
  exact ⟨Or.inl he, h_not_D⟩

/--
THEOREM 5: Inductive Multi-Tick Scar Permanence
Proves that if an edge is never in a 3-cycle across an arbitrary sequence of ticks
under the deletion grammar, the edge persists indefinitely.
-/
theorem scar_multi_tick_induction {V : Type}
    (E_seq : Nat → GraphEdges V)
    (D_seq : Nat → GraphEdges V)
    (A_seq : Nat → GraphEdges V)
    (h_step : ∀ t e, E_seq (t + 1) e ↔ (E_seq t e ∨ A_seq t e) ∧ ¬ D_seq t e)
    (h_del_rule : ∀ t, LegalDeletionGrammar (E_seq t) (D_seq t))
    (e : Edge V)
    (h_never_in_cycle : ∀ t, ¬ InAny3Cycle (E_seq t) e)
    (h_init : E_seq 0 e) :
    ∀ t, E_seq t e := by
  intro t
  induction t with
  | zero => exact h_init
  | succ n ih =>
    rw [h_step n e]
    refine ⟨Or.inl ih, ?_⟩
    intro hD
    have h_in := (h_del_rule n) e hD
    exact (h_never_in_cycle n) h_in