gap_second_difference_neg
plain-language theorem explainer
The theorem proves that the gap function on integers satisfies gap(n+2) + gap(n) < 2*gap(n+1) for every natural number n, establishing strict negativity of the second difference. Researchers constructing the Recognition Science mass ladder for fermion bands would cite it to confirm concavity of the zero-parameter residue. The proof is a one-line wrapper that applies the diminishing-increments lemma and rearranges via linear arithmetic.
Claim. For every natural number $n$, $g(n+2) + g(n) < 2 g(n+1)$, where $g(Z) = log(1 + Z/φ)/log φ$ and $φ$ denotes the golden ratio.
background
The module supplies Lean-verified algebraic properties of the structural residue $g(Z) = log(1 + Z/φ)/log φ$, presented as the zero-parameter Recognition-side residue $f^{Rec}$ used in the mass framework. This function supplies the adjustment term on the phi-ladder for canonical Z-values 24, 276 and 1332 that label the three fermion bands. The present result depends on the sibling lemma gap_diminishing_increments, which asserts that the first forward differences of $g$ are strictly decreasing on the non-negative integers.
proof idea
The proof calls gap_diminishing_increments (n := n) to obtain the first-difference inequality g(n+2) - g(n+1) < g(n+1) - g(n), then invokes linarith to rearrange the relation into the claimed second-difference form.
why it matters
The theorem certifies strict concavity of the gap residue on the non-negative integers, thereby supporting its use as a diminishing increment in the phi-ladder mass formula. It belongs to the numerical interval bounds section that prepares certified values at the canonical Z-points 24, 276, 1332. Within the Recognition framework it reinforces the self-similar fixed-point structure (T6) and the yardstick scaling of masses by phi-powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.