minus_one_step_forces_phi_shift
plain-language theorem explainer
The theorem shows that the three normalization conditions g(0)=0, g(1)=1, g(-1)=-2 on the affine-log family g(x)=a log(1+x/b)+c force the scale parameter b to equal the golden ratio φ whenever b>1. Mass-ladder and gap-function derivations in Recognition Science cite this step to justify the canonical form gap(Z)=log_φ(1+Z/φ). The proof extracts c=0, converts the remaining conditions into a logarithmic relation, combines them into a product identity that equals 1, clears denominators to obtain the quadratic b²-b-1=0, and selects the root φ using
Claim. Let $g(x)=a·log(1+x/b)+c$. Assume $1<b$, $g(0)=0$, $g(1)=1$, and $g(-1)=-2$. Then $b=φ$.
background
The module examines the affine-log candidate family $g(x)=a·log(1+x/b)+c$ inside the Recognition Science bridge from multiplicative J-costs to additive rung shifts on the φ-ladder. Module documentation states that three normalization conditions uniquely fix the parameters: g(0)=0 forces c=0, g(-1)=-2 with b>1 forces b=φ, and g(1)=1 forces a=1/log(φ). This lemma isolates the forcing of b. It draws on the upstream lemmas one_lt_phi (establishing φ>1) and phi_sq_eq (φ²=φ+1) together with basic real-arithmetic facts such as lt_trans and mul_eq_zero.
proof idea
The tactic proof first obtains c=0 from the g(0)=0 hypothesis. It rewrites the g(1)=1 and g(-1)=-2 conditions as a·log(1+1/b)=1 and a·log(1-1/b)=-2. Algebraic rearrangement produces the relation log(1-1/b)=-2·log(1+1/b). Adding the identity log((1+1/b)²)=2·log(1+1/b) yields log((1-1/b)·(1+1/b)²)=0, so the product equals 1. Clearing the denominator b² produces the quadratic b²-b-1=0. The proof then invokes phi_sq_eq to note that φ satisfies the same equation and uses one_lt_phi plus the assumption b>1 to discard the extraneous root.
why it matters
The result supplies the central step inside the three-point calibration theorems affine_log_parameters_forced and three_point_forces_canonical_gap (and their counterparts in the Masses module). It thereby pins the canonical gap function gap(Z)=log_φ(1+Z/φ) used for mass formulas on the φ-ladder. Within the Recognition Science framework it realizes the self-similar fixed-point forcing of φ (T6) into the cost-to-rung conversion. The uniqueness is proved only inside the affine-log family; the module documentation notes that this family being the correct bridge remains a structural postulate motivated by the logarithmic nature of the conversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.