H_one_of_normalized
plain-language theorem explainer
If a real-valued function F satisfies the normalization condition F(1) = 0, then the shifted reparametrization H_F evaluates to 1 at the origin. This auxiliary result appears inside the Aczel classification package and is invoked when establishing uniqueness of the kernel for the J-cost. The proof is a direct simplification that unfolds the definitions of H and G after extracting the normalization hypothesis.
Claim. Let $F : ℝ → ℝ$ satisfy $F(1) = 0$. Then $H_F(0) = 1$, where $H_F(t) := F(e^t) + 1$.
background
The AczelClassification module supplies the regularity bridge for the d'Alembert forcing chain. It isolates consequences of the Aczel theorem so downstream uniqueness statements can cite a calibrated kernel without invoking the raw classification axiom directly. IsNormalized is the condition $F(1) = 0$. The reparametrized operator H applied to F is defined by $H_F t = F(e^t) + 1$, which shifts the G reparametrization $G_F t = F(e^t)$.
proof idea
The proof first extracts the equality $F(1) = 0$ from the IsNormalized hypothesis using simpa. It then applies simp with the definitions of H, G, and the extracted equality to reduce the goal $H_F 0 = 1$ directly.
why it matters
This lemma supplies the base value $H_F 0 = 1$ inside primitive_to_uniqueness_of_kernel, the public T5 statement establishing uniqueness of the J-cost kernel under PrimitiveCostHypotheses. It closes the calibration step in the Aczel package that feeds the eight-tick octave and D=3 forcing chain. The module doc notes that this allows downstream exclusivity code to depend on the kernel without touching the raw Aczel axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.