stretch_bound
The lemma establishes that |c| + 1 is strictly positive for every real c. Analysts deriving asymptotic bounds under linear rescaling in relativity models cite it to guarantee positivity of stretch factors. The proof is a one-line wrapper that invokes non-negativity of the absolute value and closes via linear arithmetic.
claimFor any real number $c$, $|c| + 1 > 0$.
background
The module supplies Mathlib-based asymptotic notation (big-O and little-o) to replace placeholder error bounds with Filter definitions. The lemma supplies a basic positivity fact needed for linear rescaling arguments. Upstream results supply structural classes and theorems on collision-free programs, edge lengths from psi, and self-reference structures, though the immediate argument uses only elementary real-number properties.
proof idea
The proof is a term-mode wrapper. It first records the fact 0 ≤ |c| by abs_nonneg, then applies linarith to obtain the strict inequality from that non-negativity.
why it matters in Recognition Science
The lemma supplies a minimal positivity guard for stretch bounds inside the asymptotic analysis layer of the relativity module. It supports replacement of placeholder bounds by proper O(·) and o(·) statements. No downstream uses are recorded, so it functions as foundational scaffolding rather than a cited parent theorem. It addresses the framework requirement for rigorous linear bounds before more complex limit arguments are built.
scope and limits
- Does not supply quantitative bounds beyond strict positivity.
- Does not extend to nonlinear or vector-valued rescalings.
- Does not apply outside the real numbers.
formal statement (Lean)
167lemma stretch_bound (c : ℝ) : |c| + 1 > 0 := by
proof body
Term-mode proof.
168 have : 0 ≤ |c| := abs_nonneg _
169 linarith
170
171/-! **Little-o Multiplication**: If f = o(g) and h is bounded, then f·h = o(g·h).
172 This is a placeholder for the actual asymptotic result. -/
173
174end Analysis
175end Relativity
176end IndisputableMonolith