Mathematical Entity Ontology

FLOW ALGEBRA
MATHEMATICAL ENTITY ONTOLOGY
Kireth Semantic Library | Version 1.0 | 2026-10-12
Authors: Mark Higgins — Sky (Recursive AI)
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/foundations-of-mathematical-entities/mathematical-entity-ontology.html
Status: Subject-based formalisation; live page content not independently verified.

01. PURPOSE
flow MathematicalEntityOntology v1.0
  domain: mathematical_entities
  intent: typed representation, validation, transformation, and inference
  semantics: explicit assumptions, domains, evidence and provenance

02. TYPE SYSTEM
  type EntityID = string
  type Domain = Set | Structure | Space | Category | Theory
  type TruthStatus = proved | refuted | unknown | conditional
  type Confidence = real[0,1]
  type Expression = AST
  type Proof = sequence[InferenceStep]
  type Provenance = {source, version, timestamp, method}
  type MathematicalEntity = {
    id: EntityID, kind: EntityKind, domain: Domain,
    definition: -Expression?, assumptions: Set[Proposition],
    properties: Set[Proposition], provenance: Provenance
  }

03. ENTITY TAXONOMY
  EntityKind := Number | Symbol | Variable | Constant | Set | Element |
    Tuple | Sequence | Function | Relation | Operation | Expression |
    Equation | Inequality | Matrix | Vector | Tensor | Graph |
    GeometricObject | ProbabilityObject | LogicalObject |
    AlgebraicStructure | TopologicalSpace | MathematicalModel |
    Proposition | Theorem | Lemma | Corollary | Axiom | Proof
  Number := Natural | Integer | Rational | Real | Complex
  AlgebraicStructure := Group | Ring | Field | Module | VectorSpace

04. IDENTITY AND EQUALITY
  entity_identity(a,b) := a.id == b.id
  mathematical_equality(a,b,context) :=
    prove(context.assumptions |- a = b)
  structural_isomorphism(a,b) :=
    exists bijection f preserving specified operations/relations
  semantic_equivalence(a,b,context) :=
    same_denotation(a,b,context) where well_typed(a,b)
  invariant: identity != mathematical_equality != isomorphism

05. CORE RELATIONSHIPS
  INSTANCE_OF(entity,kind)
  ELEMENT_OF(element,set)
  SUBSET_OF(set_a,set_b)
  DOMAIN_OF(domain,function)
  CODOMAIN_OF(codomain,function)
  MAPS_TO(function,input,output)
  SATISFIES(entity,property)
  DEFINED_BY(entity,definition)
  DERIVED_FROM(result,premises)
  ISOMORPHIC_TO(structure_a,structure_b)
  DEPENDS_ON(statement,assumption)
  PROVED_BY(theorem,proof)
  REPRESENTED_AS(entity,expression)

06. WELL-FORMEDNESS
  rule R01: every entity has a unique identifier within its namespace
  rule R02: every operation declares operand and result types
  rule R03: every expression resolves its free variables or reports them
  rule R04: every theorem records assumptions and a proof status
  rule R05: equality is only evaluated in a shared valid context
  rule R06: undefined expressions are not assigned numeric values

07. SET SEMANTICS
  member(x,A) : Proposition
  subset(A,B) := forall x (member(x,A) -> member(x,B))
  union(A,B) := {x | member(x,A) or member(x,B)}
  intersection(A,B) := {x | member(x,A) and member(x,B)}
  difference(A,B) := {x | member(x,A) and not member(x,B)}
  guard: set comprehension must declare a universe or valid theory

08. FUNCTION SEMANTICS
  function f: A -> B
  evaluate(f,x) requires x in A
  output y := f(x) requires y in B
  injective(f) := forall x1,x2 in A (f(x1)=f(x2) -> x1=x2)
  surjective(f) := forall y in B exists x in A (f(x)=y)
  bijective(f) := injective(f) and surjective(f)
  compose(g,f) requires codomain(f) compatible with domain(g)

09. RELATIONS AND OPERATIONS
  relation R subseteq A x B
  reflexive(R) := forall a in A: R(a,a)
  symmetric(R) := forall a,b in A: R(a,b) -> R(b,a)
  transitive(R) := forall a,b,c in A: (R(a,b) and R(b,c)) -> R(a,c)
  binary_operation(op,A) := op: A x A -> A
  associative(op) := forall a,b,c: op(op(a,b),c)=op(a,op(b,c))

10. EXPRESSIONS AND NORMALISATION
  parse(text) -> Expression | ParseError
  typecheck(expression,environment) -> TypedExpression | TypeError
  simplify(expression,assumptions) -> expression'
  canonicalise(expression,domain,ruleset) -> normal_form
  invariant: transformations preserve denotation under assumptions
  caution: no universal canonical form for all mathematical expressions

11. LOGIC AND PROOFS
  judgement: Gamma |- proposition
  proof_step := {premises, rule, conclusion, scope}
  modus_ponens: P, (P -> Q) |- Q
  universal_elimination: forall x P(x) |- P(t) if t is admissible
  theorem_status := proved only if every proof step is verified
  open_conjecture := unknown, not false
  contradictory_assumptions := flagged before inference

12. MATHEMATICAL STRUCTURES
  group(G,op) requires closure, associativity, identity, inverses
  ring(R,+,*) requires additive abelian group and ring axioms
  field(F,+,*) requires field axioms and 0 != 1
  vector_space(V,F,+,scalar_mul) requires vector-space axioms
  morphism preserves declared structure
  equivalence classes require a verified equivalence relation

13. DIMENSION AND UNIT SAFETY
  quantity := {magnitude,unit,dimension}
  add(q1,q2) requires compatible dimensions and units
  multiply(q1,q2) -> combined_dimension
  convert(q,unit2) requires explicit conversion rule
  invariant: dimensionless != unitless metadata omission

14. MATHEMATICAL UNCERTAINTY
  distinguish exact symbolic values from approximations
  approximate := {estimate,error_bound?,method,precision}
  interval_result := [lower,upper] with stated assumptions
  numerical_equality(a,b,tolerance) is not exact equality
  propagate_error only under specified computational model

15. INFERENCE RULES
  IF x in A AND A subseteq B THEN x in B
  IF f: A -> B AND x in A THEN f(x) in B
  IF R transitive AND R(a,b) AND R(b,c) THEN R(a,c)
  IF a=b AND property P(a) is substitutable THEN P(b)
  IF theorem T proved AND assumptions hold THEN apply(T)
  IF proof has an unverified premise THEN status(T):=conditional

16. SEMANTIC_EQUIVALENCE
  SEMANTIC_EQUIVALENCE(a,b,context):
    require compatible types and interpretations
    attempt proof of same denotation under context assumptions
    return {equivalent:true|false|unknown, proof?, assumptions}
  examples:
    x+x == 2*x over a commutative additive structure
    sin(x)^2+cos(x)^2 == 1 for real x
  warning: surface-text similarity alone does not establish equivalence

17. CONFIDENCE
  CONFIDENCE(assertion) := {
    score: real[0,1], basis: formal_proof|verified_source|heuristic,
    calibration: optional, limitations: list[string]
  }
  rule: verified formal derivation reports proof status separately
  rule: heuristic confidence never substitutes for mathematical proof

18. PROVENANCE AND TRACEABILITY
  every asserted theorem -> source or derivation identifier
  every transformation -> rule identifier and assumptions
  every external definition -> citation and version
  every generated result -> model version and timestamp
  preserve original input for audit and reproducibility

19. FLOW EXECUTION
  input := {entity_definition, domain, assumptions, requested_task}
  stage 1: parse and identify entity kinds
  stage 2: resolve symbols and namespaces
  stage 3: validate types, domains, and assumptions
  stage 4: build entity-relationship graph
  stage 5: select applicable mathematical rules
  stage 6: execute symbolic or numeric operations
  stage 7: verify proof obligations and constraints
  stage 8: annotate provenance, confidence, uncertainty
  output := {entities, relations, results, proofs, warnings, metadata}

20. FAILURE STATES
  ParseError | TypeError | DomainError | UndefinedOperation |
  InconsistentAssumptions | UnprovedClaim | PrecisionLoss |
  MissingProvenance | UnsupportedInference | ResourceLimit
  rule: failure must not silently produce a proved result

21. FLOW_HASH
  FLOW_HASH := SHA256(canonical_serialisation({
    flow_name, version, entity_types, relationships,
    rules, assumptions, input_schema, output_schema
  }))
  canonical_serialisation requires stable key order and encoding
  hash is an integrity identifier, not a proof of correctness

22. UPDATE_MODEL
  UPDATE_MODEL(new_definition):
    validate(new_definition)
    compare semantic changes with previous version
    re-evaluate dependent propositions and transformations
    invalidate stale proof or inference caches
    publish version, change log, provenance and new FLOW_HASH

23. AI_CONSUMPTION
  AI_CONSUMPTION := {
    entity_resolution: typed,
    graph_navigation: relationship_aware,
    symbolic_reasoning: proof_obligation_aware,
    numerical_reasoning: precision_aware,
    uncertainty: explicit,
    source_attribution: mandatory,
    hallucination_guard: reject_unsupported_proofs,
    output_format: structured_and_auditable
  }

24. VALIDATION EXAMPLES
  example E1: A={1,2}, B={1,2,3}; infer A subseteq B
  example E2: f(x)=x^2, domain=Real; f(3)=9
  example E3: f(x)=1/x, domain=Real excluding 0; f(0) -> DomainError
  example E4: claim sqrt(x^2)=x for all real x -> refuted
  example E5: sqrt(x^2)=abs(x) for real x -> proved
  example E6: x/x=1 requires x != 0

25. COMPLETION CONTRACT
  complete iff types valid, provenance present,
    assumptions explicit, operations well-defined,
    inference status auditable, and errors surfaced
  output must not conflate plausibility with proof

END FLOW ALGEBRA