geometricMean_pos
plain-language theorem explainer
The declaration proves that the geometric mean of any non-empty list of positive real numbers is positive. Researchers establishing optimality of the geometric mean for total J-cost in log-domain geometries cite it to guarantee that the candidate minimizer lies in the positive reals. The proof is a one-line term reduction that unfolds the exponential definition and applies the strict positivity of the real exponential function.
Claim. Let $ns$ be a non-empty list of positive real numbers. Then the geometric mean defined by $ns$ satisfies $0 < {ns} > 0$, where the geometric mean is the exponential of the average of the logarithms: $0 < {ns} = {ns} > 0$.
background
The module develops the log-domain geometry of the canonical J-cost $J(x) = (x + x^{-1})/2 - 1$, equivalently $J(e^ε) = cosh(ε) - 1$. The geometric mean of a list of positive reals is introduced as the quantity that simultaneously minimizes total bond cost under the Recognition Composition Law. Its definition is the exponential of the average of the logarithms of the list entries, which is well-defined precisely when the list is non-empty and all entries are positive.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of geometricMean to expose the outer Real.exp applied to the average of the logs, then invokes the library fact that the exponential function is strictly positive on the reals.
why it matters
The result supplies the positivity needed for the geometric-mean optimality theorem (totalJcost_minimized_at_geometric_mean) in the F1 foundation paper. It closes the basic positivity step required before one can compare simultaneous versus sequential descent or invoke the geometric mean inside the eight-tick octave and phi-ladder constructions. No open scaffolding remains for this elementary fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.