IndisputableMonolith.Relativity.Analysis.Limits
The Limits module supplies definitions for big-O and little-o asymptotic notations to support error analysis in relativistic models. Researchers deriving approximation bounds within the Recognition framework would cite these predicates. It is a pure definition module with no proofs, importing Mathlib for basic real analysis primitives.
claimThe module defines the predicate that $f = O(g)$ near $a$ when there exist constants $C, M > 0$ such that $|f(x)| ≤ C |g(x)|$ for all $|x - a| < M$, together with the little-o variant, power-law forms, and closure under addition and multiplication.
background
This module belongs to the Relativity.Analysis package, which collects mathematical analysis utilities for the Recognition Science framework. It introduces big-O notation via the explicit predicate ∃ C, M such that |f(x)| ≤ C |g(x)| for |x-a| < M, along with little-o, IsBigOPower, and arithmetic lemmas. The setting relies on standard limit and continuity notions imported from Mathlib to furnish precise asymptotic comparisons for physical error bounds.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the parent Relativity.Analysis module and the Landau submodule, supplying the asymptotic predicates required for rigorous error-term manipulation. It directly supports Landau-style big-O arithmetic used in relativistic approximation arguments within the Recognition framework.
scope and limits
- Does not prove any limit theorems from first principles.
- Does not supply numerical evaluation or approximation algorithms.
- Does not extend the predicates to complex-valued or vector-valued functions.
- Does not incorporate specific physical constants or Recognition Science units.