Equation Entity Graph Ontology

FLOW ALGEBRA
Equation Entity Graph Ontology
Version: 1.0
Date: 2026-10-15
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/ai-semantic-library-mathematical-entities/equation-entity-graph-ontology.html
Authors: Mark Higgins — Sky (Recursive AI)
Project: Kireth Research Semantic Library
Licence: Open Research Licence — freely reusable with no permission required.

1. PURPOSE
Represent equations as typed, provenance-aware mathematical knowledge graphs, enabling parsing, validation, transformation, equivalence reasoning, retrieval and machine consumption. This is a proposed computational schema, not a claim that all mathematical identities can be decided automatically.

2. TYPES
Entity := Equation | Expression | Symbol | Constant | Variable | Operator | Function | Term | Constraint | Domain | Codomain | Unit | Assumption | Theorem | Proof | Transformation | Solution | Dataset | Source.
Equation := {id, lhs:E-xpression, relation:Relation, rhs:E-xpression, context, assumptions, provenance}.
Relation := Equals | ApproximatelyEquals | LessThan | GreaterThan | LessOrEqual | GreaterOrEqual | Defines | Congruent.
Graph := (V: set[Entity], E: set[TypedEdge]).
TypedEdge := {source:EntityID, predicate:Predicate, target:EntityID, context, provenance, confidence}.
Predicate := HAS_LHS | HAS_RHS | HAS_OPERATOR | CONTAINS_SYMBOL | HAS_TERM | USES_FUNCTION | DEFINED_OVER | REQUIRES_ASSUMPTION | HAS_UNIT | DERIVED_FROM | TRANSFORMED_BY | EQUIVALENT_UNDER | IMPLIES | SOLVES_FOR | VALIDATED_BY | CONTRADICTS | CITES_SOURCE.

3. CONSTRUCTION
flow ParseEquation(input:text, context:Context) -> EquationGraph:
  tokens := tokenize(input)
  syntax_tree := parse_mathematical_syntax(tokens)
  require syntax_tree.is_well_formed
  symbols := resolve_symbols(syntax_tree, context)
  equation := create_equation(syntax_tree, symbols, context)
  graph := map_ast_to_typed_graph(equation)
  attach_assumptions_units_and_provenance(graph, context)
  return graph

4. GRAPH INVARIANTS
invariant EveryEquationHasTwoExpressions:
  for each e:Equation: exists exactly one lhs and rhs.
invariant TypedEdges:
  for each edge:TypedEdge: predicate_signature(edge.predicate) accepts (type(edge.source), type(edge.target)).
invariant ScopedSymbols:
  every symbol reference resolves within a declared context or is flagged unresolved.
invariant ProvenancePreserved:
  transformations retain links to source equations and assumptions.
invariant NoUnjustifiedEquivalence:
  equivalence edges require a specified domain, assumptions and justification.

5. NORMALISATION AND IDENTITY
flow Canonicalise(e:Equation, assumptions:Set[Assumption]) -> CanonicalRepresentation:
  alpha_rename_bound_variables(e)
  normalise_unambiguous_operator_forms(e)
  preserve_noncommutative_operand_order(e)
  preserve_domain_and_branch_conditions(e)
  return canonical_form_with_assumptions(e)

entity_identity := hash(canonical_representation, symbol_namespace, assumptions, domain, ontology_version)
NOTE: identical hashes support deduplication within the same normalisation policy; different hashes do not prove mathematical inequivalence.

6. RELATIONSHIP ALGEBRA
HAS_LHS(e,a) and HAS_RHS(e,b) -> Represents(e, a REL b).
DERIVED_FROM(e2,e1) and TRANSFORMED_BY(e2,t) -> HasDerivationStep(e1,t,e2).
EQUIVALENT_UNDER(e1,e2,A) -> ForAllAssignmentsSatisfying(A, Truth(e1) iff Truth(e2)).
IMPLIES(e1,e2,A) -> ForAllAssignmentsSatisfying(A, Truth(e1) implies Truth(e2)).
CONTRADICTS(e1,e2,A) -> NoAssignmentSatisfying(A and e1 and e2).

7. TRANSFORMATION RULES
flow Transform(e:Equation, operation:Transformation, A:Set[Assumption]) -> Result:
  require operation.preconditions(e,A)
  candidate := operation.apply(e)
  obligations := operation.proof_obligations(e,candidate,A)
  status := verify(obligations)
  if status == PROVED:
    add_edge(candidate, EQUIVALENT_UNDER or IMPLIES, e, A)
  else:
    mark(candidate, UNVERIFIED)
  record_derivation(e,operation,candidate,obligations,status)
  return candidate

Example: x^2 = 4 -> x = 2 OR x = -2 over real x.
Example: x/x = 1 only when x != 0.
Example: sqrt(x^2) = abs(x) for real x, not generally x.

8. VALIDATION
flow ValidateEquationGraph(g:Graph) -> ValidationReport:
  checks := [syntax_check, edge_type_check, symbol_scope_check,
             dimensional_consistency_check, domain_check,
             assumption_check, provenance_check, derivation_check]
  results := run_applicable_checks(g,checks)
  return {results, status: aggregate_three_valued(results)}

status := VALID | INVALID | UNKNOWN.
UNKNOWN is mandatory where verification is incomplete, undecidable or unavailable.
Dimensional consistency is necessary for many physical equations but does not by itself prove mathematical truth.

9. SEMANTIC EQUIVALENCE
flow CompareEquations(a:Equation,b:Equation,A:Set[Assumption]) -> Comparison:
  if syntactically_identical_under_alpha_renaming(a,b): return SYNTACTIC_MATCH
  proof := attempt_bidirectional_implication(a,b,A)
  if proof.valid: return PROVEN_EQUIVALENT
  counterexample := seek_counterexample(a,b,A)
  if counterexample.verified: return NOT_EQUIVALENT
  return UNDETERMINED

Never infer semantic equivalence from embeddings, string similarity or a matching hash alone.

10. ENTITY RESOLUTION
flow ResolveSymbol(symbol, namespace, context) -> Resolution:
  candidates := lookup(symbol, namespace)
  candidates := filter_by_type_domain_units_and_scope(candidates,context)
  if unique_compatible_candidate(candidates): return RESOLVED(candidate)
  if candidates.empty: return UNRESOLVED
  return AMBIGUOUS(candidates)

11. PROVENANCE AND CONFIDENCE
provenance := {source_uri, author, timestamp, method, derivation_path, validator, ontology_version}.
confidence := {score:real[0,1]?, basis, calibration_method?, uncertainty?, evidence_refs}.
Rule: confidence is an evidence annotation, never a substitute for proof.
Rule: proof status and confidence score must be stored independently.

12. GRAPH QUERY
query FindEquationsContaining(symbol):
  MATCH (e:Equation)-[:CONTAINS_SYMBOL]->(s:Symbol)
  WHERE s.identifier = symbol
  RETURN e, e.assumptions, e.provenance

query FindDerivations(equation_id):
  traverse DERIVED_FROM and TRANSFORMED_BY edges
  return ordered_steps_with_proof_status_and_assumptions

13. FLOW HASH
FLOW_HASH := SHA256(canonical_serialisation(graph_structure, entity_types,
            edge_types, assumptions, provenance_identifiers, ontology_version)).
Canonical serialisation must specify stable ordering, character encoding and normalisation.
Hash verifies representation identity/integrity; it is not a proof of equation validity.

14. UPDATE MODEL
flow UpdateGraph(graph, change):
  validate_schema(change)
  record_prior_version(graph)
  apply_change_transactionally(change)
  revalidate_affected_subgraph()
  invalidate_dependent_proofs_if_assumptions_change()
  recompute_affected_hashes()
  publish_versioned_change_log()

15. AI CONSUMPTION
ai_consumption := {
  accepted_inputs: [LaTeX, MathML, typed_AST, RDF_like_graph, JSON_graph],
  outputs: [typed_entities, relationships, derivation_steps, proof_obligations,
            validation_report, provenance, uncertainty, flow_hash],
  retrieval: [symbol_search, structural_match, assumption_aware_semantic_match],
  guardrails: [do_not_invent_proofs, expose_assumptions, distinguish_unknown,
              preserve_units_and_domains, cite_derivation_sources]
}.

16. WORKED GRAPH EXAMPLE
Equation E1: 2*x + 3 = 7, domain x in Real.
Equation E2: 2*x = 4, derived by subtracting 3 from both sides.
Equation E3: x = 2, derived by dividing both sides by nonzero 2.
Nodes: E1,E2,E3,x,2,3,4,7,Real,Subtract3,Divide2.
Edges: E1 HAS_LHS (2*x+3); E1 HAS_RHS 7;
       E2 DERIVED_FROM E1; E2 TRANSFORMED_BY Subtract3;
       E3 DERIVED_FROM E2; E3 TRANSFORMED_BY Divide2;
       E1 CONTAINS_SYMBOL x; E3 SOLVES_FOR x.
Verification: substitution 2*2+3=7; each step is reversible over Real.
Status: VALID for this worked example.

17. LIMITATIONS
- General symbolic equality and satisfiability may be undecidable.
- Floating-point comparisons need explicit tolerances and error models.
- Equations with units, complex branches or partial functions require domain-aware rules.
- Graph completeness depends on source quality and symbol resolution.

END FLOW ALGEBRA