pith. machine review for the scientific record. sign in
def definition def or abbrev high

exactJCostAction

show as:
view Lean formalization →

The exact J-cost action on a weighted ledger graph is the double sum over vertex pairs of edge weight times (cosh of log-potential difference minus one). Researchers extending J-cost gravity into strong-field or black-hole regimes would cite this definition to remove the weak-field restriction. It is introduced as a direct definition matching the Recognition Composition Law, with no approximation or additional lemmas required.

claimLet $G$ be a weighted ledger graph on $n$ vertices with non-negative symmetric edge weights $w_{ij}$, and let $ε$ be a log-potential function. The exact J-cost action is defined by $∑_{i,j} w_{ij} (cosh(ε_i - ε_j) - 1)$.

background

This declaration sits in the Nonlinear J-Cost / Regge Bridge module, which directly addresses Beltracchi §6 by supplying a J-cost functional valid at all orders in the potential difference. The module defines the nonlinear coupling via $J(exp(ε_i - ε_j)) = cosh(ε_i - ε_j) - 1$, which follows from the Recognition Composition Law and the J-uniqueness property $J(x) = cosh(log x) - 1$. WeightedLedgerGraph is the structure carrying a non-negative symmetric weight function on Fin n × Fin n; LogPotential is the type of functions Fin n → ℝ that assign log-potentials to vertices. Upstream results supply the constants G and the cost functional from MultiplicativeRecognizerL4 and ObserverForcing, both of which reduce to the same J-cost expression.

proof idea

This is a direct definition that unfolds immediately to the double summation over the graph weights and the cosh expression. No tactics or lemmas are applied inside the body; the definition is the explicit transcription of the Recognition Composition Law into graph language.

why it matters in Recognition Science

This definition supplies the nonlinear extension required by the downstream decomposition theorem exact_decomposition, which writes exactJCostAction = laplacian_action + quarticRemainder with the remainder non-negative. It closes the strong-field gap in the J-cost ↔ Regge identification, allowing the framework to treat black-hole regimes without a weak-field assumption. The construction rests on T5 J-uniqueness and the Recognition Composition Law; it feeds the stationarity corollary jcost_stationarity_to_regge_nonlinear and the flat-vacuum agreement theorems.

scope and limits

formal statement (Lean)

  98def exactJCostAction {n : ℕ} (G : WeightedLedgerGraph n)
  99    (ε : LogPotential n) : ℝ :=

proof body

Definition body.

 100  ∑ i : Fin n, ∑ j : Fin n,
 101    G.weight i j * (Real.cosh (ε i - ε j) - 1)
 102
 103/-- The exact J-cost action vanishes on the flat vacuum `ε ≡ 0`. -/

used by (11)

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

depends on (9)

Lean names referenced from this declaration's body.