-- ============================================================================
-- Section 4.6: Kinematics & Evolution Operator Confluence
-- Standalone Lean 4 Core Formalization (Zero Axioms, Zero External Dependencies)
-- ============================================================================

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

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

-- Representing addition and deletion edge subsets as predicates over directed pairs
def IsLegalAdditionSet {V : Type} (E A_edges : Edge V → Prop) : Prop :=
  ∀ e, A_edges e → ¬ (E e)

def IsLegalDeletionSet {V : Type} (E D : Edge V → Prop) : Prop :=
  ∀ e, D e → E e

/--
THEOREM 1: Dynamic Move Disjointness
Proves that the set of accepted additions and accepted deletions generated
within the same parallel tick are strictly disjoint: A_edges ∩ D = ∅.
-/
theorem dynamic_move_disjointness {V : Type}
    (E A_edges D : Edge V → Prop)
    (hA : IsLegalAdditionSet E A_edges)
    (hD : IsLegalDeletionSet E D) :
    ∀ e, ¬ (A_edges e ∧ D e) := by
  intro e ⟨heA, heD⟩
  have h_not_in_E : ¬ (E e) := hA e heA
  have h_in_E : E e := hD e heD
  exact h_not_in_E h_in_E

/--
THEOREM 2: Deterministic Race-Free Invariance
Proves that in the four-step parallel scheduler (merge additions into E' = E ∪ A_edges,
then apply deletions E_{t+1} = E' \ D), every newly added edge strictly survives deletion
within the same tick: ∀ e, A_edges e → ((E e ∨ A_edges e) ∧ ¬ (D e)).
-/
theorem dynamic_race_free_invariance {V : Type}
    (E A_edges D : Edge V → Prop)
    (hA : IsLegalAdditionSet E A_edges)
    (hD : IsLegalDeletionSet E D) :
    ∀ e, A_edges e → ((E e ∨ A_edges e) ∧ ¬ (D e)) := by
  intro e heA
  constructor
  · exact Or.inr heA
  · intro heD
    have h_disjoint := dynamic_move_disjointness E A_edges D hA hD e
    exact h_disjoint ⟨heA, heD⟩

-- Step 3 Addition Merging Algebra
def merge_edge {V : Type} (E : GraphEdges V) (e : Edge V) : GraphEdges V :=
  fun x => E x ∨ x = e

/--
THEOREM 3: Parallel Edge Merging Commutes
Proves that concurrent edge additions can be accumulated in arbitrary sequence
without altering the resulting intermediate topology G'.
-/
theorem parallel_addition_commutes {V : Type} 
    (E : GraphEdges V) (e1 e2 : Edge V) :
    merge_edge (merge_edge E e1) e2 = merge_edge (merge_edge E e2) e1 := by
  funext x
  dsimp [merge_edge]
  apply propext
  constructor
  · intro h
    rcases h with (hE | he1) | he2
    · exact Or.inl (Or.inl hE)
    · exact Or.inr he1
    · exact Or.inl (Or.inr he2)
  · intro h
    rcases h with (hE | he2) | he1
    · exact Or.inl (Or.inl hE)
    · exact Or.inr he2
    · exact Or.inl (Or.inr he1)

/--
THEOREM 4: Parallel Edge Merging is Idempotent
Proves that duplicate proposals targeting the same edge fold idempotently.
-/
theorem parallel_addition_idempotent {V : Type} 
    (E : GraphEdges V) (e : Edge V) :
    merge_edge (merge_edge E e) e = merge_edge E e := by
  funext x
  dsimp [merge_edge]
  apply propext
  constructor
  · intro h
    rcases h with (hE | he1) | he2
    · exact Or.inl hE
    · exact Or.inr he1
    · exact Or.inr he2
  · intro h
    rcases h with hE | he
    · exact Or.inl (Or.inl hE)
    · exact Or.inr he