u0_eq_ofReal
plain-language theorem explainer
The limit log-argument u₀(α) equals the real number √(k(α)²−1)−k(α) embedded in ℂ, where k is the Lorentzian cosine scale on the causal range. Downstream lemmas on real/imaginary parts and the complex norm cite this identity. The proof is a short algebraic rewrite of the definition via simp and ring.
Claim. For every real $\alpha$, the complex limit log-argument $u_0(\alpha) := -k(\alpha) + \sqrt{k(\alpha)^2-1}$ equals the complex embedding of the real number $\sqrt{k(\alpha)^2-1} - k(\alpha)$, where $k(\alpha)=(5+6\alpha)/(2+6\alpha)$ is the positive Lorentzian cosine scale.
background
Wave C4 F1 generalizes the fixed α=1 six-lemma cut-limit route to a parameterized causal family under $7/12 < \alpha$. All arguments are pointwise in α; there is no uniform-in-α bound because the Lorentzian scale tends to 1 as α → ∞.
The Lorentzian cosine scale $k(\alpha)=(5+6\alpha)/(2+6\alpha)$ is the absolute value of the Lorentzian cosine on the causal range. The limit log-argument is defined by $u_0(\alpha) := -k(\alpha) + \sqrt{k(\alpha)^2-1}$ as a complex number, matching the sum of the L2 and L3 path limits in the α=1 module. The α=1 specialization recovers the constant $(-11+\sqrt{57})/8$.
The present identity rewrites that two-term complex sum as a single real embedding, which is the form needed for norm and component lemmas.
proof idea
Term-mode proof. Unfold the definition of $u_0(\alpha)$, apply the complex-of-real subtraction identity, then finish by ring, which rearranges $-k + \sqrt{k^2-1}$ into $\sqrt{k^2-1} - k$ under the real embedding. No external lemmas beyond the definition and ofReal_sub.
why it matters
This is the family analogue of the α=1 identity that writes the constant log-argument as a single real. It is the rewrite step used by the family lemmas on the imaginary part (vanishes), the real part, and the complex norm $|u_0(\alpha)| = k(\alpha) - \sqrt{k(\alpha)^2-1}$ under $7/12 < \alpha$.
Those norm and component facts sit inside the parameterized cut-limit succession that generalizes the six-lemma Wick-action route. The module does not yet inhabit the continuation certificate or flip ledger Bools; this lemma is pure algebraic scaffolding for the pointwise causal analysis. Framework context is the gravity seven-gaps stack, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.