module module moderate

`IndisputableMonolith.Gravity.Analysis.Regge4DSchlaefliPathwise`

Pathwise Schläfli identities for 4D Regge triangle hinges at the flat Freudenthal seed: flat closed form and directional Schläfli kill. Gravity analysts cite it when elevating the nonlinear 4D Regge action to an edge Hessian. The argument wires hinge incidence, orbit classes, Heron areas, and dihedral derivatives into explicit flat evaluations.

claimOn each 4D Freudenthal triangle hinge at the flat seed, the Regge hinge contribution admits a closed-form flat evaluation, and the directional Schläfli residual along edge-length variations vanishes (pathwise Schläfli kill). Boundary edge slots of a hinge are ordered $(v_0v_1, v_0v_2, v_1v_2)$; flat squared edge lengths and Heron hinge area are evaluated explicitly.

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. The classical Schläfli identity relates area variations to dihedral-angle variations and is the standard route from the nonlinear action to a second-variation (Hessian) form on edge lengths.

This module sits in the QG full-theory campaign after the Freudenthal hinge incidence layer, the 15-class edge stencil, per-orbit star kernels, and dihedral-cosine kernels at flat. Upstream SchlaefliN supplies a 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. Local objects include squared edge 4-tuples, hinge boundary slots, flat edge squares, and Heron area at flat (with elementary square-root evaluations such as $\sqrt{1/4}$ and $\sqrt{1/2}$).

proof idea

Definition-heavy pathwise assembly, not a single wrapper. Flat squared edges are identified with the seed configuration; hinge boundary slots fix the three triangle edges in order $(v_0v_1,v_0v_2,v_1v_2)$. Flat hinge area is obtained from Heron on those edges. Dihedral data at flat come from the imported 4D hinge dihedral kernel; orbit classification supplies the combinatorial star types. The module then evaluates the flat closed form of the hinge contribution and shows the directional Schläfli residual kills along edge variations, using the n-dimensional Schläfli interface specialized to the 4D hinge setting and the standard arccos derivative chain.

why it matters in Recognition Science

Gate A2 in 4D needs a Schläfli-reduced edge Hessian for the true nonlinear Regge action. Downstream Regge4DFlatSecondVariation states explicitly that the flat-seed Freudenthal closed form and flat directional Schläfli kill are theorems in this module, mirroring the 3D elevation trueReggeAction_secondVariation_flat_schlaefli. Without those kills, the Hessian assembly in ReggeFlat4DHessianAssembly cannot replace provisional weight-1 aggregates by true second variation.

ReggeFoldSchlaefliBookkeeping4D also imports this module for Arc 2 fold-to-action Schläfli bookkeeping (frozen factor propositions). In the broader RS gravity stack this is the analytic bridge from combinatorial hinge kernels to a usable 4D flat second variation, not a foundational T0–T8 step.

scope and limits

Does not prove the full nonlinear 4D Regge second variation away from the flat seed.
Does not redefine Freudenthal incidence, 15-class stencils, or orbit APIs; imports them only.
Does not establish continuum GR recovery or physical units; stays in discrete Regge edge variables.
Does not discharge 3D tetrahedral Schläfli; that is a separate instantiation of SchlaefliN.
Does not claim global topology or boundary terms beyond pathwise hinge identities.

used by (2)

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

IndisputableMonolith.Gravity.Analysis.Regge4DFlatSecondVariation module_import
IndisputableMonolith.Gravity.Analysis.ReggeFoldSchlaefliBookkeeping4D 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