Bridge: SynObj → SynGraph

@cite{adger-2025}

Embeds tree-based syntactic objects (SynObj) into graph-based structures (SynGraph MLabel), making SynGraph the canonical operational type for Angular Locality while preserving SynObj as an ergonomic builder.

SynObj is an inductive type that gives structural recursion and rfl proofs — useful for tree-shaped work (classifier hierarchies, basic clause structure). SynGraph supports multiparthood (unbounded in-degree), required for movement in mereological syntax. The embedding connects them: build with SynObj, convert to SynGraph when you need AL, movement, or island constraints.

Pre-order Indexing

The embedding assigns node indices via pre-order traversal:

• Root = 0
• 1-part subtree: indices [1, 1 + onePart.size)
• 2-part subtree: indices [1 + onePart.size, size)

Key Results

• toSynGraph: embeds any SynObj as a SynGraph MLabel
• isTree verified on all test structures
• compLine agrees with onePartChain
• angularLocalityOK (tree, label-based) agrees with satisfiesAL (graph, index-based) — verified on the critical cross-dimensional structure from @cite{adger-2025} p. 95

def MereologicalSyntax.SynObj.size : SynObj → ℕ

Number of nodes in a SynObj tree.

Equations

• (MereologicalSyntax.SynObj.leaf a).size = 1
• (MereologicalSyntax.SynObj.sub₁ a one).size = 1 + one.size
• (MereologicalSyntax.SynObj.sub₁₂ a one two).size = 1 + one.size + two.size

theorem MereologicalSyntax.SynObj.size_pos (t : SynObj) : 0 < t.size

def MereologicalSyntax.SynObj.toSynGraphAux : SynObj → { g : SynGraph MLabel // 0 < g.numNodes }

Embed a SynObj tree into a SynGraph MLabel, with a proof that numNodes > 0. Used by toSynGraph which extracts the graph.

Equations

• One or more equations did not get rendered due to their size.
• (MereologicalSyntax.SynObj.leaf a).toSynGraphAux = ⟨{ numNodes := 1, label := fun (x : Fin 1) => a, onePart := fun (x : Fin 1) => none, twoPart := fun (x : Fin 1) => none }, Nat.one_pos⟩

def MereologicalSyntax.SynObj.toSynGraph (t : SynObj) : SynGraph MLabel

Embed a SynObj tree into a SynGraph MLabel.

Node indexing follows pre-order: root = 0, then 1-part subtree, then 2-part subtree. The result satisfies isTree (acyclic, in-degree ≤ 1).

The definition is compositional: each case builds the graph from subgraphs, making structural induction possible.

Equations

• t.toSynGraph = ↑t.toSynGraphAux

theorem MereologicalSyntax.SynObj.toSynGraph_pos (t : SynObj) : 0 < t.toSynGraph.numNodes

def MereologicalSyntax.SynObj.alOK_via_graph (l : MLabel) (t : SynObj) : Bool

Angular Locality check via the graph representation: does any node with label l satisfy satisfiesAL for the root (node 0)?

This is the existential analogue of satisfiesAL that operates on labels rather than node indices, making it directly comparable to the tree-based angularLocalityOK.

Equations

• One or more equations did not get rendered due to their size.

theorem MereologicalSyntax.antilocal_al_agrees : angularLocalityOK MLabel.N MereologicalSyntax.t_antilocal✝ = SynObj.alOK_via_graph MLabel.N MereologicalSyntax.t_antilocal✝¹

theorem MereologicalSyntax.antilocal_isTree : MereologicalSyntax.t_antilocal✝.toSynGraph.isTree = true

theorem MereologicalSyntax.rollup_2part_agrees : angularLocalityOK MLabel.D MereologicalSyntax.t_rollup✝ = SynObj.alOK_via_graph MLabel.D MereologicalSyntax.t_rollup✝¹

theorem MereologicalSyntax.rollup_1part_agrees : angularLocalityOK MLabel.V MereologicalSyntax.t_rollup✝ = SynObj.alOK_via_graph MLabel.V MereologicalSyntax.t_rollup✝¹

theorem MereologicalSyntax.rollup_isTree : MereologicalSyntax.t_rollup✝.toSynGraph.isTree = true

theorem MereologicalSyntax.rollup_compLine : MereologicalSyntax.t_rollup✝.compLine = MereologicalSyntax.t_rollup✝¹.toSynGraph.onePartChain ⟨0, ⋯⟩

theorem MereologicalSyntax.crossdim_allows_agrees : angularLocalityOK MLabel.D MereologicalSyntax.t_crossdim✝ = SynObj.alOK_via_graph MLabel.D MereologicalSyntax.t_crossdim✝¹

theorem MereologicalSyntax.crossdim_blocks_agrees : angularLocalityOK MLabel.N MereologicalSyntax.t_crossdim✝ = SynObj.alOK_via_graph MLabel.N MereologicalSyntax.t_crossdim✝¹

theorem MereologicalSyntax.crossdim_isTree : MereologicalSyntax.t_crossdim✝.toSynGraph.isTree = true

theorem MereologicalSyntax.crossdim_compLine : MereologicalSyntax.t_crossdim✝.compLine = MereologicalSyntax.t_crossdim✝¹.toSynGraph.onePartChain ⟨0, ⋯⟩

theorem MereologicalSyntax.classifier_compLine : MereologicalSyntax.t_classifier✝.compLine = MereologicalSyntax.t_classifier✝¹.toSynGraph.onePartChain ⟨0, ⋯⟩

theorem MereologicalSyntax.classifier_isTree : MereologicalSyntax.t_classifier✝.toSynGraph.isTree = true

theorem MereologicalSyntax.al_bridge (t : SynObj) (l : MLabel) : angularLocalityOK l t = SynObj.alOK_via_graph l t

The tree-based Angular Locality check agrees with the graph-based version on all SynObj trees: angularLocalityOK l t returns the same answer as the existential check "does any node with label l satisfy satisfiesAL in the embedded graph?"

Proved by induction on SynObj, showing that the pre-order embedding preserves within-dimension chains.