strictConcaveOn_gapR_Ici
plain-language theorem explainer
gapR(x) := log(1 + x/phi)/log phi is strictly concave on [0, ∞). Researchers deriving mass ladders or discrete increments in Recognition Science cite this to control the second differences of the structural residue. The proof reduces the claim to the known strict concavity of the logarithm by composing with the injective affine map h(x) = 1 + x/phi and scaling by the positive constant 1/log phi.
Claim. The function $gapR(x) = log(1 + x/φ) / log φ$ is strictly concave on the interval $[0, ∞)$.
background
The module establishes analytic properties of the structural residue gap(Z) = log(1 + Z/φ) / log φ, the zero-parameter Recognition-side function f^Rec used in the mass framework. gapR is its real extension to the non-negative reals. Upstream, one_lt_phi supplies 1 < φ and phi_pos supplies φ > 0; these guarantee that the affine reparametrization h(x) = 1 + x/φ maps [0, ∞) into (0, ∞) and that the scaling factor 1/log φ is positive. The proof also invokes the Mathlib fact that log is strictly concave on (0, ∞).
proof idea
The tactic proof first records strictConcaveOn_log_Ioi. It builds the affine map h(x) = 1 + x/φ, proves that h sends Ici 0 into Ioi 0 and is injective there, then shows that log ∘ h is strictly concave on Ici 0 by transporting the concavity inequality through the affine combination. Finally it multiplies the resulting strict inequality by the positive constant 1/log φ and rewrites every occurrence of gapR via the definitional unfolding gapR t = (1/log φ) · log(h t).
why it matters
The result is invoked directly by gap_diminishing_increments to obtain the discrete slope inequality gap(n+2) - gap(n+1) < gap(n+1) - gap(n). Within the Recognition framework it supplies the analytic justification for the phi-ladder residue that appears in the mass formula yardstick · φ^(rung-8+gap(Z)). It closes one link in the chain from T5 (J-uniqueness) through the self-similar fixed point φ to the concrete gap function used in nucleosynthesis and large-scale structure derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.