arithmeticMean
plain-language theorem explainer
The arithmetic mean of two real numbers is defined as their sum divided by two. Researchers analyzing J-cost geometries cite it to mark the limit of sequential single-bond descent. It is contrasted with the geometric mean to separate simultaneous and sequential update paths. The definition is a direct algebraic expression with no lemmas or tactics.
Claim. For real numbers $n_1$ and $n_2$, the arithmetic mean is given by $(n_1 + n_2)/2$.
background
This definition sits in the F1 log-domain J-cost geometry module. The J-cost function is $J(x) = 1/2(x + x^{-1}) - 1$, which quantifies reciprocal deviation from unity. The module collects identities from JcostCore and proves geometric-mean optimality together with the distinction between simultaneous and sequential descent paths.
proof idea
The declaration is a one-line definition that directly encodes the standard arithmetic-mean formula. No lemmas are applied and no tactics are used; the body is simply the expression $(n_1 + n_2)/2$.
why it matters
The definition is invoked by simultaneous_differs_from_sequential, which shows sequential descent converges to the arithmetic mean while simultaneous descent converges to the geometric mean for distinct positive reals. It fills the F1.4.2 slot in the foundation paper and supplies the target point needed to separate the two descent modes in J-cost geometry. The distinction supports the broader forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.