unit_is_selected_by_minimality_over_powers
plain-language theorem explainer
For every positive real base other than one and every integer exponent at least two, recognition cost of the base is strictly smaller than cost of that power. Anyone proving the unit is the unique least-cost generator of the nondegenerate power family cites this comparison. The argument is a one-line term wrapper around the already-proved strict power inequality.
Claim. For all real $x > 0$ with $x \neq 1$ and all natural numbers $n \geq 2$, $J(x) < J(x^n)$, where $J(t) = (t + t^{-1})/2 - 1$ is the recognition cost on positive reals.
background
The recognition cost on positive reals is $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$. It is the unique continuous solution of the Recognition Composition Law forced at T5 of the unified forcing chain, vanishes only at the unit $x = 1$, and is symmetric under inversion: $J(x) = J(x^{-1})$.
This module isolates how $J$ selects the unit among power families. The nondegenerate power family of a base $x$ consists of the points $x^m$ for exponents $m \geq 1$; exponent zero is excluded because it yields the identically zero cost. The local goal is to show the base itself is strictly cheaper than every higher power, so specializing the base to one makes the unit the unique least element under the pointwise order.
Upstream, the strict inequality for powers is already proved by trichotomy on $x < 1$ versus $x > 1$, reducing the sub-unit case via $J$-symmetry and the identity relating $J(x^n)$ to $J((x^{-1})^n)$.
proof idea
One-line term wrapper: the proof is the lambda that applies jcost_lt_pow at the same hypotheses $(x > 0)$, $(x \neq 1)$, and $(n \geq 2)$. No extra case split or algebraic work occurs here; all content lives in that upstream lemma, which removes the odd-parity restriction from the earlier odd-power comparison and handles $x < 1$ by inversion.
why it matters
In Recognition Science the cost $J$ is forced at T5 (J-uniqueness) from the Recognition Composition Law; once $J$ is fixed, minimality statements identify the unit as the unique zero-cost and least-cost generator. This theorem is the comparison engine for the power-family classification in the same module: it feeds the predicate that an exponent-$n$ member is least in the nondegenerate power family, and the equivalence that least power-cost holds precisely for the canonical unit case.
No downstream consumers are wired yet in the dependency graph, so the result presently closes a local scaffolding step rather than a named parent theorem. It sits beside the odd-power variants and the least-element characterizations, completing the parity-free form the corrected classification needs. Framework landmarks touched: T5 J-uniqueness and the RCL-derived cost; no direct claim on phi, the eight-tick octave, or $D = 3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.