h
plain-language theorem explainer
The quadratic h(t) = t²/2 supplies the local approximation to the transformed J-cost near its minimum in logarithmic coordinates. Researchers establishing the ALEXIS closed-loop control identity cite it when matching the log-ratio cost family to J(x) at the fixed point x=1. The declaration is introduced as a direct noncomputable definition with no lemmas or reductions required.
Claim. Define the function $h : ℝ → ℝ$ by $h(t) := t^2 / 2$. This quadratic supplies the log-ratio approximation to the J-cost in coordinates $t = ln(x)$ near the fixed point at $t=0$.
background
The module J-Cost Convexity in Log Space examines the J-cost function in logarithmic coordinates. From the module documentation, g(t) = J(e^t) satisfies g(0) = 0, is even, and is positive for t ≠ 0, with the local approximation g(t) ≈ t²/2 near the origin. The declaration introduces h(t) to capture this quadratic behavior explicitly, consistent with the statement that the log-ratio (1/2)(ln x)² belongs to the same cost family as J.
proof idea
The declaration is a direct definition of the quadratic expression t squared over 2 with no lemmas applied and no tactics used.
why it matters
This definition supplies the explicit quadratic form that demonstrates the log-ratio cost shares the fixed point at t=0 and the sign pattern with the J-cost. It supports the structural identity underlying the ALEXIS closed-loop control result and contributes to the Recognition Science forcing chain at the step establishing J-uniqueness and the phi-ladder minimum. The module documentation ties it directly to the closed-loop control identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.