same_fixed_point
g and h, defined as the J-cost and its log-ratio approximation in logarithmic coordinates, both vanish at the origin. Researchers establishing the shared fixed point for J-cost convexity in the ALEXIS closed-loop control setting would cite this identity. The proof is a direct term-mode conjunction of the separate zero evaluations for g and h.
claimLet $g(t) := J(e^t)$ where $J$ is the J-cost function, and let $h(t)$ be the log-ratio cost. Then $g(0) = 0$ and $h(0) = 0$.
background
The module proves structural properties of the J-cost in log space as described in the ALEXIS internal note. Here g is the composition g(t) = J(e^t) and h is the quadratic log-ratio approximation, both required to share the fixed point at t = 0 corresponding to x = 1. Upstream g_at_zero states that g(0) = J(e^0) = J(1) = 0, while h_at_zero follows by direct simplification of the definition of h.
proof idea
Term-mode proof that directly pairs the two zero theorems via the constructor for conjunction.
why it matters in Recognition Science
This theorem supplies the shared zero property required by the downstream definition jCostLogSpaceCert, which bundles the zero, evenness, and positivity facts for both g and h. It completes one step of the structural identity showing that J-cost and the log-ratio (1/2)(ln x)^2 share the fixed point at x = 1, the same symmetry J(x) = J(x^{-1}), and the same sign pattern, as stated in the module doc-comment.
scope and limits
- Does not prove evenness or positivity of g or h.
- Does not give the explicit form of g or h away from zero.
- Does not address derivatives or convexity inequalities.
formal statement (Lean)
73theorem same_fixed_point : g 0 = 0 ∧ h 0 = 0 := ⟨g_at_zero, h_at_zero⟩
proof body
Term-mode proof.
74
75/-- Both g and h are even functions. -/