gap_strictMono_on_nonneg
plain-language theorem explainer
gap(n) := log(1 + n/φ) / log φ is strictly increasing for n in the non-negative integers. Mass ladder calculations in Recognition Science cite this to order residues at Z = 24, 276, 1332 and beyond. The tactic proof reduces the claim to the strict increase of the logarithm on positive reals after scaling by the positive constant log φ, using the definition of gap and basic inequalities on division.
Claim. The map $nmapsto log(1 + n/φ)/log φ$ from the non-negative integers to the reals is strictly monotonic.
background
In the RSBridge module the structural residue is given explicitly by gap(Z) = log(1 + Z/φ) / log φ. This expression serves as the Recognition-side counterpart to RG residues and appears in the mass formula as the rung adjustment on the phi-ladder. The module establishes its monotonicity, concavity, and ordering properties to support deterministic mass predictions. Upstream, one_lt_phi guarantees log φ > 0, while structures from PhiForcingDerived and SpectralEmergence supply the context for J-cost and gauge content that motivate the gap definition. The setting is zero-parameter verification of gap behavior, as stated in the module documentation.
proof idea
Tactic proof begins by introducing a < b, then constructs positivity of 1 + a/φ from zero_le on naturals and div_nonneg. It shows the scaled arguments increase via div_lt_div_of_pos_right, applies Real.log_lt_log to obtain the log inequality, divides by the positive log φ (from one_lt_phi and Real.log_pos), and concludes by simpa with the gap definition.
why it matters
This theorem directly enables the concrete comparisons gap_24_lt_gap_276 and gap_276_lt_gap_1332 in the same module. Those results confirm the ordering of gaps at key structural integers tied to the 24 chiral flavors and higher tiers. Within the framework it reinforces the phi-forced self-similarity (T6) and the discrete ladder structure leading to D=3 dimensions, closing part of the gap properties needed for mass spectrum calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.