gap_diminishing_increments
plain-language theorem explainer
The gap residue satisfies strictly diminishing first differences on non-negative integers: gap(n+2) - gap(n+1) is less than gap(n+1) - gap(n) for every natural n. Modelers of Recognition Science mass ladders or structural residues cite the result to confirm concavity of the zero-parameter f^Rec. The argument lifts the integer claim to the real extension gapR, applies the slope anti-monotonicity property of strict concavity at three consecutive points, simplifies the unit denominators, and rewrites back via the nat-to-real identification.
Claim. For every natural number $n$, $gap(n+2) - gap(n+1) < gap(n+1) - gap(n)$, where $gap(Z) = log(1 + Z/φ) / log φ$ for integer $Z$.
background
The gap function is the Recognition Science structural residue defined by gap(Z) = log(1 + Z/φ) / log φ, serving as the zero-parameter f^Rec in the mass framework. Its real extension gapR is strictly concave on [0, ∞), obtained by composing the logarithm with the affine map x ↦ 1 + x/φ and using the known strict concavity of log on (0, ∞). This analytic behavior is required for the discrete phi-ladder that assigns masses via yardstick · φ^(rung - 8 + gap(Z)).
proof idea
The proof calls strictConcaveOn_gapR_Ici, verifies that n, n+1, n+2 lie in Set.Ici 0, and invokes StrictConcaveOn.slope_anti_adjacent to obtain the slope inequality. It then uses simpa with Nat.cast_add and norm_num to cancel the unit denominators, rewrites the real expressions back to the natural-number form via explicit cast lemmas, and finally applies gapR_nat three times to recover the original gap inequality on integers.
why it matters
The theorem feeds gap_second_difference_neg, which rearranges the inequality to show that the second difference is negative. It supplies the concavity step needed for the gap residue inside the Recognition framework, consistent with the phi fixed-point forcing (T6) and the eight-tick octave (T7). The result guarantees that increments along the integer ladder diminish, supporting the mass formula and the transition from continuous residue to discrete tiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.