Dominance properties under the unique-heads constraint: parent-pointer tracing, iterParent chains, antisymmetry of dominance, and dominates_to_parent.

These results require hasUniqueHeads and/or isAcyclic from Basic.lean and the Dominates inductive + projection bridge theorems from Projection.lean.

def DepGrammar.parentOf_uh (t : DepTree) (x : ℕ) : ℕ

The unique parent of node x (follows find? on depIdx). Returns x if no parent.

Equations

• DepGrammar.parentOf_uh t x = match List.find? (fun (d : DepGrammar.Dependency) => d.depIdx == x) t.deps with | some d => d.headIdx | none => x

def DepGrammar.iterParent_uh (t : DepTree) (x : ℕ) : ℕ → ℕ

Iterate parentOf k times.

Equations

• DepGrammar.iterParent_uh t x 0 = x
• DepGrammar.iterParent_uh t x fuel'.succ = DepGrammar.parentOf_uh t (DepGrammar.iterParent_uh t x fuel')

theorem DepGrammar.parentOf_of_edge_uh (t : DepTree) (hwf : t.WF) {v c : ℕ} (hedge : ∃ (d : Dependency), d ∈ t.deps ∧ d.headIdx = v ∧ d.depIdx = c) : parentOf_uh t c = v

Under unique heads, if edge(v, c) exists, then parentOf c = v.

theorem DepGrammar.dominates_iterParent_uh (t : DepTree) (hwf : t.WF) {v w : ℕ} (hdom : Dominates t.deps v w) (hne : v ≠ w) : ∃ (k : ℕ), k > 0 ∧ iterParent_uh t w k = v ∧ ∀ (i : ℕ), i < k → ∃ (dep : Dependency), List.find? (fun (d : Dependency) => d.depIdx == iterParent_uh t w i) t.deps = some dep ∧ dep.headIdx = iterParent_uh t w (i + 1)

Under unique heads, Dominates v w with v ≠ w implies the iterParent chain from w reaches v, with valid parent edges at each step.

theorem DepGrammar.iterParent_chain_bound (t : DepTree) (hacyc : isAcyclic t = true) (h_dep_wf : ∀ (d : Dependency), d ∈ t.deps → d.depIdx < t.words.length) (start k : ℕ) (hchain : ∀ (i : ℕ), i < k → ∃ (dep : Dependency), List.find? (fun (d : Dependency) => d.depIdx == iterParent_uh t start i) t.deps = some dep ∧ dep.headIdx = iterParent_uh t start (i + 1)) (hstart_lt : start < t.words.length) : k ≤ t.words.length

The iterParent chain length from a dominance derivation is bounded by n.

If k > n, the first n+1 chain values are n+1 distinct values in [0, n). Distinctness: any duplicate at positions i < j ≤ n creates a sub-cycle of length j - i ≤ n, detectable by follow_false_of_cycle with fuel n + 1 ≥ j - i + 1. But isAcyclic = true, contradiction. Then nodup_bound gives n + 1 ≤ n, contradiction.

theorem DepGrammar.dominates_antisymm (t : DepTree) (hwf : t.WF) (hacyc : isAcyclic t = true) (v w : ℕ) (hvw : Dominates t.deps v w) (hwv : Dominates t.deps w v) : v = w

In a well-formed tree (unique heads + acyclic), dominance is antisymmetric: if v dominates w and w dominates v, then v = w.

Proof: By contradiction, assume v ≠ w. Extract iterParent chains from both Dominates derivations, combine into a cycle, and show isAcyclic.follow detects it (returning false), contradicting isAcyclic = true.

theorem DepGrammar.dominates_to_parent {deps : List Dependency} {v c a : ℕ} (hdom : Dominates deps v c) (hne : v ≠ c) (hparent : ∀ (d : Dependency), d ∈ deps → d.depIdx = c → d.headIdx = a) : Dominates deps v a

If v dominates c (with v ≠ c) and every edge into c has head = a, then v dominates a.

Key proof technique: induction on the Dominates derivation. The last edge in the path v →... → c terminates at c, so its head endpoint must be c's unique parent a. Dropping this last edge gives v dominates a.

Used in projective_implies_planar to extract dominance cycles from crossing edges under unique heads.