Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.WickActionEuclidSchlaefli

show as:
view Lean formalization →

Analytic core for the Euclidean-model side of the 4d Wick-action Schläfli identity: domain lemmas put the model cosine strictly in (-1,1) for causal α > 7/12, then differentiate the cosine, the spherical area functional, and the dihedral angle. Gravity/QG campaign authors cite it when assembling the carccos continuation certificate. Proofs are calculus: chain rule, field_simp, and the standard arccos derivative from DihedralDerivatives.

claimFor causal hinge parameter $\alpha$ strictly above the cut $7/12$, the Euclidean model cosine $c_E(\alpha)$ lies in $(-1,1)$. The module supplies $c_E'(\alpha)$, the Euclidean area functional $A_E(\alpha)$ with derivative $A_E'$, and the dihedral angle $\theta_E=\arccos(c_E)$ with $\theta_E'=-(1/\sqrt{1-c_E^2})\,c_E'$, the Euclidean half of the Schläfli identity used in the Wick continuation.

background

Part of the Gravity SevenGaps full-theory campaign (Wave C4), this module sits between the frozen Wick-action continuation schema and certificate assembly. Upstream, WickActionInteriorHinge freezes the 4d continuation target and the complex arccos lift (N1+N2); WickActionInteriorHingeConfinement closes Moebius confinement and the Lorentzian cut-boundary story (N3+N4). The Euclidean model cosine is the real counterpart that must stay off the arccos branch cut.

DihedralDerivatives isolates the pure analytic step: once a Cayley-Menger cofactor cosine is differentiable, the angle $\theta=\arccos(\cos\theta)$ obeys $d\theta=-(1/\sqrt{1-\cos^2}),d(\cos\theta)$. The module doc stresses the honest domain: causal $\alpha$ forces the Euclidean model cosine into $(-1,1)$; at the lower edge $\alpha=7/12$ one has cosine $=1$ (the cut), so strict inequality is required.

Sibling lemmas cover denominator positivity, membership in the open unit interval, $|c_E|<1$, positivity of $1-c_E^2$, elementary product/difference derivative rules, hasDerivAt for the cosine and area, and the named angle derivative equality.

proof idea

Not a single theorem: a ladder of real-analysis lemmas. First, algebraic positivity and non-vanishing of the Euclidean-cosine denominator, then $c_E(\alpha)\in(-1,1)$ and $|c_E|<1$ on the strict causal range, hence $1-c_E^2>0$. Elementary HasDerivAt facts for $x\mapsto ax-b$ and $x\mapsto b-ax$ feed a chain-rule proof that $c_E$ is differentiable. The area functional is differentiated the same way. The angle derivative is the standard arccos formula from DihedralDerivatives applied to $c_E'$, packaged as euclidAngle_deriv_eq. Tactics are field_simp, linarith, ring, and Mathlib derivative lemmas; no geometric axioms beyond the imported cosine definition.

why it matters in Recognition Science

Closes the Euclidean analytic half of Wave C4 R4 (Wick action / Schläfli). Downstream, WickActionCertAssembly (R5) binds the pointwise complex arccos value at $\alpha=1$ against the N4 cut limit $\pi+I\cdot\mathrm{arcosh}(11/8)$ and needs these real derivatives as the Euclidean comparison side. WickActionEuclidSchlaefliAudit axiom-audits the headline theorems of this module against the kernel set {propext, Classical.choice, Quot.sound}.

In the broader RS gravity program this is scaffolding for the full-theory ledger pillar on Wick-continued 4d action: without a machine-checked Euclidean angle/area derivative off the arccos cut, the Lorentzian continuation certificate cannot be assembled. It does not itself flip a FullTheoryLedger flag; it supplies the calculus the assembly and audit modules import.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (24)