IndisputableMonolith.Relativity.Analysis
Aggregation module for asymptotic analysis in the relativity sector. It surfaces rigorous Landau big-O membership and filter-based limits so curvature and post-Newtonian expansions can cite proper O(·) and o(·) remainders instead of informal error talk. Anyone writing weak-field or slow-motion expansions in the RS stack would cite this layer. The module itself holds no theorems; it imports and exposes the Landau and Limits submodules.
claimNamespace packaging filter-based asymptotic classes $f \in O(g)$ and $f \in o(g)$, with arithmetic lemmas on error bounds, as the analysis layer for relativistic expansions.
background
The relativity sector of Recognition Science needs controlled expansions (weak-field, post-Newtonian, multipole) whose error terms survive formal verification. Mathlib already supplies Filter asymptotics; this module surfaces them under a single Relativity.Analysis entry point.
The Landau submodule implements $f \in O(g)$ as a proper Filter predicate and supplies arithmetic operations on asymptotic expressions, with lemmas for manipulating those expressions. The Limits submodule integrates Mathlib's asymptotics library so placeholder error bounds can be replaced by rigorous $O(\cdot)$ and $o(\cdot)$ statements.
Together they are the pre-read toolkit before any metric-perturbation or curvature argument that quotes an asymptotic remainder.
proof idea
This is a re-export module with no standalone proofs. It imports the Landau submodule (Filter-based big-O with arithmetic lemmas) and the Limits submodule (Mathlib asymptotics integration for $O$ and $o$), exposing both to the rest of the relativity stack.
why it matters in Recognition Science
Downstream relativity work that needs verified error bounds depends on one analysis entry point rather than ad-hoc placeholders. The module sits in the Relativity domain and feeds any argument that manipulates $O(g)$ remainders in expansions. No direct used-by edges are recorded at module granularity; the role is infrastructural, closing the gap between informal asymptotic language and Lean Filter predicates so later geometric or forcing-chain claims can cite clean bounds.
scope and limits
- Does not prove physical identities or Einstein-equation consequences.
- Does not define metrics, curvature tensors, or RS mass ladders.
- Does not replace Mathlib asymptotics; it organizes them for Relativity.
- Does not add theorems beyond what the Landau and Limits imports export.
- Does not treat discrete phi-ladder or eight-tick constructions.