IndisputableMonolith.Geometry.ReggeRemainderClosureAudit

   1import IndisputableMonolith.Geometry.ReggeActionCubicTaylorBound
   2import IndisputableMonolith.Geometry.ReggeActionNonlinearCorrespondence
   3
   4/-!
   5# Regge Remainder Closure Audit
   6
   7Lane-local audit for Track 1B-REM.  The broad
   8`ReggeClosureProgressAudit` imports the active finite-Freudenthal
   9combinatorics module, so this file gives the analytic-remainder branch its own
  10buildable closure certificate.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Geometry
  15namespace ReggeRemainderClosureAudit
  16
  17open Triangulation3DConsistency
  18open ReggeHessian3D
  19open ReggeActionConcrete
  20open ReggeActionSmoothness
  21open ReggeActionSecondVariation
  22open ReggeActionNonlinearHessianProof
  23open ReggeActionNonlinearCorrespondence
  24
  25/-- The 1B-REM proof surface needed downstream: every local analytic remainder
  26target is closed from `FlatConfiguration` plus the standard first- and
  27second-variation remainder jet inputs. -/
  28structure RemainderAnalyticClosed where
  29  closure :
  30    ∀ (K : ReggeTriangulation3D.Triangulation3D) (hK : IncidenceConsistent K),
  31      ReggeActionCubicTaylorBound.CanonicalRemainderAnalyticClosureCert K hK
  32
  33/-- Lane-local theorem-valued certificate for Track 1B-REM. -/
  34def remainderAnalyticClosed : RemainderAnalyticClosed where
  35  closure := ReggeActionCubicTaylorBound.canonicalRemainderAnalyticClosureCert
  36
  37/-- Explicit theorem form for agents that only need the third-derivative bound
  38and should not import the broad progress audit. -/
  39theorem canonicalRemainderLineThirdDerivBound_closed
  40    (K : ReggeTriangulation3D.Triangulation3D) (hK : IncidenceConsistent K)
  41    (hFlat : FlatConfiguration K hK) :
  42    ReggeActionCubicTaylorBound.CanonicalRemainderLineThirdDerivBoundTarget K hK :=
  43  (remainderAnalyticClosed.closure K hK).line_third_deriv_bound_from_flat hFlat
  44
  45/-- Explicit theorem form for the full cubic Taylor theorem endpoint. -/
  46theorem nonlinearReggeCubicTaylorTheorem_closed
  47    (K : ReggeTriangulation3D.Triangulation3D) (hK : IncidenceConsistent K)
  48    (hFlat : FlatConfiguration K hK)
  49    (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
  50      (canonicalReggeHessian K hK))
  51    (hSecond : ReggeActionRemainderSecondVariationInput K hK) :
  52    ReggeActionCubicTaylorBound.NonlinearReggeCubicTaylorTheorem K hK :=
  53  (remainderAnalyticClosed.closure K hK).cubic_taylor_from_flat_and_jets
  54    hFlat hFirst hSecond
  55
  56/-- Direct handoff theorem from the closed analytic-remainder certificate to the
  57local Hessian/Taylor input package used by the nonlinear correspondence layer.
  58The only inputs left are the non-remainder data: flatness, the nonlinear
  59Hessian theorem, and first-variation vanishing for the canonical remainder. -/
  60theorem nonlinearReggeLocalHessianTaylorInputs_closed
  61    (K : ReggeTriangulation3D.Triangulation3D) (hK : IncidenceConsistent K)
  62    (hFlat : FlatConfiguration K hK)
  63    (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
  64    (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
  65      (canonicalReggeHessian K hK)) :
  66    ReggeActionCubicTaylorBound.NonlinearReggeLocalHessianTaylorInputs K hK hFlat := by
  67  let hSecond : ReggeActionRemainderSecondVariationInput K hK :=
  68    reggeActionRemainderSecondVariationInput_of_flat_nonlinearHessian K hK hFlat
  69      hHessian
  70  exact ReggeActionCubicTaylorBound.nonlinearReggeLocalHessianTaylorInputs_of_hessian_and_taylor
  71    K hK hFlat hHessian
  72    (nonlinearReggeCubicTaylorTheorem_closed K hK hFlat hFirst hSecond)
  73
  74/-- Direct local-correspondence endpoint from the closed 1B-REM certificate.
  75This keeps downstream users out of the line-Taylor split; they supply only the
  76non-remainder Hessian theorem and canonical remainder first-variation input. -/
  77theorem nonlinearReggeJCostLocalCorrespondence_closed
  78    (K : ReggeTriangulation3D.Triangulation3D) (hK : IncidenceConsistent K)
  79    (hFlat : FlatConfiguration K hK)
  80    (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
  81    (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
  82      (canonicalReggeHessian K hK)) :
  83    NonlinearReggeJCostLocalCorrespondence K hK :=
  84  nonlinearRegge_localCorrespondence_of_localHessianTaylorInputs K hK hFlat
  85    (nonlinearReggeLocalHessianTaylorInputs_closed K hK hFlat hHessian hFirst)
  86
  87/-- Alias at the strongest true replacement surface: local quadratic-core
  88correspondence with a controlled cubic remainder. -/
  89theorem strongestTrueReggeJCostReplacement_closed
  90    (K : ReggeTriangulation3D.Triangulation3D) (hK : IncidenceConsistent K)
  91    (hFlat : FlatConfiguration K hK)
  92    (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
  93    (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
  94      (canonicalReggeHessian K hK)) :
  95    StrongestTrueReggeJCostReplacement K hK :=
  96  nonlinearReggeJCostLocalCorrespondence_closed K hK hFlat hHessian hFirst
  97
  98end ReggeRemainderClosureAudit
  99end Geometry
 100end IndisputableMonolith
 101