Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.StationarityBridgeClosure

show as:
view Lean formalization →

Closes the bridge from sourced hinge stationarity to the recognition-ratio package: total strain of the unique sourced minimizer equals n arsinh(c/n), the log of the constructor's xRatio. Gravity workers cite it when wiring the cubic bound to the stationary ratio. The argument identifies the minimizer strain with the bridge log-ratio and packages the resulting RecognitionRatioBridge instance.

claimFor the unique sourced minimizer with coordinates $t_i=\mathrm{arsinh}(c/n)$, the total strain equals $n\,\mathrm{arsinh}(c/n)$. That quantity is exactly $\log x_{\mathrm{ratio}}$ used by the recognition-ratio constructor, so stationarity supplies a closed-form $x_{\mathrm{ratio}}$ and a $RecognitionRatioBridge$ instance to which the cubic bound applies.

background

Seven Gaps Phase 0a isolates the recognition-ratio bridge (paper Def 6.2 / odd form): an admissibility package whose model tier still carries an explicit hypothesis, while named theorems under it are fully proved. Upstream, HingeStationarityCore supplies the sourced stationary ratio and the unique sourced minimizer $t_i=\mathrm{arsinh}(c/n)$ in the J-cost / ledger-energy setting (imports Cost and LedgerEnergyBridge, including quadratic curvature energy).

The present module is the kernel link between those two layers. It treats total strain of the sourced minimizer as the quantity whose exponential is the bridge constructor's $x_{\mathrm{ratio}}$, so "defined from the minimizer" and "closed form the cubic bound talks about" become the same object. Sibling material also records sign properties of the log-ratio, a non-admissible linear deficit family, and a quadratic source family used for contrast.

proof idea

Not a single theorem file: a short closure layer. Core identity equates total strain of the sourced minimizer to $n,\mathrm{arsinh}(c/n)$ and to $\log x_{\mathrm{ratio}}$. From that, definitions and lemmas ground the of-stationarity constructor (xRatio definition, log-xRatio, equality to minimizer strain, positivity/negativity cases) and assemble recognitionRatioBridge_ofStationarity. Side results mark a linear deficit family as non-admissible and introduce a quadratic source family. No new analytic heavy lifting beyond the hinge core and bridge API.

why it matters in Recognition Science

Without this identification, the cubic bound on the stationary ratio and the recognition-ratio bridge float apart: one side knows the minimizer, the other states inequalities about a formal $x_{\mathrm{ratio}}$. Downstream, RecognitionRatioSubstrateBlocker imports the closure as part of the P2.1 terminal argument that recognition_ratio_derived does not follow from a bare RecognitionLedger; the missing premise is a signed deficit-source constitutive coupling $c_\sigma=\kappa_\sigma\delta_\sigma$ linear in total strain in the J-cost action. The module therefore pins the stationarity-to-bridge wire that later substrate-blocker and gravity-gap arguments rely on when separating proved bridge theorems from still-open constitutive hypotheses.

scope and limits

used by (1)

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 (23)