min_pos3
plain-language theorem explainer
If three real numbers are strictly positive, the nested minimum of the three is strictly positive. Local arithmetic helper used when packaging cubic line-Taylor data for the nonlinear Regge remainder. Proof is a one-line double application of the two-argument min-positivity lemma.
Claim. For real numbers $a,b,c$ with $a>0$, $b>0$, and $c>0$, one has $0 < \min(\min(a,b),c)$.
background
The ambient module isolates the final analytic Taylor theorem for the nonlinear Regge remainder after the Hessian has been identified. The heavy content is a local third-order bound in finite-dimensional vertex-potential space on a 3D triangulation.
This declaration is pure real-arithmetic scaffolding inside that pipeline. Nested min appears when three positive scale or radius parameters must be collapsed to a single positive lower bound (for example when restricting a remainder estimate to a common interval). No Regge-specific structure enters the statement.
The only external fact used is the standard two-argument lemma that the minimum of two positive reals is positive.
proof idea
One-line wrapper. Apply the two-argument positivity-of-min lemma first to $a$ and $b$, then again to that result and $c$. No case splits or algebraic rewriting.
why it matters
Feeds the private assembly theorem that builds line Taylor data from split continuity, quadratic-vanishing, and third-derivative bound targets on a consistent 3D triangulation. That assembly is the last packaging step before the cubic Taylor bound for the canonical nonlinear Regge remainder can be stated as a single target.
In the broader Recognition geometry stack this sits downstream of the nonlinear Hessian identification and upstream of the cubic remainder control used in discrete curvature/action estimates. It does not itself touch forcing-chain landmarks (T5–T8, RCL, phi); it is bookkeeping that keeps positivity hypotheses closed when three positive constants are merged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.