sub_one_eq_mul_ratio
plain-language theorem explainer
The algebraic identity rewrites the deviation H(t) minus one as a product of t squared and the normalized second difference for any function satisfying H zero equals one. Analysts handling limits of the shifted cost near the origin in the T5 uniqueness argument cite this rearrangement. The proof splits on whether t vanishes, substituting the normalization hypothesis at zero and canceling factors via field simplification otherwise.
Claim. For any function $H : ℝ → ℝ$ with $H(0) = 1$ and any real $t$, $H(t) - 1 = (t^2 / 2) · (2 (H(t) - 1) / t^2)$.
background
In Recognition Science the shifted cost is introduced as $H(x) = J(x) + 1$ where $J(x) = ½(x + x^{-1}) - 1$, converting the Recognition Composition Law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The module supplies helper lemmas for the T5 cost-uniqueness proof that isolates this functional equation under the normalization $H(0) = 1$, which follows at once from $J(1) = 0$. The upstream CostAlgebra definition states: 'The shifted cost: H(x) = J(x) + 1 = ½(x + x⁻¹). Under H, the RCL becomes the standard d'Alembert equation.'
proof idea
The tactic proof opens with by_cases on t = 0. The zero branch substitutes the hypothesis H 0 = 1 and simplifies to the trivial identity. The nonzero branch applies field_simp to cancel the common t² factors on the right-hand side.
why it matters
The lemma is invoked by tendsto_H_one_of_log_curvature to control the approach of H to 1 as t tends to 0 under the HasLogCurvature hypothesis. It therefore supplies an algebraic step inside the T5 J-uniqueness argument of the forcing chain, where the second-order curvature term is isolated before extracting the self-similar fixed point phi. The identity closes a small gap between the functional equation and the limit statements needed for the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.