T2_AnalyticDiscreteness_Refinement
plain-language theorem explainer
Analytic refinement of T2 (discreteness) once the scalar cost J is in place. It packages curvature of J at its log-coordinate minimum with the classical nonnegativity, uniqueness-of-zero, and continuum-neighborhood clauses for the scalar defect. Downstream witnesses and the T5-to-analytic-refinements bridge cite it. Pure Prop structure: field list only, no proof body.
Claim. The analytic T2 refinement is the conjunction of: (i) $J_{\log}''(0)=1$ where $J_{\log}(t)=\cosh t-1$; (ii) for all $x>0$, the scalar defect $d(x)$ obeys $d(x)\ge 0$, $d(x)=0\Leftrightarrow x=1$, the same curvature identity, and every zero of $d$ is an accumulation point of the positive reals (for every $\varepsilon>0$ there is $y\ne x$ with $|y-x|<\varepsilon$).
background
Module UnifiedForcingChain claims the full T-1 through T8 ladder is forced from the Recognition Composition Law plus normalization and calibration. T2 is the discreteness step: continuous configurations cannot stabilize under cost.
After the scalar cost appears, discreteness is restated analytically. Upstream, DiscretenessForcing.J_log is $J$ in log coordinates: $J_{\log}(t)=\cosh t-1$, a convex bowl minimized at $t=0$. Its second derivative at the minimum is the calibration $F''(1)=1$ written in additive coordinates. LawOfExistence.defect is the same cost on positive reals (defect equals $J$), nonnegative with unique zero at unity.
The structure therefore records both the local curvature of the bowl and the older scalar-defect discreteness principle (nonnegativity, unique zero, curvature, and that zeros sit in a continuum neighborhood). It is the analytic face of T2 once $J$ exists, not a new physical postulate.
proof idea
Definitional Prop structure: no proof body. Two fields only. j_curved is the identity $J_{\log}''(0)=1$. discreteness_principle is a four-way conjunction restating nonnegativity of defect, unique zero at $1$, the same second-derivative calibration, and the continuum-neighborhood clause at zeros. Inhabitation is deferred to the sibling theorem that fills the fields from J_log_second_deriv_at_zero and discreteness_forcing_principle.
why it matters
Sits on the T2 rung of the complete inevitability chain (continuous configurations cannot stabilize under cost). The sibling t2_analytic_refinement_holds builds a concrete witness by plugging in the second-derivative lemma for $J_{\log}$ and the forced discreteness principle, so the old analytic discreteness theorem remains available downstream after the chain is reorganized.
Also consumed by T5_To_AnalyticRefinements_Bridge: once T5 forces the unique closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), all analytic refinement bundles, including this T2 package, rest on that same reciprocal cost. Landmark link: T5 J-uniqueness and the calibration $F''(1)=1$ that pins the bowl curvature appearing here as $J_{\log}''(0)=1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.