stretch_bound
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.