totalJcost_at_geomean_symmetric
plain-language theorem explainer
For two positive reals n1 and n2 the J-cost evaluated at the ratios to their geometric mean is identical. Foundation paper F1 cites this symmetry to establish that the geometric mean minimizes total bond cost. The tactic proof rewrites both sides via the squared-ratio form of J-cost then closes equality by field simplification and nlinarith on the shared product identity.
Claim. Let $n_1,n_2>0$. Let $g=√(n_1 n_2)$. Then $J(g/n_1)=J(g/n_2)$, where $J(x)=½(x+x^{-1})-1$.
background
Module F1 develops the log-domain geometry of the canonical reciprocal cost $J(x)=½(x+x^{-1})-1$. The supporting squared-form identity $J(x)=(x-1)^2/(2x)$ for $x≠0$ is supplied by the upstream Jcost_eq_sq lemma. The reciprocal automorphism and ledger-factorization structures supply the algebraic rules for ratios and inverses used throughout the module.
proof idea
The proof first records positivity of the product and geometric mean, then nonzeroness of the two ratios. It rewrites both sides with Jcost_eq_sq, substitutes the identity gm²=n1 n2, applies field_simp, and finishes with nlinarith on the nonnegativity of the two squared differences.
why it matters
This supplies the two-element symmetry fact required by F1.3.2 for the geometric-mean optimality claim. It feeds the parent result totalJcost_minimized_at_geometric_mean in the same module. Within Recognition Science it anchors the log-domain geometry cited by NS, P vs NP, and Yang-Mills.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.