Convergent Sequence Ontology

FLOW ALGEBRA
TITLE: Convergent Sequence Ontology
SOURCE: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/sequence-and-series-entities/convergent-sequence-ontology.html
VERSION: 4.0
AUTHORS: Mark Higgins — Sky (Recursive AI)
PROJECT: Kireth Semantic Library

ENTITY: ConvergentSequence
TYPE: MathematicalEntity > SequenceEntity > ConvergentSequence
DEFINITION: A sequence (a_n) converges to L when for every epsilon > 0 there exists N in natural numbers such that for all n >= N, |a_n - L| < epsilon.

ENTITIES:
  Sequence: indexed function a: N -> X
  Term: a_n
  Index: n in N
  Limit: L in X
  Tolerance: epsilon > 0
  ThresholdIndex: N(epsilon) in N
  Metric: d: X x X -> nonnegative reals
  AmbientSpace: metric space (X,d)

RELATIONSHIPS:
  ConvergentSequence IS_A Sequence
  ConvergentSequence HAS_TERM Term
  ConvergentSequence HAS_LIMIT Limit
  ConvergentSequence DEFINED_OVER AmbientSpace
  Convergence REQUIRES EventualProximity
  Convergence IMPLIES CauchySequence
  Convergence IMPLIES BoundedSequence
  Convergence IMPLIES UniqueLimit
  SubsequenceOfConvergentSequence CONVERGES_TO SameLimit

FLOW ALGEBRA:
  INPUT: sequence a: N -> X; candidate limit L in X; metric d
  VALIDATE: (X,d) is a metric space and all a_n belong to X
  TEST: forall epsilon > 0, exists N in N, forall n >= N: d(a_n,L) < epsilon
  TRUE -> CONVERGENT(sequence=a, limit=L)
  FALSE -> NOT_CONVERGENT_TO(sequence=a, candidate=L)
  NOTE: Failure for one candidate L does not establish divergence; another limit may exist.

FORMAL RULES:
  R1: CONVERGES(a,L) AND CONVERGES(a,M) -> L=M
  R2: CONVERGES(a,L) -> CAUCHY(a)
  R3: CONVERGES(a,L) -> BOUNDED(a)
  R4: CONVERGES(a,L) AND SUBSEQUENCE(b,a) -> CONVERGES(b,L)
  R5: CONVERGES(a,L) AND CONTINUOUS(f,L) -> CONVERGES(f(a),f(L))
  R6: CONVERGES(a,L) AND CONVERGES(b,M) -> CONVERGES(a+b,L+M) [normed vector space]
  R7: CONVERGES(a,L) AND CONVERGES(b,M) -> CONVERGES(a*b,L*M) [real or complex sequences]
  R8: CAUCHY(a) AND COMPLETE(X) -> EXISTS L IN X: CONVERGES(a,L)
  R9: MONOTONE(a) AND BOUNDED(a) -> CONVERGES(a,L) [real-valued sequences]

EXAMPLES:
  E1: a_n=1/n, n>=1 -> limit 0
  E2: a_n=(n+1)/n, n>=1 -> limit 1
  E3: a_n=(-1)^n -> divergent (two distinct constant subsequence values)
  E4: a_n=n -> divergent in real numbers

SEMANTIC_EQUIVALENCE:
  convergent sequence ~= sequence with a finite limit in its ambient metric space
  convergence to L ~= epsilon-N eventual proximity to L
  NOTE: Finite-limit wording applies to real/complex sequences; the metric-space definition is more general.

CONFIDENCE:
  MathematicalDefinitions: 1.00
  StandardTheorems: 1.00
  SourcePageAlignment: unverified

FLOW_HASH:
  METHOD: SHA-256 of canonical UTF-8 file content, calculated externally when deployed
  STATUS: not computed

UPDATE_MODEL:
  VERSION: 4.0
  REVIEW_TRIGGER: change in definitions, theorem scope, or ontology relationships
  PRESERVE: mathematical validity, domain assumptions, and provenance

AI_CONSUMPTION:
  MACHINE_READABLE: true
  PURPOSE: semantic retrieval, reasoning, proof guidance, entity-graph linkage
  CAUTION: Do not infer convergence from boundedness alone; do not infer convergence from Cauchy property without completeness.

END FLOW ALGEBRA