module module high

`IndisputableMonolith.Gravity.Analysis.Regge4DSchlaefliPathwise`

Pathwise Schläfli identities and flat closed forms for 4D Regge hinges on the Freudenthal seed. Supplies the flat-seed closed form and directional Schläfli kill that elevate the nonlinear 4D Regge action to an edge Hessian. Cited by anyone assembling the true flat second variation. Argument chains hinge incidence, orbit kernels, dihedral derivatives, and Heron area data into per-path identities.

claimOn the flat Freudenthal 4-simplex seed, for each triangle hinge the pathwise Schläfli identity holds: area-weighted dihedral variations sum to zero along admissible edge paths. The module records flat squared edge lengths, hinge boundary slots $(v_0v_1,v_0v_2,v_1v_2)$, flat hinge area (Heron), and the resulting directional Schläfli kill used to reduce the 4D Regge action at flat.

background

Regge calculus replaces smooth curvature by deficit angles on hinges of a simplicial complex. In 4D the hinges are triangles; the action couples hinge area to deficit. At a flat seed the first variation vanishes and the second variation is an edge Hessian, but only after Schläfli identities eliminate pure dihedral degrees of freedom.

This module sits in the QG full-theory campaign after the Freudenthal incidence layer, the 15-class edge stencil, per-orbit star kernels, and flat Hessian assembly. Upstream, SchlaefliN states the dimension-parametric Schläfli interface; DihedralDerivatives isolates $d\theta=-(1/\sqrt{1-\cos^2\theta}),d(\cos\theta)$ once the Cayley-Menger cosine is differentiable. Hinge kernels supply flat cosine data and orbit classification groups equivalent triangle stars.

Local objects include squared edge 4-tuples, hinge boundary edge slots in fixed vertex order, flat squared lengths on those slots, and Heron evaluation of the flat hinge area (with elementary square-root identities such as $\sqrt{1/4}$ and $\sqrt{1/2}$).

proof idea

Definition-heavy pathwise assembly, not a single wrapper. Flat edge squares are tied to the seed; hinge boundary slots are enumerated and shown trivial in the zero-deficit case. Flat hinge area is evaluated by Heron on those edges. Dihedral cosine kernels at flat are differentiated via the upstream arccos chain rule, then contracted against area gradients along each admissible edge path. Orbit classification ensures each star type is hit once. The resulting path sums cancel (directional Schläfli kill), yielding the flat closed form needed for Hessian reduction. Supporting lemmas are elementary algebraic identities on the seed lengths and square roots.

why it matters in Recognition Science

Gate A2 in 4D mirrors the 3D contract: elevate the true nonlinear Regge action to a Schläfli-reduced edge Hessian. Downstream Regge4DFlatSecondVariation states that in 3D this elevation is already theorem, and that "in 4D the flat-seed Freudenthal flat closed form and flat directional Schläfli kill are THEOREM in Regge4DSchlaefliPathwise." Without those kills the second-variation class would retain provisional weight-1 aggregates rather than true area-weighted deficits.

The module therefore closes the analytic gap between hinge kernels / orbit classification / Hessian assembly and the flat second-variation theorem. It instantiates the n-dimensional Schläfli interface at the 4D Freudenthal seed in pathwise form, which is the precise input the parent second-variation development imports.

scope and limits

Does not treat curved (non-flat) seeds or nonzero deficit backgrounds.
Does not prove the full 4D second-variation theorem; only the Schläfli pathwise ingredients.
Does not redefine the 15-class stencil, Freudenthal incidence, or orbit API.
Does not address Lorentzian signature or continuum limit convergence.
Does not claim a global closed form off the Freudenthal flat seed.

used by (1)

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

IndisputableMonolith.Gravity.Analysis.Regge4DFlatSecondVariation module_import

depends on (6)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.DihedralDerivatives module_import
IndisputableMonolith.Geometry.SchlaefliN module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification module_import

declarations in this module (76)

abbrev SqEdges4 L51
def localEdge L55
def localHinge L56
def flatSqEdges L57
theorem flatSqEdges_eq_seed L59
def hingeBoundarySlots L62
theorem hingeBoundarySlots_zero L75
def hingeFlatEdgeSq L80
def hingeAreaFlat L84
lemma heron_eval L88
lemma sqrt_one_quarter L92
lemma sqrt_half L96
lemma sqrt_three_quarter L101
theorem hingeAreaFlat_0 L107
theorem hingeAreaFlat_1 L113
theorem hingeAreaFlat_2 L119
theorem hingeAreaFlat_3 L125
theorem hingeAreaFlat_4 L131
theorem hingeAreaFlat_5 L137
theorem hingeAreaFlat_6 L143
theorem hingeAreaFlat_7 L149
theorem hingeAreaFlat_8 L155
theorem hingeAreaFlat_9 L161
theorem hingeAreaFlat_pos L167
def flatSchlaefliSummandQ L184
def flatSchlaefliSummand L205
abbrev flatSchlaefliSummandReal L207
lemma univ10 L209
lemma sum10 L213
theorem freudenthal4SimplexFlatSchlaefli L222
theorem freudenthal4SimplexFlatSchlaefli_real L228
theorem seed_hinge_is_zero L234
lemma seed_summand_mul_angle L236
theorem flatSchlaefliSummand_seed_eq_area_angleKernel L241
def flatHingeData L281
def flatSchlaefliData L285
theorem flatSchlaefliIdentity L292
theorem flat_schlaefliN_kills L304
def freudenthal4SimplexFlatSchlaefliPresent L310
theorem freudenthal4SimplexFlatSchlaefliPresent_true L312
def seedDihedralAngle L319
theorem cosDihedral_flat_ne_endpoints L321
theorem arccos_chain_factor_flat L335
theorem coordPath_at_seed L343
theorem hasDerivAt_seedDihedralAngle_coord L350
def affineThroughFlat L376
theorem affineThroughFlat_zero L379
theorem coordPath_eq_affine L384
def flatAngleJacobian L396
theorem flatAngleJacobian_seed L399
def flatDirectionalAngleDeriv L407
lemma mul_div_cancel_area L410
theorem freudenthal4SimplexFlatDirectionalSchlaefli L422
theorem freudenthal4SimplexFlatDirectionalSchlaefli_coord L447
def freudenthal4SimplexFlatDirectionalSchlaefliPresent L457
theorem freudenthal4SimplexFlatDirectionalSchlaefliPresent_true L459
def hingeVertexPerm L469
def hingeVertexPermInv L482
def pullEdgeSlot L495
def remappedSqEdges L517
theorem remappedSqEdges_seed_id L520
theorem remappedSqEdges_zero L524
theorem remapped_seed_dihedral_eq L527
structure Nondeg4Simplex L533
theorem nondeg_flat L540
def seedCosDihedral L548
def freudenthal4SimplexPathwiseSchlaefliPresent L551
theorem freudenthal4SimplexPathwiseSchlaefliPresent_false L553
def Freudenthal4SimplexPathwiseSchlaefliTarget L557
theorem Freudenthal4SimplexPathwiseSchlaefliTarget_open L560
def PathwiseFlatRemainder L567
theorem pathwiseFlatRemainder_flat_zero L576
theorem pathwiseFlatRemainder_directional_zero L600
structure Regge4DSchlaefliPathwiseStatus L608
def regge4DSchlaefliPathwiseStatus L617
theorem regge4DSchlaefliPathwiseStatus_flags L626