Spanning Tree Ontology

FLOW ALGEBRA
TITLE: Spanning Tree Ontology
DOMAIN: Discrete Mathematics / Graph Theory
SOURCE_URL: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/graph-theory/spanning-tree-ontology.html
VERSION: 1.0
LANGUAGE: en-GB
AUTHORS: Mark Higgins — Sky (Recursive AI)
SITE: https://kirethresearch.org
SOURCE_STATUS: Formal mathematical synthesis; live page not independently verified.

1. PURPOSE
Represent spanning trees as typed mathematical objects with explicit constraints, construction rules, optimisation criteria and machine-checkable validation.

2. TYPE SYSTEM
TYPE Vertex := hashable identifier
TYPE Edge := unordered pair of distinct Vertex identifiers
TYPE Graph := {V: Set[Vertex], E: Set[Edge]}
TYPE Tree := Graph satisfying connectedness and acyclicity
TYPE SpanningTree(G) := Tree T with V(T)=V(G) and E(T) subset_of E(G)
TYPE Weight := finite real number
TYPE WeightedGraph := (G, w: E(G) -> Weight)
TYPE Forest := acyclic undirected Graph
TYPE Certificate := {selected_edges, connectivity_witness, acyclicity_witness}

3. DEFINITIONS AND PRECONDITIONS
ASSUME finite, undirected, simple graph G=(V,E), unless explicitly overridden.
DEFINE connected(G) := every pair of vertices is joined by a path.
DEFINE acyclic(G) := G contains no cycle.
DEFINE spanning_tree(T,G) := V(T)=V(G) AND E(T) subset_of E(G) AND connected(T) AND acyclic(T).
DEFINE spanning_forest(F,G) := V(F)=V(G) AND E(F) subset_of E(G) AND acyclic(F) AND each component of G induces a spanning tree in F.
EXISTS spanning_tree(G) IFF connected(G), for finite undirected graphs (including the singleton graph).
CONVENTION empty graph has no spanning tree under the non-empty tree definition.

4. CORE FLOW OPERATIONS
FLOW CHECK_SPANNING_TREE(G,T):
  REQUIRE valid_graph(G) AND valid_graph(T)
  REQUIRE V(T)=V(G)
  REQUIRE E(T) subset_of E(G)
  RETURN connected(T) AND acyclic(T)

FLOW CONSTRUCT_SPANNING_TREE(G,start):
  REQUIRE connected(G) AND start in V(G)
  T := graph(vertices=V(G), edges={})
  visited := {start}
  frontier := [start]
  WHILE frontier not empty:
    u := remove_next(frontier)
    FOR each neighbour v of u in G:
      IF v not in visited:
        visited.add(v)
        T.edges.add({u,v})
        frontier.add(v)
  ENSURE spanning_tree(T,G)
  RETURN T
NOTE: queue gives breadth-first construction; stack gives depth-first construction.

FLOW MINIMUM_SPANNING_TREE(G,w):
  REQUIRE connected(G) AND every edge has a finite comparable weight
  SORT E(G) by nondecreasing weight; ties resolved deterministically
  T := (V(G),{})
  FOR e in sorted edges:
    IF endpoints(e) lie in distinct connected components of T:
      T.edges.add(e)
  ENSURE spanning_tree(T,G)
  ENSURE weight(T)=min{weight(S) : spanning_tree(S,G)}
  RETURN T
NOTE: Kruskal's algorithm; negative edge weights are permitted.

5. ALGEBRAIC LAWS AND INVARIANTS
LAW TREE_EDGE_COUNT: spanning_tree(T,G) => |E(T)|=|V(G)|-1.
LAW UNIQUE_PATH: spanning_tree(T,G) => exactly one simple path between every distinct vertex pair.
LAW MINIMAL_CONNECTED: removing any edge of T disconnects T.
LAW MAXIMAL_ACYCLIC: adding any edge of G not already in T creates exactly one cycle in T+e.
LAW BRIDGE_INCLUSION: every bridge of G belongs to every spanning tree of G.
LAW CYCLE_EXCHANGE: for e in E(G)\E(T), adding e creates a cycle C; removing any edge f in C other than e yields another spanning tree.
LAW CUT_PROPERTY: a minimum-weight edge crossing any cut is safe for some MST; a uniquely lightest cut edge occurs in every MST.
LAW CYCLE_PROPERTY: a uniquely heaviest edge on a cycle belongs to no MST.
LAW MST_UNIQUENESS: pairwise distinct edge weights imply a unique MST; the converse need not hold.
LAW COMPONENT_COUNT: a spanning forest of G has |V(G)|-c(G) edges, where c(G) counts connected components.
LAW CAYLEY: complete labelled graph K_n has n^(n-2) spanning trees for n>=2; K_1 has one.

6. SEMANTIC RELATIONSHIPS
SpanningTree IS_A Tree
SpanningTree IS_A ConnectedGraph
SpanningTree IS_A AcyclicGraph
SpanningTree SPANS VertexSet
SpanningTree SUBGRAPH_OF Graph
SpanningTree CONTAINS Edge
MinimumSpanningTree IS_A SpanningTree
MinimumSpanningTree MINIMISES TotalEdgeWeight
SpanningForest GENERALISES SpanningTree for disconnected graphs
Bridge MUST_BELONG_TO EverySpanningTree
GraphCycle ENABLES EdgeExchange

7. INFERENCE RULES
RULE ST1: connected(G) AND acyclic(G) => spanning_tree(G,G).
RULE ST2: connected(G) AND |E(G)|=|V(G)|-1 => spanning_tree(G,G), for finite non-empty simple undirected G.
RULE ST3: acyclic(T) AND |E(T)|=|V(T)|-1 => connected(T), for finite non-empty undirected T.
RULE ST4: spanning_tree(T,G) AND e in E(T) => T-e is a two-component forest.
RULE ST5: spanning_tree(T,G) AND e in E(G)\E(T) => T+e has one cycle.
RULE ST6: connected(G) AND nonnegative weights => Kruskal and Prim both return an MST; nonnegativity is not necessary for either algorithm.
RULE ST7: spanning_tree(T,G) AND minimal_total_weight(T,G,w) => minimum_spanning_tree(T,G,w).

8. VALIDATION
VALIDATE vertices and endpoints are well typed.
VALIDATE no self-loops or duplicate undirected edges under the simple-graph assumption.
VALIDATE source graph connectivity before requiring a spanning tree.
VALIDATE candidate includes every vertex and only source edges.
VALIDATE acyclicity using union-find or DFS.
VALIDATE connectedness using BFS or DFS.
VALIDATE edge count equals |V|-1 as a necessary condition; never use edge count alone without connectivity or acyclicity.
VALIDATE MST optimality by cut/cycle exchange or an independently verified algorithm.
VALIDATE tie handling without claiming MST uniqueness.
VALIDATE all weights finite and defined on every edge.

9. EXAMPLE
G.V={A,B,C,D}
G.E={{A,B},{B,C},{C,D},{A,D},{A,C}}
T.E={{A,B},{B,C},{C,D}}
CHECK_SPANNING_TREE(G,T)=true
|V|=4; |E(T)|=3; unique paths exist between all vertices.
Adding {A,D} creates cycle A-B-C-D-A.

10. SEMANTIC_EQUIVALENCE
"spanning tree" <=> "connected acyclic spanning subgraph" (finite undirected graph context)
"minimum spanning tree" <=> "least-total-edge-weight spanning tree" (weighted connected graph context)
NOT_EQUIVALENT: shortest-path tree and minimum spanning tree in general.
NOT_EQUIVALENT: spanning tree and spanning forest for disconnected source graphs.
NOT_EQUIVALENT: minimal spanning tree by edge inclusion and minimum-weight spanning tree without an explicit objective.

11. CONFIDENCE
MATHEMATICAL_DEFINITIONS: 1.00 (conditional on declared assumptions)
FORMAL_RULES: 1.00 (conditional on declared assumptions)
SOURCE_PAGE_MATCH: unverified
ASSERTION_POLICY: do not assign empirical confidence to a theorem; record assumptions and proof status instead.

12. FLOW_HASH
CANONICALISE: Unicode UTF-8, LF line endings, stable field ordering, normalised edge endpoint order.
HASH_ALGORITHM: SHA-256
FLOW_HASH: compute SHA-256 over the final canonicalised file bytes at publication; never substitute a fabricated digest.

13. UPDATE_MODEL
VERSION_POLICY: increment version on semantic changes.
DEPENDENCIES: Graph Ontology; Vertex Ontology; Edge Ontology; Tree Ontology; Forest Ontology; Weighted Graph Ontology.
ON_UPDATE: revalidate types, invariants, examples, proof assumptions and cross-ontology mappings.
PROVENANCE: source URL, authorship, version and validation state retained.

14. AI_CONSUMPTION
INPUT: finite undirected graph, optional edge weights, requested task.
TASKS: detect existence; construct spanning tree; construct spanning forest; compute MST; verify candidate; explain certificates.
OUTPUT: typed graph object, selected edges, objective value when applicable, validity checks, assumptions and provenance.
SAFETY: reject malformed graph input; distinguish disconnected cases; do not claim a unique optimum without proof.

END FLOW ALGEBRA