Jphi_numerical_band
plain-language theorem explainer
The theorem proves that the recognition cost J at the golden ratio satisfies 0.11 < J(φ) < 0.12. Researchers certifying visual beauty scores in Recognition Science cite this numerical interval to anchor the asymmetric minimum of the beauty function. The proof is a short algebraic reduction that substitutes the closed-form J(φ) = φ − 3/2 and applies the supplied bounds on φ together with real arithmetic.
Claim. $0.11 < J(φ) ∧ J(φ) < 0.12$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost and $φ$ is the golden ratio.
background
In the VisualBeauty module the beauty score of a composition (a, b) is defined by B(a, b) := −J(a/b), where J is the canonical recognition cost. This score is bounded above by zero and equals zero precisely when a = b (perfect symmetry). At the golden-ratio ratio a/b = φ the score equals 3/2 − φ ≈ −0.118, as stated in the upstream theorem beautyScore_at_phi.
proof idea
The proof first obtains the identity Jcost phi = phi − 3/2 by unfolding beautyScore_at_phi, rewriting the division by one, and closing with linarith. It then imports the two constant lemmas 1.61 < phi and phi < 1.62. The target interval is recovered by substituting the identity and applying linarith to the resulting real inequalities.
why it matters
Jphi_numerical_band supplies the numerical band required by the master certificate visualBeautyCert and by the one-statement theorem visual_beauty_one_statement. It completes the visual-aesthetics closure that parallels the musical-scale derivation, confirming that the J-minimizing asymmetric ratio lies inside the interval predicted by the J-uniqueness and phi fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.