IndisputableMonolith.Relativity.Analysis.Limits
The module supplies definitions for big-O, little-o and related asymptotic predicates in one variable. Researchers bounding approximation errors in relativistic models cite these for limit statements. It consists entirely of predicate definitions with no proof obligations or theorems.
claim$f = O(g)$ near $a$ when there exist $C, M > 0$ such that $|f(x)| ≤ C |g(x)|$ for all $|x-a| < M$; analogous predicates are supplied for little-o, powers, addition, multiplication and composition.
background
The module belongs to Relativity.Analysis, whose doc-comment states it supplies mathematical analysis utilities for Landau big-O notation and limit theorems. It introduces the predicates IsBigO, IsLittleO, IsBigOPower, IsLittleOPower together with arithmetic lemmas such as bigO_add, bigO_mul and littleO_implies_bigO. The parent Analysis module positions these tools for error bounds in physical limits.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module is imported by Relativity.Analysis and by Relativity.Analysis.Landau; the latter implements f ∈ O(g) as a Filter predicate and supplies lemmas for manipulating asymptotic expressions. It therefore supplies the concrete predicates required by the Landau submodule for rigorous error control.
scope and limits
- Does not contain continuity or limit theorems.
- Does not treat multi-variable or vector-valued cases.
- Does not supply numerical evaluation or approximation algorithms.
- Does not address convergence rates beyond the listed predicates.