pith. sign in
theorem

Jlog_strictConvexOn

proved
show as:
module
IndisputableMonolith.Cost.Convexity
domain
Cost
line
52 · github
papers citing
1 paper (below)

plain-language theorem explainer

Jlog is strictly convex on the reals. Variational dynamics and annular cost arguments cite it to justify Jensen bounds on total defect for fixed log-charge. The proof rewrites Jlog pointwise as cosh minus one via the prior identity lemma, then transfers strict convexity from cosh by an affine shift.

Claim. The function $J_ {log}(t) := (e^t + e^{-t})/2 - 1$ is strictly convex on $ℝ$.

background

The Cost.Convexity module proves convexity properties of the Recognition cost functions. Jlog is defined as the composition Jcost ∘ exp, where Jcost(x) = ½(x + x^{-1}) - 1 on the positive reals; equivalently Jlog(t) = cosh(t) - 1. This log-domain version is required for the uniqueness step T5 in the forcing chain, which identifies J as the unique function satisfying the Recognition Composition Law with the self-similar fixed point phi.

proof idea

The tactic proof first obtains the extensional equality Jlog = fun t => Real.cosh t - 1 by applying the sibling lemma Jlog_eq_cosh_sub_one. It then rewrites the goal and invokes strictConvexOn_cosh.add_const (-1), which is itself a one-line wrapper around the known strict convexity of cosh on ℝ.

why it matters

The result supplies the strict-convexity ingredient for T5 J-uniqueness. It is invoked in total_defect_lower_bound and eq_constant_config_of_defect_eq to obtain the Jensen lower bound on total defect and the equality case forcing uniform configurations. It is also used in phiCost_convexOn to establish convexity of the annular cost after linear reparametrization by log phi. No open scaffolding remains for this step.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 1 of 1)