Big O Notation Ontology

FLOW ALGEBRA
BIG O NOTATION ONTOLOGY
Version: 1.0
Source: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/algorithmic-mathematics/big-o-notation-ontology.html
Authors: Mark Higgins — Sky (Recursive AI)
Project: Kireth Semantic Library
Date: 2026-10-11

1. PURPOSE
Represent asymptotic upper bounds, complexity classes, proof obligations and algorithm-analysis relationships in a typed, inspectable semantic flow.

2. SIGNATURE
sort Natural; sort RealNonnegative; sort Function; sort Algorithm; sort InputModel; sort Resource; sort BoundClaim; sort Proof; sort Evidence.
resource := TIME | SPACE | COMPARISONS | OPERATIONS | IO | COMMUNICATION.
relation cost : Algorithm × InputModel × Resource -> Function.
relation big_o : Function × Function -> Boolean.
relation big_omega : Function × Function -> Boolean.
relation big_theta : Function × Function -> Boolean.
relation little_o : Function × Function -> Boolean.
relation little_omega : Function × Function -> Boolean.
relation supports : Proof × BoundClaim -> Boolean.
relation assumes : BoundClaim × InputModel -> Boolean.

3. DEFINITIONS
For eventually nonnegative f,g : N -> R>=0:
BIG_O(f,g) iff exists c>0, n0 in N such that for all n>=n0, f(n)<=c*g(n).
BIG_OMEGA(f,g) iff exists c>0, n0 in N such that for all n>=n0, f(n)>=c*g(n).
BIG_THETA(f,g) iff BIG_O(f,g) and BIG_OMEGA(f,g).
LITTLE_O(f,g) iff for every c>0 there exists n0 such that for all n>=n0, f(n)<c*g(n).
LITTLE_OMEGA(f,g) iff for every c>0 there exists n0 such that for all n>=n0, f(n)>c*g(n).
All claims require explicit domains, eventual nonnegativity and input-size meaning.

4. TYPED ENTITIES
Algorithm {id, name, specification, assumptions}
InputModel {size_parameter, encoding, case_kind, machine_model}
ComplexityFunction {expression, domain, resource, nonnegative_eventually}
BoundClaim {algorithm_id, input_model_id, resource, relation, bound, status}
Witness {constant_c, threshold_n0, inequalities}
Proof {premises, derivation, witness, validity}
Counterexample {input_family, violated_inequality}

5. RELATIONSHIPS
ALGORITHM --HAS_COST--> COMPLEXITY_FUNCTION
ALGORITHM --EVALUATED_UNDER--> INPUT_MODEL
COMPLEXITY_FUNCTION --UPPER_BOUNDED_BY--> COMPLEXITY_FUNCTION
COMPLEXITY_FUNCTION --LOWER_BOUNDED_BY--> COMPLEXITY_FUNCTION
BOUND_CLAIM --SUPPORTED_BY--> PROOF
BOUND_CLAIM --REFUTED_BY--> COUNTEREXAMPLE
BOUND_CLAIM --MEASURES--> RESOURCE
BOUND_CLAIM --REQUIRES--> ASSUMPTIONS

6. INFERENCE RULES
R1 REFLEXIVITY: BIG_O(f,f).
R2 TRANSITIVITY: BIG_O(f,g) and BIG_O(g,h) => BIG_O(f,h).
R3 CONSTANT SCALING: a>0 => BIG_THETA(a*f,f).
R4 SUM: BIG_O(f,h) and BIG_O(g,h) => BIG_O(f+g,h), for eventually nonnegative functions.
R5 PRODUCT: BIG_O(f,g) and BIG_O(h,k) => BIG_O(f*h,g*k), for eventually nonnegative functions.
R6 THETA: BIG_O(f,g) and BIG_OMEGA(f,g) => BIG_THETA(f,g).
R7 POLYNOMIAL: polynomial p of degree d with positive leading coefficient and eventual nonnegativity => BIG_THETA(p,n^d).
R8 LOG BASE: a,b>1 => BIG_THETA(log_a(n),log_b(n)) for n>=2.
R9 STRICT UPPER: LITTLE_O(f,g) => BIG_O(f,g).
R10 BOUND WEAKENING: BIG_O(f,g) and BIG_O(g,h) => BIG_O(f,h); never infer tightness from an upper bound alone.

7. STANDARD GROWTH FAMILIES
CONSTANT: 1
LOGARITHMIC: log(n)
POLYLOGARITHMIC: (log(n))^k, k>0
LINEAR: n
LINEARITHMIC: n*log(n)
POLYNOMIAL: n^k, k>0
EXPONENTIAL: a^n, a>1
FACTORIAL: n!
For fixed positive k and a>1, the standard ordering holds asymptotically where relevant; parameter constraints must be retained.

8. PROOF FLOW
flow PROVE_BIG_O(f,g,domain):
  require eventually_nonnegative(f) and eventually_nonnegative(g)
  choose c > 0
  choose n0 in domain
  verify forall n >= n0: f(n) <= c*g(n)
  if verified: emit PROVEN with witness(c,n0)
  else: emit UNPROVEN; do not infer FALSE from a failed witness search

9. WORKED EXAMPLES
E1: f(n)=3*n^2+5*n+7; g(n)=n^2.
For n>=1: 3*n^2+5*n+7 <= 15*n^2.
Witness c=15, n0=1; BIG_O(f,g)=TRUE.
Also f(n)>=3*n^2 for n>=1; BIG_THETA(f,g)=TRUE.

E2: f(n)=n*log2(n); g(n)=n^2, n>=2.
Since log2(n)<=n, f(n)<=n^2; BIG_O(f,g)=TRUE.
Moreover f(n)/g(n)=log2(n)/n -> 0; LITTLE_O(f,g)=TRUE.

E3: f(n)=n^2; g(n)=n.
For every c>0 choose n>c; then n^2>c*n.
BIG_O(f,g)=FALSE; BIG_OMEGA(f,g)=TRUE.

10. ALGORITHM COST INTERPRETATION
A claim such as O(n log n) is an upper bound, not necessarily a tight bound.
Specify worst, average, amortised or best case independently.
Specify the computational model and size parameter.
Distinguish running time from memory, I/O and communication costs.
Do not treat benchmark measurements alone as asymptotic proofs.
Multivariate bounds require named parameters and a declared limiting regime.

11. VALIDATION
V1: reject missing function domain or resource type.
V2: reject upper-bound claims without quantified witnesses or accepted theorem provenance when status=PROVEN.
V3: detect contradictions between proven O and proven non-O for identical assumptions.
V4: check input model consistency across compared algorithms.
V5: prevent conversion from BIG_O to BIG_THETA without lower-bound proof.
V6: preserve logarithm bases and parameter constraints during normalisation.
V7: retain proof provenance and uncertainty on imported claims.

12. SEMANTIC EQUIVALENCE
aliases: [Big O notation, asymptotic upper bound, Landau O notation]
related_not_identical: [Theta notation, Omega notation, little-o notation, empirical runtime, worst-case complexity]
canonical_relation: BIG_O(f,g)
normalisation: alpha-rename bound variables; simplify positive constant factors under stated conditions; retain domains and assumptions.

13. CONFIDENCE
confidence.kind: epistemic
confidence.proven: 1.0 only when proof is checked against stated assumptions
confidence.unverified: unknown, not a fabricated numeric score
confidence.empirical: report separately from formal proof status

14. FLOW_HASH
algorithm: SHA-256
input: canonical UTF-8 serialisation of ontology version, typed signature, axioms, rules and assumptions
value: COMPUTE_ON_PUBLICATION
note: no hash is asserted without computation.

15. UPDATE_MODEL
versioning: semantic
on_change: increment version, regenerate canonical hash, preserve previous revisions, rerun validation and proof checks
breaking_changes: altered definitions, quantifier scope, input-model semantics or inference rules

16. AI_CONSUMPTION
format: UTF-8 plain text
purpose: semantic retrieval, formal reasoning, complexity comparison and proof-assisted analysis
parse_order: metadata -> types -> definitions -> relationships -> inference -> examples -> validation
safety: never promote heuristic complexity estimates to formal theorems
output_contract: {claim, resource, input_model, assumptions, bound, proof_status, witness_or_reference, confidence}

END FLOW ALGEBRA