lorentzAngleRe
plain-language theorem explainer
Defines the real part of the Lorentzian boost angle on the Wick arc as the constant π, independent of the chart parameter. Used wherever the Lorentzian endpoint of the complex dihedral angle is assembled (cut-limit certificates, action-path mismatches, decoy falsifiers). The body is a frozen constant assignment: principal value of arccos on the ray cos ≤ −1.
Claim. The real part of the Lorentzian hinge boost angle is the constant $\pi$, for every real chart parameter $\alpha$. (Principal value on the branch where the cosine is at most $-1$; the one-sided cut identification is owned by the N4 package, not by this definition.)
background
Module Wave C4 R2 freezes the Wick-action continuation schema for the three-pent 4D object: arc parameter $t=0$ is Lorentzian and $t=1$ is Euclidean. On that object the shared hinge is the all-spacelike triangle ${0,1,2}$, so the three dihedral cosine paths collapse to one chart pair and the deficit is $3\cdot\theta(t)$ with constant real hinge area squared $3/16$.
Complex angles are lifted by $\mathrm{carccos},w:=-I\log(w+I\sqrt{1-w^2})$ (repo half-power square root, never applied to cofactor products). At the Lorentzian end the cosine sits on or beyond the cut $\cos\le -1$, so the principal real part is frozen at $\pi$ while the imaginary part is a rapidity (arcosh of the absolute cosine).
Sibling constants include the Euclidean cosine/angle, the Lorentzian cosine/rapidity, hinge area, and the full complex action path along the arc. This definition supplies only the real Lorentzian angle slot.
proof idea
Pure definitional assignment: ignore the chart parameter and return $\mathrm{Real.pi}$. No lemmas, no tactics. Downstream proofs simply unfold this name (paired with the rapidity sibling) to obtain the complex cut value $\pi+I,\mathrm{arcosh}(11/8)$ at the design point $\alpha=1$.
why it matters
Anchors the Lorentzian endpoint of the complex dihedral angle in the Gap-6 Wick continuation campaign. Downstream cut-limit theorems identify the one-sided $t\to 0^+$ limit of $\mathrm{carccos}$ along the pent-hinge cosine path with $\uparrow(\pi)+I,\uparrow(\mathrm{rapidity})$, and the decisive mismatch lemmas show that the pointwise principal value of $\mathrm{carccos}$ at $t=0$ is not equal to that cut limit.
The same constant enters the repaired certificate structure (interior continuity on $(0,1]$ plus explicit one-sided Tendsto) and the decoy falsifiers: a Euclidean-only real action is killed because the genuine Lorentzian endpoint has nonzero imaginary part built from $2\pi-3\pi$ and the rapidity term. N4 owns the analytic identification of the cut; this definition only freezes the real principal value so those statements typecheck and compare cleanly.
Does not flip any action-level Bool or inhabit the terminal wick_action_continuation_4d Prop; it is schema infrastructure for the frozen design.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.