def HexRootsMathlib.Glue.Edge (s t : Hex.DyadicSquare) : Prop

The exact edge relation used by the executable gluer.

Equations

• HexRootsMathlib.Glue.Edge s t = (s.adjacent t = true)

def HexRootsMathlib.Glue.Linked (s t : Hex.DyadicSquare) : Prop

Undirected executable edge adjacency.

Equations

• HexRootsMathlib.Glue.Linked s t = (HexRootsMathlib.Glue.Edge s t ∨ HexRootsMathlib.Glue.Edge t s)

theorem HexRootsMathlib.Glue.linked_symm {s t : Hex.DyadicSquare} : Linked s t → Linked t s

Undirected adjacency is symmetric.

theorem HexRootsMathlib.Glue.edge_refl (s : Hex.DyadicSquare) : Edge s s

Executable adjacency is reflexive: a square is adjacent to itself.

theorem HexRootsMathlib.Glue.nodup_glueList (squares : List Hex.DyadicSquare) : (Hex.glueList squares).Nodup

The outer connected-component list produced by the gluer has no duplicate component values.

def HexRootsMathlib.Glue.Connected (component : List Hex.DyadicSquare) : Prop

Every predicate invariant across internal adjacency edges is constant on the component. This induced-graph formulation records that paths stay inside the component, which is exactly what downstream semantic propagation needs.

Equations

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

def HexRootsMathlib.Glue.Separated (components : List (List Hex.DyadicSquare)) : Prop

Distinct components have no executable adjacency edge in either direction. Together with coverage and connectedness this is maximality.

Equations

• HexRootsMathlib.Glue.Separated components = ∀ c ∈ components, ∀ d ∈ components, c ≠ d → ∀ s ∈ c, ∀ t ∈ d, ¬HexRootsMathlib.Glue.Edge s t ∧ ¬HexRootsMathlib.Glue.Edge t s

theorem HexRootsMathlib.Glue.touches_iff {s : Hex.DyadicSquare} {component : List Hex.DyadicSquare} : s.touches component = true ↔ ∃ t ∈ component, Linked s t

The executable touches test is adjacency to some member.

theorem HexRootsMathlib.Glue.not_touches_iff {s : Hex.DyadicSquare} {component : List Hex.DyadicSquare} : s.touches component = false ↔ ∀ t ∈ component, ¬Edge s t ∧ ¬Edge t s

A failed touches test is two-sided non-adjacency to every member.

theorem HexRootsMathlib.Glue.connected_glueInsert {s : Hex.DyadicSquare} {components : List (List Hex.DyadicSquare)} (hconnected : ∀ c ∈ components, Connected c) (c : List Hex.DyadicSquare) : c ∈ Hex.glueInsert s components → Connected c

Inserting a square preserves connectedness of every component.

theorem HexRootsMathlib.Glue.connected_glueList (squares c : List Hex.DyadicSquare) : c ∈ Hex.glueList squares → Connected c

Every component returned by glueList is edge-connected.

theorem HexRootsMathlib.Glue.separated_glueInsert {s : Hex.DyadicSquare} {components : List (List Hex.DyadicSquare)} (hseparated : Separated components) : Separated (Hex.glueInsert s components)

Inserting a square preserves the absence of cross-component edges.

theorem HexRootsMathlib.Glue.separated_glueList (squares : List Hex.DyadicSquare) : Separated (Hex.glueList squares)

Distinct components returned by glueList have no edge between them.

theorem HexRootsMathlib.flatten_glueInsert_perm (s : Hex.DyadicSquare) (components : List (List Hex.DyadicSquare)) : (Hex.glueInsert s components).flatten.Perm (s :: components.flatten)

Inserting one square into a partial component partition preserves the flattened multiset, up to order.

theorem HexRootsMathlib.flatten_glueList_perm (squares : List Hex.DyadicSquare) : (Hex.glueList squares).flatten.Perm squares

glueList is a partition of the input list at the multiset level.

theorem HexRootsMathlib.flatten_glue_perm (squares : Array Hex.DyadicSquare) : (List.map Array.toList (Hex.glue squares).toList).flatten.Perm squares.toList

The executable array gluer preserves its input multiset exactly.

theorem HexRootsMathlib.mem_glue {squares : Array Hex.DyadicSquare} {s : Hex.DyadicSquare} (hs : s ∈ squares.toList) : ∃ c ∈ (Hex.glue squares).toList, s ∈ c.toList

Every input square occurs in an output component of glue.

theorem HexRootsMathlib.glueCovered_eq_glue (squares : Array Hex.DyadicSquare) : Hex.glueCovered squares = Hex.glue squares

The defensive branch of glueCovered is unreachable: the structurally recursive gluer already preserves every input member.

theorem HexRootsMathlib.glueCovered_nodup (squares : Array Hex.DyadicSquare) : (Hex.glueCovered squares).toList.Nodup

The guarded array gluer has no duplicate outer components.

theorem HexRootsMathlib.flatten_glueCovered_perm (squares : Array Hex.DyadicSquare) : (List.map Array.toList (Hex.glueCovered squares).toList).flatten.Perm squares.toList

The guarded gluer preserves the input multiset exactly.

theorem HexRootsMathlib.mem_of_mem_glueCovered {squares component : Array Hex.DyadicSquare} {s : Hex.DyadicSquare} (hc : component ∈ (Hex.glueCovered squares).toList) (hs : s ∈ component.toList) : s ∈ squares.toList

Every member of an output component came from the input array.

theorem HexRootsMathlib.glueCovered_nodup_disjoint {squares : Array Hex.DyadicSquare} (h : squares.toList.Nodup) : (∀ c ∈ (Hex.glueCovered squares).toList, c.toList.Nodup) ∧ List.Pairwise (fun (c d : Array Hex.DyadicSquare) => c.toList.Disjoint d.toList) (Hex.glueCovered squares).toList

Duplicate-free input gives duplicate-free, pairwise-disjoint output components.

theorem HexRootsMathlib.glueCovered_connected (squares c : Array Hex.DyadicSquare) : c ∈ (Hex.glueCovered squares).toList → Glue.Connected c.toList

Every guarded output component is edge-connected.

theorem HexRootsMathlib.glueCovered_separated (squares c : Array Hex.DyadicSquare) : c ∈ (Hex.glueCovered squares).toList → ∀ d ∈ (Hex.glueCovered squares).toList, c ≠ d → ∀ s ∈ c.toList, ∀ t ∈ d.toList, ¬Glue.Edge s t ∧ ¬Glue.Edge t s

Distinct guarded output components have no adjacency edge between any pair of their members, the maximality half of the gluing contract.