geometricMean_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply when the input list is empty.
- Does not prove that the geometric mean is the unique minimizer of total J-cost.
- Does not extend positivity to lists containing zero or negative entries.
- Does not address non-real arguments or complex logarithms.
formal statement (Lean)
113theorem geometricMean_pos {ns : List ℝ} (hns : ∀ n ∈ ns, 0 < n) (hne : ns ≠ []) :
114 0 < geometricMean ns := by
proof body
Term-mode proof.
115 unfold geometricMean
116 exact Real.exp_pos _
117
118/-- **F1.3.2 (two-element case)**: For two positive reals, the geometric mean
119 minimizes the total J-cost. We prove the key fact: at the geometric mean,
120 the J-cost is symmetric in the two neighbors. -/