ratio_mono
plain-language theorem explainer
The real ratio n/(n+1) is nondecreasing in the natural degree n: each step up the ladder weakly increases the contraction factor. Anyone bounding pairwise distances under iterated barycentric subdivision of affine simplices cites this. The proof clears positive denominators and finishes by nonlinear arithmetic with a square nonnegativity witness.
Claim. For every natural number $n$, $\frac{n}{n+1}\le\frac{n+1}{n+2}$ as an inequality of real numbers.
background
The module develops affine singular chains and barycentric subdivision for Recognition Science Stage 6 estimates. An affine simplex is a tuple of vertices in a standard simplex; the barycentric subdivision operator asub splits it into smaller affine pieces whose vertices remain in the original convex hull.
Distance control on those pieces uses the elementary contraction factor $n/(n+1)$ in degree $n$. Monotonicity of that factor in $n$ is the pure real-arithmetic fact recorded here; it is independent of the geometric embedding and of the homology machinery imported from Mathlib singular homology.
Downstream, the Stage 6 main estimate packages hull membership together with the contracted diameter bound. This lemma supplies the comparison between consecutive degree ratios used when that bound is assembled.
proof idea
Term-mode proof in two steps. Rewrite the claimed division inequality via div_le_div_iff₀, discharging both denominator positivity goals by positivity (since $n+1$ and $n+2$ are positive as reals). The cleared form is a quadratic comparison; close it with nlinarith seeded by sq_nonneg on $(n:\mathbb{R})$, which supplies the nonnegativity certificate the linear arithmetic engine needs.
why it matters
Feeds directly into asub_support_bound, the Stage 6 main estimate: every piece of the barycentric subdivision of an affine simplex has vertices in the original hull, with pairwise distances contracted by the factor $n/(n+1)$. Without monotonicity of that ratio, comparing subdivision depths or chaining diameter bounds across degrees would need ad-hoc case splits.
In the Recognition foundation stack this sits under the singular-subdivision layer that supports controlled chain-level approximations (eight-tick and forcing-chain geometry live upstream; this lemma is local real arithmetic). It closes no open forcing step by itself, but it is a proved, sorry-free brick in the diameter estimate that Stage 6 quotes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.