gap_276_lt_gap_1332
plain-language theorem explainer
The structural residue satisfies gap(276) < gap(1332) for the Recognition Science display function. Researchers ordering masses on the phi-ladder or assigning particle tiers cite this to confirm that larger Z yields strictly larger residue. The proof is a one-line wrapper that invokes the strict monotonicity of gap on non-negative integers together with a decidable comparison.
Claim. Let $gap(Z) = log(1 + Z/φ) / log φ$. Then $gap(276) < gap(1332)$.
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. This definition appears directly in the module header and is the same residue whose derivation is recorded in Gap45.Derivation.gap as the product of closure and Fibonacci factors. The local setting is the phi-ladder mass formula, where gap(Z) supplies the rung offset after the base phi^(-8) scaling.
proof idea
The tactic obtains the lemma gap_strictMono_on_nonneg, records the decidable fact that 276 < 1332 as naturals, and applies the lemma via simpa. No further rewriting or case analysis is required.
why it matters
The inequality supplies a concrete instance of the monotonic ordering required by the phi-ladder mass assignments (T6 self-similar fixed point and T7 eight-tick octave). It closes part of the analytic verification that gap increases with Z, supporting downstream use in mass spectra and tier assignments even though no direct used_by edges are recorded yet. The result is independent of the specific upstream structures (NucleosynthesisTiers, LedgerFactorization, SpectralEmergence) that appear in the dependency list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.