NonlinearJCostReggeCert
plain-language theorem explainer
NonlinearJCostReggeCert bundles five properties of the exact J-cost action on weighted ledger graphs: nonnegativity for arbitrary log-potentials, vanishing on the flat vacuum, exact decomposition into Laplacian action plus quartic remainder, nonnegativity of that remainder, and equality to the scaled Regge sum under the nonlinear matching hypothesis. Researchers working on strong-field Regge calculus or addressing Beltracchi §6 would cite it to separate unconditional J-cost facts from the remaining hypothesis. The structure is assembled by one-
Claim. A certificate structure asserting that the exact J-cost action $S_J(G,ε)=∑_{ij}w_{ij}(cosh(ε_i−ε_j)−1)$ satisfies $0≤S_J(G,ε)$ for every weighted ledger graph $G$ and log-potential $ε$, that $S_J(G,0)=0$, that $S_J(G,ε)=Δ(G,ε)+Q(G,ε)$ with $0≤Q(G,ε)$, and that under the hypothesis NonlinearReggeJCostIdentity$(D,a,ha,hinges,G)$ one has $S_J(G,ε)=(1/jcost_to_regge_factor)⋅regge_sum(D.functional,conformal_edge_length_field(a,ha,ε),hinges)$.
background
The module establishes the nonlinear J-cost/Regge bridge to answer Beltracchi §6: prior identifications were limited to quadratic order and therefore could not authorize black-hole physics. The exact J-cost action is defined as the sum over edges of $w_{ij}(cosh(ε_i−ε_j)−1)$, which equals the Laplacian action plus a quartic remainder whose sign follows from the Taylor series of cosh. NonlinearDeficitFunctional extends the linear deficit-angle functional to strong-field configurations; NonlinearReggeJCostIdentity is the hypothesis that the Regge sum on this functional equals jcost_to_regge_factor times the exact J-cost action. Upstream results supply the constants G and the reparametrization G_F(t)=F(exp t) used in the conformal edge-length map.
proof idea
The declaration is a structure definition. Its five fields are witnessed directly by sibling lemmas: exactJCostAction_nonneg supplies exact_well_defined, exactJCostAction_flat supplies exact_flat_zero, exact_decomposition supplies the split, quarticRemainder_nonneg supplies remainder_nonneg, and the final identity field follows from the definition of NonlinearReggeJCostIdentity. No tactics or reductions occur inside the structure.
why it matters
The certificate separates the unconditionally established properties of the exact J-cost action from the nonlinear Regge matching hypothesis, thereby supplying the Lean-level resolution of the strong-field validity question stated in the module documentation. It is instantiated by the downstream theorem nonlinearJCostReggeCert. In the Recognition framework it extends J-uniqueness (T5) and the composition law (RCL) to the full nonlinear regime while leaving the Regge side as an explicit hypothesis; it touches the open question of whether the nonlinear identity holds for generic simplicial complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.