simultaneous_differs_from_sequential
plain-language theorem explainer
The theorem shows that for any two distinct positive reals the geometric mean differs from the arithmetic mean, which separates simultaneous descent (converging to the geometric mean) from sequential single-bond descent (converging to the arithmetic mean) in log-domain J-cost geometry. Researchers citing the F1 foundation paper on J-cost identities or the Recognition Composition Law would reference this distinction when analyzing bond-cost minimization. The proof is a one-line wrapper that directly invokes the strict AM-GM inequality already on
Claim. For positive real numbers $n_1$ and $n_2$ with $n_1 ≠ n_2$, the geometric mean satisfies $√(n_1 n_2) ≠ (n_1 + n_2)/2$.
background
The module develops log-domain geometry for the canonical J-cost $J(x) = ½(x + x^{-1}) - 1$. The arithmetic mean is defined as $(n_1 + n_2)/2$ and represents the limit of sequential descent along individual bonds. The geometric mean $√(n_1 n_2)$ is the simultaneous-descent fixed point. The upstream Composition axiom (Recognition Composition Law) states that for positive $x,y$ the functional equation $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ holds; this forces compatibility with multiplicative structure and underpins the mean identities. The sibling theorem geometric_ne_arithmetic supplies the strict inequality between the two means.
proof idea
The proof is a one-line wrapper that applies the geometric_ne_arithmetic lemma to the supplied hypotheses. That lemma proceeds by contradiction: assume equality, square both sides to obtain $4n_1 n_2 = (n_1 + n_2)^2$, expand the right-hand side, and reach $0 = (n_1 - n_2)^2$, contradicting the distinctness hypothesis.
why it matters
This fact completes the geometric_mean_ne_arithmetic_mean item listed among the module's main results and supplies the separation between simultaneous and sequential descent required by the F1 paper. It is cited in the Recognition framework for NS, P vs NP, Yang-Mills, and the frustrated-phase variant of the Riemann hypothesis. The distinction rests on the J-uniqueness and phi-fixed-point steps of the forcing chain and on the eight-tick octave structure that organizes bond costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.