Geometry Regge Action Nonlinear Hessian Proof Second Product Rule Equals Canonic

/-- Final geometric identity after the second product rule: the second
product-rule expression at the flat point is the canonical Hessian quadratic
form. -/
def SecondProductRuleEqualsCanonicalHessianTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∀ ξ : VertexPotential K,
    reggeActionSecondProductRuleDerivative K hK ξ 0 =
      hessianQuadratic (canonicalReggeHessian K hK) ξ

theorem canonicalHessianSecondVariation_of_nonlinearDirectionalHessian
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h : NonlinearReggeDirectionalHessianTheorem K hK) :
    CanonicalHessianSecondVariationAtZero K hK :=
  h

/-- The full nonlinear Hessian proof is reduced to proving zero second
variation for the canonical remainder line.  The remaining expansion is the
Cayley-Menger/arccos chain-rule calculation. -/
def NonlinearReggeHessianReducedToRemainder
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∀ ξ : VertexPotential K,
    HasSecondDerivAt (canonicalRemainderAlongLine K hK ξ) 0 0

theorem localConformalSchlaefliAngleSqEdgeChainRuleNearZero_of_flatConfiguration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFlat : FlatConfiguration K hK) :
    LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget K := by
  intro ξ
  rw [Filter.eventually_all]
  intro τ
  rw [Filter.eventually_all]
  intro f
  filter_upwards
    [cm3_conformalTetSqEdges_line_pos_eventually K ξ τ,
      dihedralCos3Sq_conformalTetSqEdges_line_endpoint_free_eventually K hK hFlat ξ τ f]
    with t hcm hEndpoint
  let T : ReggeRigorousFoundation.NonDegenerateTet :=
    { sqEdge := conformalTetSqEdges K (linePotential K ξ t) τ
      sqEdge_pos := by
        intro k
        exact conformalLocalSqEdge_line_pos K ξ t τ k
      cm_pos := hcm }
  let F : CayleyMengerPolynomial.SqEdges → ℝ :=
    fun a => DihedralDerivatives.dihedralAngle3Sq a f
  let v : CayleyMengerPolynomial.SqEdges :=
    fun k : Fin 6 =>
      deriv
        (fun s : ℝ =>
          conformalLocalSqEdge K (linePotential K ξ s) τ k) t
  have hAngle : ContDiffAt ℝ 1 F T.sqEdge := by
    simpa [F, T] using
      ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
        T f 1 hEndpoint
  have hDiff : DifferentiableAt ℝ F T.sqEdge :=
    hAngle.differentiableAt (by simp)
  have hF : HasFDerivAt F (fderiv ℝ F T.sqEdge) T.sqEdge :=
    hDiff.hasFDerivAt
  have hgamma : HasDerivAt
      (fun s : ℝ => conformalTetSqEdges K (linePotential K ξ s) τ) v t := by
    simpa [v] using conformalTetSqEdges_hasDerivAt_line K ξ t τ
  have hcomp := HasFDerivAt.comp_hasDerivAt
    (x := t)
    (f := fun s : ℝ => conformalTetSqEdges K (linePotential K ξ s) τ)
    (l := F)
    hF hgamma
  have hvalue :
      (fderiv ℝ F T.sqEdge) v =
        ∑ k : Fin 6,
          DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
            (conformalTetSqEdges K (linePotential K ξ t) τ) f k *
            deriv
              (fun s : ℝ =>
                conformalLocalSqEdge K (linePotential K ξ s) τ k) t := by
    calc
      (fderiv ℝ F T.sqEdge) v
          = ∑ k : Fin 6,
              v k * (fderiv ℝ F T.sqEdge)
                (Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ)) := by
            exact ReggeActionFirstVariation.continuousLinearMap_apply_eq_sum_single
              (fderiv ℝ F T.sqEdge) v
      _ = ∑ k : Fin 6,
          DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
            (conformalTetSqEdges K (linePotential K ξ t) τ) f k *
            deriv
              (fun s : ℝ =>
                conformalLocalSqEdge K (linePotential K ξ s) τ k) t := by
            refine Finset.sum_congr rfl ?_
            intro k _
            have hcoord :=
              ReggeActionFirstVariation.fderiv_dihedralAngle3Sq_apply_single
                T f k hEndpoint
            simp [F, T, v, hcoord, SchlaefliTetrahedronProof.dihedralClosedDerivSq,
              mul_comm]
  rw [hvalue] at hcomp
  simpa [F, Function.comp_def, tetDihedralAngleUnderConformal] using hcomp.deriv

theorem remainder_reduction_eq_canonicalRemainderSecondVariation
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    NonlinearReggeHessianReducedToRemainder K hK ↔
      CanonicalRemainderSecondVariationZero K hK := by
  rfl