t2_analytic_refinement_holds
plain-language theorem explainer
After scalar cost is available, T2's analytic refinement packages two facts: the log-coordinate cost has unit curvature at its minimum, and the full discreteness forcing principle holds (nonnegative defect, unique zero at identity, continuum non-isolation). Citers of the continuous-cannot-stabilize step in the unified forcing chain use this bundle. The proof is a two-field structure constructor reusing the second-derivative identity and the discreteness forcing theorem.
Claim. The analytic refinement of discreteness holds: $\frac{d^2}{dt^2} J_{\log}(0) = 1$, and the discreteness forcing principle is true, namely $\mathrm{defect}(x)\ge 0$ for $x>0$ with $\mathrm{defect}(x)=0\Leftrightarrow x=1$, the same unit curvature, and every zero of the defect fails to be isolated in $\mathbb{R}_{>0}$.
background
The Unified Forcing Chain module shows T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T2 is the discreteness step: continuous configurations cannot stabilize under cost, because an infinitesimal move costs only an infinitesimal amount.
Once the scalar cost is in play, the analytic form is $J(x)=\frac12(x+x^{-1})-1$, or in log coordinates $J_{\log}(t)=\cosh(t)-1$. Upstream, the second derivative of $J_{\log}$ at $0$ equals $1$; that curvature is the stiffness of the cost bowl and the minimum step cost for discrete configurations. The discreteness forcing principle packages four claims: defect nonnegative, unique zero at $x=1$, unit curvature, and continuum non-isolation at every zero.
The structure here is only the analytic refinement of T2 after scalar $J$ has been introduced; the pre-analytic floor story sits earlier in the chain.
proof idea
Term-mode structure constructor with two fields and no new algebra. The curvature field is discharged by the upstream identity that the second derivative of $J_{\log}$ at zero is $1$ (via $J_{\log}=\cosh-1$, so the second derivative is $\cosh$ and $\cosh(0)=1$). The discreteness-principle field is filled by the already-proved discreteness forcing principle, which is exactly the four-conjunct Prop required by the structure. Pure packaging of prior DiscretenessForcing results into the T2 analytic-refinement interface.
why it matters
Keeps the classical analytic discreteness theorem live as a named T2 refinement after the chain was reorganized around the absolute floor and cost foundation. The sole downstream consumer is the T5-to-analytic-refinements bridge, which "follows from T5 plus the closed-form identities of the analytic $J$-scaffolding" and needs this bundle among the refinements.
In the forcing landmarks, T2 sits between MP (T1) and the ledger (T3). The unit-curvature calibration is the same stiffness later used when unique $J$ is forced at T5 (d'Alembert plus normalization and calibration) and when $\varphi$ is pinned as the self-similar fixed point at T6. Without this refinement, the scalar-defect form of "continuous cannot stabilize" would drop out of the post-T5 analytic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.