Pith. sign in
theorem

continuumFace_fullTwoJet_normalizedCross_e0Dir

proved
show as:
module
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D
domain
Gravity
line
1818 · github
papers citing
none yet

plain-language theorem explainer

On the axis ray e0=(1,0,0,0), the full two-jet distinct-hinge all-orbit m² moment of the unit-normalized TT cross polarization equals -1/16. Gravity analysts working the Regge–Bloch continuum face cite this as the certified cross value (not the Einstein–Hilbert target -1/4). The proof scales the unnormalized cross certificate by the squared normalization factor and divides by the unit Euclidean norm of e0.

Claim. The full two-jet, distinct-hinge transported all-orbit $m^2$ moment of the normalized cross polarization $\frac{1}{\sqrt{2}}H_{\mathrm{cross}}$ (entries $H_{23}=H_{32}=1$) on the axis direction $e_0=(1,0,0,0)$, divided by $\|e_0\|^2$, equals $-1/16$.

background

In the Regge–Bloch 4D analysis, the continuum face is probed by a transported all-orbit $m^2$ moment of transverse-traceless edge polarizations. Cross is the symmetric matrix with only $H_{23}=H_{32}=1$; plus is $\mathrm{diag}(0,0,1,-1)$. The distinct-hinge full moment folds each hinge-orbit contribution by the inverse orbit-star size and uses the full cosine two-jet $A_0 K_2+A_2 K_0$.

This module closes raw and distinct-hinge certificates on plus and cross against symbol directions and the bare axis ray $e_0=(1,0,0,0)$. Slotwise $K_0=0$ on both polarizations, so full two-jet equals the truncated jet on every direction. On the symbol direction, normalized plus and cross both give raw $-1/8$; on bare $e_0$ they disagree (plus vanishes, cross does not).

Upstream, the full distinct-hinge moment is homogeneous of degree two under $H\mapsto c\cdot H$. A sibling certificate supplies the unnormalized cross value on $e_0$.

proof idea

Rewrite with the smul homogeneity of the full distinct-hinge moment, inserting the factor $(1/\sqrt{2})^2$. Apply the unnormalized cross-on-$e_0$ certificate (value $-1/8$). Replace the denominator by the squared Euclidean norm of $e_0$ (equals 1). Simplify $(1/\sqrt{2})^2$ via inverse-power and square-root cancellation, then close by numeric normalization to $-1/16$.

why it matters

Certifies the normalized continuum-face value of the TT cross mode on the axis ray under the full two-jet: $-1/16$, not the Einstein–Hilbert continuum target $-1/4$. Paired with the companion plus claim (restoration status false: plus stays 0 because $A_2 K_0$ vanishes), it shows the full cosine two-jet does not repair $e_0$ anisotropy or restore plus. Module documentation flags the open isotropy blockage on the axis mode and records that this evaluation does not flip gap_action_recovery. No downstream consumers yet; it is a terminal certificate in the transported all-orbit $M_2$ evaluation stack.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.