Geometry Regge Action Second Variation Regge Action Remainder Second Variation I

The remainder's second variation

In the Recognition Science framework, the Regge action is a way to write down the total curvature of a triangulated space by summing contributions from its edges. The declaration ReggeActionRemainderSecondVariationInput names a precise analytic condition: when the action is expanded around a flat configuration, the part left over after removing the quadratic (Hessian) term has zero second variation along any line through the flat point. In plain terms, the remainder is flatter than quadratic at the flat configuration; it does not contribute to the second derivative that defines stability.

The declaration is a structure, not a theorem. It packages the condition as an input for later results, and the accompanying theorem reggeActionRemainder_secondVariation_zero merely unpacks it: given the input, the condition holds. The library's docstring is explicit that the lower-level calculation, a large Cayley-Menger and arccos chain-rule expansion, is not yet materialized. The declaration therefore establishes a target property, not a proof that the property holds for the actual Regge action.

This matters for what the framework can currently claim. The second-variation input is a named assumption, and the cubic remainder input is a separate structure that states a local bound of order three. A sanity constructor shows that if the remainder were identically zero, the cubic bound would follow with constant zero. But the general proof that the Regge action's remainder satisfies either condition remains open, and the declaration does not assert it.

What the declaration does establish is a clean interface: it lets later theorems be stated and checked against a well-defined hypothesis, so that the framework can build the structure of a second-order analysis before the heavy analytic work is complete. It is a scaffold, not a finished wall.

structure ReggeActionRemainderSecondVariationInput
    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  remainder_secondVariation_zero :
    CanonicalRemainderSecondVariationZero K hK

theorem reggeActionRemainder_secondVariation_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_rem : ReggeActionRemainderSecondVariationInput K hK) :
    CanonicalRemainderSecondVariationZero K hK :=
  h_rem.remainder_secondVariation_zero

What this page does not claim

The declaration does not prove that the Regge action's remainder actually has zero second variation. It does not establish the cubic remainder bound as a theorem. It does not claim the Regge action's second variation equals the canonical Hessian without further input.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/ReggeActionSecondVariation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: