sq_sub_one_limit
plain-language theorem explainer
Exact complex arithmetic: $(11/8)^2 - 1 = 57/64$. Cited by the cut-limit square-root tendsto and the eventual nonvanishing of $z^2-1$ along the pentagonal hinge path. Proof is a one-line `norm_num` evaluation.
Claim. As complex numbers, $\bigl(\tfrac{11}{8}\bigr)^2 - 1 = \tfrac{57}{64}$.
background
Module Wave C4 N4 builds the cut-boundary limit of complex arccosh along a pentagonal hinge cosine path, aiming at carccos_tendsto_at_cut_one and the Lorentz anchor at one via a six-lemma route. It does not close the gap6 terminal or flip ledger Bools.
Along that path the relevant complex value approaches $11/8$. The identity here records the exact value of $z^2-1$ at that point, namely $57/64$, which is the radicand fed to the principal complex square root in the cut-limit analysis. Downstream, $\sqrt{57/64}=\sqrt{57}/8$ becomes the claimed limit point of csqrt along the path.
proof idea
One-line wrapper: norm_num evaluates the rational arithmetic $(11/8)^2-1=121/64-64/64=57/64$ in $\mathbb{C}$.
why it matters
Supplies the exact radicand used by tendsto_csqrt_sq_sub_one_one, which asserts
$$\mathrm{Tendsto},t\mapsto\mathrm{csqrt}(\mathrm{pentHingeCosPath},1,t^2-1)\to\sqrt{57}/8$$
along the right neighborhood of zero, and by eventually_sq_sub_one_ne, which keeps that radicand off zero so the square-root branch is well-defined.
Those two results sit on the L1–L6 spine that lands the carccos cut-boundary limit and the Lorentz anchor at one. Within Recognition gravity this is bookkeeping for the Wick-rotated action cut, not a forcing-chain step (T0–T8) or an RCL identity; it simply pins the numerical hinge value that the complex-analytic limit needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.