jcost_dominates_squared_log
plain-language theorem explainer
J(x) dominates the squared logarithm for x > 0, establishing that the recognition cost functional bounds the Fisher information metric from above. Thermodynamic derivations in the Recognition Science framework cite this to show that Shannon entropy emerges as a quadratic approximation to J-cost. The short proof substitutes the logarithmic change of variables into the elementary cosh inequality.
Claim. For all real $x > 0$, $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(x) ≥ (log x)^2 / 2$.
background
The module derives the relationship between J-cost and Shannon entropy by showing that Gibbs weights arise as the solution to constrained optimization on many-body ledgers. J-cost is the energy functional $J(x) = (x + x^{-1})/2 - 1$. The auxiliary Jlog is defined by Jlog(t) = Jcost(exp t), which equals cosh(t) - 1 by the upstream lemma Jlog_as_cosh. The local setting is the ancestor hierarchy in which J-cost is strictly stronger than log-based entropy.
proof idea
The proof applies the upstream theorem cosh_sub_one_ge_sq_div_two to the argument log x. It equates Jlog(log x) with Jcost x by simplification using exp_log, rewrites via the lemma Jlog_as_cosh, and concludes by exact matching to the inequality.
why it matters
This inequality is invoked by entropyAncestorCert to certify the ancestor relationship and by jcost_div_ge_half_chi_squared to strengthen the divergence comparison. It fills the Ancestor Inequality step in the module's derivation of Gibbs weights from ledger optimization. In the broader framework it shows J-cost is strictly stronger than the log-based entropy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.