gapR
plain-language theorem explainer
gapR extends the integer structural residue to real arguments via the explicit logarithmic ratio involving the golden ratio. Analysts working on concavity and increment properties within the Recognition Science mass framework cite this extension to enable real-domain arguments. The definition is supplied directly as a noncomputable expression that agrees with the discrete gap on naturals.
Claim. $gapR(x) = log(1 + x/φ) / log φ$ for $x ∈ ℝ$, where $φ$ is the golden ratio.
background
The module develops Lean-checked properties of the structural residue gap(Z) = log(1 + Z/φ) / log φ, proposed as the zero-parameter Recognition-side residue f^{Rec} used in the mass framework. gapR supplies the real extension required for analytic statements such as strict concavity on [0, ∞). The local setting treats gap as definitional, permitting direct verification of algebraic and analytic behavior without external kernels; phi is the self-similar fixed point imported from Constants.
proof idea
The declaration is a direct definition that writes gapR(x) as the ratio of the natural logarithm of (1 + x/phi) to the natural logarithm of phi. No lemmas or tactics are invoked; the expression itself serves as the base for downstream results.
why it matters
gapR underpins gapR_nat, strictConcaveOn_gapR_Ici, and gap_diminishing_increments in the same module. It supplies the real extension needed to verify the residue's concavity and diminishing increments, supporting the mass formula on the phi-ladder and the claim that gap acts as a zero-parameter f^{Rec}. This connects to the forcing chain landmarks T5 (J-uniqueness) and T6 (phi fixed point) while closing the analytic side of the residue definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.