Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge

show as:
view Lean formalization →

Bridge between discrete hinge curvature energy and the recognition ledger cost. Defines the Isaacson-type quadratic energy Σ A_h δ_h² on hinge areas and deficit angles, proves nonnegativity and positivity, and supplies hyperbolic comparison lemmas tying J-cost remainders to half-square curvature. Cited by hinge-stationarity and recognition-ratio work in the seven-gaps campaign. Argument is definitional plus elementary real-analytic bounds on sinh/cosh and J.

claimOn hinge data $(A_h, \delta_h)$, the discrete quadratic curvature energy is $E = \sum_h A_h \delta_h^2$. It is nonnegative, even in $\delta$, and (when $A>0$ and $\delta\neq 0$) strictly positive. Comparison lemmas bound $J(e^t)-t^2/2$ and related $\cosh/\sinh$ remainders so the geometric energy matches the parity and sign of the ledger cost side.

background

Recognition gravity books curvature against a recognition ledger whose continuum limit is a gravitational action (see RecognitionLedger). On the discrete side one works with hinge data: areas $A:H\to\mathbb{R}$ and deficit angles $\delta:H\to\mathbb{R}$. The module isolates the purely geometric quadratic form $\sum_h A_h\delta_h^2$, the discrete Isaacson-type curvature energy density, with no ledger objects in its definition.

The cost side uses the RS $J$-cost from Cost, classically $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Matching ledger parity requires the geometric energy to be even in $\delta$ and nonnegative. Hyperbolic identities (bounds of $\sinh$ by $|\cdot|\cosh$, of $\cosh-1$ by half-square times $\cosh$, and remainder controls on $J(e^t)-t^2/2$) make that match quantitative.

A coboundary predicate and an RCL-gate identity for $J$ appear as interface lemmas so later modules can treat ledger increments as exact differences rather than free sources.

proof idea

Definition module with supporting real-analysis lemmas, not a single deep theorem. quadraticCurvatureEnergy is the sum $\sum A_h\delta_h^2$; nonnegativity is termwise from squares, positivity when some $A_h>0$ and $\delta_h\neq 0$.

The bulk of the file is elementary inequalities: $\sinh$ controlled by absolute value times $\cosh$; $\cosh u-1\le (u^2/2)\cosh u$; nonnegativity and upper bounds on the cosh remainder; $\cosh 1<2$; and the key comparison $|J(e^t)-t^2/2|$ bounded via those remainders. IsCoboundary and rclGate_Jcost_eq are structural interfaces tying cost increments to the Recognition Composition Law gate, proved by direct unfolding of $J$.

why it matters in Recognition Science

Feeds the seven-gaps campaign at the energy-ledger interface. HingeStationarityCore imports only Cost and this bridge (plus Mathlib) to obtain the sourced stationary ratio on hinges; its doc states the import set is exactly those three, so stationarity proofs sit on this energy definition and the $J$-remainder bounds.

RecognitionRatioBridge (Phase 0a, paper odd form / Def 6.2 clause) uses the bridge to align geometric curvature energy with the recognition-ratio side. CampaignLedger records scoped increments against these modules without flipping full QGScopeAudit flags. RecognitionDualEntryEnrichment4D pulls the same energy/ledger match into Wave B residual work on signed-source enrichment.

In framework terms this is the discrete nonnegative curvature quadratic that must match ledger parity before continuum recognition gravity (ledger total cost as action) can be compared to Einstein-Hilbert-type curvature squares.

scope and limits

used by (4)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (31)