JCostLogSpaceCert
plain-language theorem explainer
JCostLogSpaceCert bundles the zero, evenness, strict positivity of g(t) = J(e^t) and the nonnegativity of its quadratic approximation h(t) = t²/2 in logarithmic coordinates. A physicist working on closed-loop control or the ALEXIS result would cite the certificate to confirm that the exact J-cost and the log-ratio share the origin fixed point together with even symmetry. The structure is introduced by directly listing the properties already established in the sibling lemmas g_even, h_even and h_nonneg.
Claim. Let $g(t) := J(e^t)$ with $J(x) = (x + x^{-1})/2 - 1$ and let $h(t) := t^2/2$. The structure JCostLogSpaceCert consists of the assertions $g(0)=0$, $g(t)=g(-t)$ for all real $t$, $g(t)>0$ for $t≠0$, $h(0)=0$, $h(t)=h(-t)$, $h(t)≥0$ for all real $t$, together with the shared fixed-point and even-symmetry statements.
background
In the JCostConvexityInLogSpace module the J-cost is transformed to logarithmic coordinates via $t=ln x$. The function g is defined by g(t)=J(e^t) and inherits evenness g(t)=g(-t) from the inversion symmetry of J. The auxiliary function h is the quadratic log-ratio approximation h(t)=t²/2, which is manifestly even and nonnegative by direct expansion. The module document states that both functions share the unique global minimum at the origin and the same sign pattern, establishing the structural identity required for the ALEXIS closed-loop control result.
proof idea
The structure JCostLogSpaceCert is introduced as a record type whose fields are populated directly by the theorems g_even, h_even, h_nonneg together with the zero and positivity statements for g and h. No tactics are applied inside the structure declaration itself; it simply assembles the already-proved properties.
why it matters
This certificate is consumed by the definition jCostLogSpaceCert, which in turn supports the ALEXIS closed-loop control analysis described in the module documentation. It encodes the key observation that the J-cost and the log-ratio (1/2)(ln x)² share the fixed point at x=1, the inversion symmetry J(x)=J(x^{-1}), and the positivity pattern away from the minimum. Within Recognition Science this supplies the convexity foundation in log space that underpins the phi-ladder mass formula and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.