J_log_quadratic_approx
plain-language theorem explainer
The theorem supplies a fourth-order error bound on the quadratic Taylor approximation to the log-coordinate J-cost for perturbations smaller than unity. Analysts of stability in continuous versus discrete configuration spaces cite it when quantifying how infinitesimal defects incur vanishingly small costs. The proof reduces the claim to the pre-established cosh remainder estimate after rewriting the cost function and normalizing the absolute-value term.
Claim. For every real number ε satisfying |ε| < 1, |(cosh ε − 1) − ε²/2| ≤ |ε|⁴/20, where cosh ε − 1 is the expression for the J-cost evaluated at the exponential of the log-ratio ε.
background
In the Discreteness Forcing module the J-cost is rewritten in logarithmic coordinates by the definition J_log(t) := cosh(t) − 1. This produces a convex bowl centered at the origin whose second derivative at zero equals one, furnishing the minimal step cost that later forces discreteness. The local theoretical setting is the argument that continuous configuration spaces admit no isolated J-minima because any point can be perturbed by an arbitrarily small ε whose cost is only quadratic in ε.
proof idea
The tactic proof first rewrites J_log ε to cosh ε − 1 by unfolding the definition and simplifying the exponential identities. It then replaces |ε|⁴ by ε⁴ via the identity |ε|⁴ = (ε²)². The resulting inequality is discharged by a direct application of the upstream cosh_quadratic_bound lemma.
why it matters
The result supplies the quantitative estimate needed to conclude that continuous spaces possess no stable J-minima, because the cost of an infinitesimal defect can be made smaller than any positive threshold. It therefore supports the module’s main chain: continuous_no_stable_minima and rs_exists_requires_discrete. Within the Recognition Science framework it sharpens the T5 J-uniqueness statement by exhibiting the explicit quadratic bowl that must be escaped by discrete jumps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Survey maps paths to efficient LLM reasoning
"RL with Length Reward Design... length reward assigns higher scores to short, correct answers while penalizing lengthy or incorrect ones"
-
Mixup on example pairs improves neural network generalization
"mixup regularizes the neural network to favor simple linear behavior in-between training examples."