geometric_ne_arithmetic
plain-language theorem explainer
geometric_ne_arithmetic proves that the geometric mean is strictly unequal to the arithmetic mean for any two distinct positive reals. Researchers deriving simultaneous versus sequential descent in J-cost minimization cite it to separate the two modes. The proof is a short tactic argument that assumes equality, squares both sides, and obtains a contradiction with the distinctness hypothesis via nlinarith.
Claim. For all positive real numbers $n_1, n_2$ with $n_1 ≠ n_2$, $√(n_1 n_2) ≠ (n_1 + n_2)/2$.
background
The module develops log-domain geometry for the reciprocal cost $J(x) = ½(x + x^{-1}) - 1$. It establishes that the geometric mean minimizes total bond cost and that simultaneous descent converges to the geometric mean while sequential descent converges to the arithmetic mean. The present theorem supplies the strict separation required when the two means differ for distinct neighbors. The local setting is the foundation paper F1 on J-cost identities and their consequences for bond graphs.
proof idea
Assume equality. Use Real.sq_sqrt on the nonnegative product to recover the product from the squared square root, then rewrite to obtain the squared average. Apply nlinarith to the resulting identity to conclude that (n1 - n2)^2 = 0. Cast to obtain n1 = n2 and contradict the distinctness hypothesis with linarith. The argument is a direct algebraic contradiction using linear and nonlinear arithmetic tactics.
why it matters
It is invoked directly by simultaneous_differs_from_sequential to separate the two descent modes when neighbors differ. The result fills F1.4.3 in the foundation paper, confirming the strict AM-GM inequality as a structural fact for J-cost geometry. In the Recognition framework it underpins geometric-mean optimality in the phi-ladder and the distinction between simultaneous and sequential processes within the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.