IndisputableMonolith.Gravity.SevenGaps.SourcedMinimizerSupDiameter
Analytic helper module for the seven-gaps gravity program: it introduces the shift residual g(h)=sinh(s+h)-sinh s-h and a companion energy-style map F, then records derivative, sign, and monotonicity facts. These feed diameter and quadratic-well estimates for sourced tick minimizers. Proofs are elementary real-analysis arguments (derivatives via Mathlib, sign via mean-value or convexity).
claimDefine the residual $g(h)=\sinh(s+h)-\sinh s-h$ and a companion map $F$. The module proves $g(0)=0$, $g'(h)=\cosh(s+h)-1$, monotonicity and sign control of $g$, nonnegativity of $F$, and that a sourced tick energy has a quadratic well; it also records an approximate tick-distance comparison used for supremum-diameter bounds on sourced minimizers.
background
In the Recognition Science gravity stack, the seven-gaps program studies sourced stationary ratios on the recognition ledger. The upstream module HingeStationarityCore packages the hinge-stationarity core: theorem-level statements (no sorry) linking ledger energy, quadratic curvature energy, and the sourced stationary ratio, importing only Mathlib, Cost, and the ledger-energy bridge.
This module sits one layer down as pure real analysis. The residual $g(h)=\sinh(s+h)-\sinh s-h$ measures how far a hyperbolic shift departs from the linear term $h$; its derivative $\cosh(s+h)-1$ is nonnegative and vanishes only at the balanced point when $s+h=0$ in the appropriate regime. Companion lemmas track $F$, a nonnegative energy-style functional built from the same hyperbolic data, and an approximate tick-distance comparison that turns local quadratic wells into diameter control.
proof idea
Definition-first module with short calculus lemmas. $g$ and $F$ are introduced as plain functions of a real shift. Derivative claims (hasDerivAt_g, hasDerivAt_F) are Mathlib HasDerivAt calculations. Zero and sign lemmas (g_zero, g_nonneg_of_nonneg, g_nonpos_of_nonpos, F_zero, F_nonneg) follow from the derivative formula and the fact that $\cosh u-1\ge 0$. Monotonicity of $g$ is the integral (or MVT) consequence of a nonnegative derivative. The sourced-tick quadratic-well statement packages the second-order lower bound near the stationary hinge; approx_tick_dist converts that well into a concrete distance comparison for later supremum-diameter arguments.
why it matters in Recognition Science
Supremum-diameter control on sourced minimizers is the geometric payoff of hinge stationarity: once the sourced stationary ratio is fixed, one needs a uniform bound on how far discrete tick configurations can wander. This module supplies the elementary hyperbolic calculus that turns the hinge core into a quadratic well and an approximate tick metric, without reopening ledger or curvature definitions.
No downstream edges are recorded on the page yet, so the module presently acts as a leaf helper under Gravity.SevenGaps. It is the natural place later diameter or uniqueness theorems will cite when they need $g$-sign control or the sourced-tick well. Framework-wise it supports the gravity side of the recognition ledger rather than the T0–T8 forcing chain directly.
scope and limits
- Does not prove existence or uniqueness of sourced minimizers.
- Does not derive the hinge stationarity equation itself (that lives upstream).
- Does not bound physical constants (G, alpha, masses) or invoke the phi-ladder.
- Does not claim global diameter bounds without the approximate tick-distance hypotheses.
- Does not address discrete ledger combinatorics beyond the real residual g.