zero_mem_Icc_zero_one
plain-language theorem explainer
Zero belongs to the closed real interval [0,1]. Anyone restricting the nonlinear Regge remainder to the canonical line segment from a flat configuration needs this membership fact when evaluating jets at the basepoint. The proof is a two-line constructor: reflexivity of ≤ on the left endpoint and a numeric check on the right.
Claim. As a real number, $0$ lies in the closed interval $[0,1]$, i.e. $0 \le 0$ and $0 \le 1$.
background
The module isolates the cubic Taylor bound for the nonlinear Regge action remainder after the Hessian has already been identified. The analytic content is a local third-order estimate in the finite-dimensional space of vertex potentials on a 3D triangulation.
Along a flat configuration one studies the remainder restricted to the line segment $t \mapsto t\xi$ for $t \in [0,1]$. Membership of the basepoint $t=0$ in that parameter interval is a prerequisite for statements about iteratedDerivWithin of the line restriction at zero, and for norm bounds that only hold on $[0,1]$.
The surrounding development already has first- and second-variation inputs that force the first two derivatives of the remainder (and of its line restriction) to vanish at the flat point; the interval fact itself is pure real analysis.
proof idea
Term-mode proof that builds the Set.Icc membership pair directly. The left inequality $0 \le 0$ is le_refl 0. The right inequality $0 \le 1$ is discharged by norm_num. No geometry or Regge-specific lemmas are used.
why it matters
Private helper inside the cubic Taylor pipeline. It is cited by the two jet-input theorems that compute the first and second iterated derivatives of the canonical remainder line at zero: both need $0 \in [0,1]$ before they can invoke iteratedDerivWithin on that interval and conclude the derivatives vanish from the first- and second-variation hypotheses.
Those vanishing derivatives are the analytic input to the cubic remainder estimate that closes the nonlinear Regge Taylor theorem in this module. The result is scaffolding glue, not a framework landmark; it does not touch T0–T8, the RCL, or the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.