g_zero
plain-language theorem explainer
For any real source parameter s, the local response kernel g(s,·) vanishes at zero load: g(s,0)=0. Sign and monotonicity lemmas in the sourced-minimizer diameter module cite this as the basepoint; the J-cost log-space certificate structure also requires a zero-at-origin clause of this shape. The proof is a one-line simp that unfolds the definition of g.
Claim. For every real number $s$, the kernel satisfies $g(s,0)=0$.
background
The module develops diameter and stationarity controls for sourced tick minimizers in the Seven Gaps gravity layer. A two-argument kernel $g(s,h)$ appears as the elementary building block: $s$ is a fixed source (or scale) parameter and $h$ is the load or height variable. Sibling facts record that $g(s,\cdot)$ is monotone and differentiable, and that a companion potential $F$ inherits nonnegativity from $g$.
Zero load is the natural basepoint. Once $g(s,0)=0$ is known, monotonicity immediately yields the sign rules $h\ge 0\Rightarrow g(s,h)\ge 0$ and $h\le 0\Rightarrow g(s,h)\le 0$. The same zero-at-origin pattern is required by the abstract certificate structure for J-cost convexity in log space (the field demanding $g(0)=0$), which packages evenness and strict positivity off zero for the Recognition cost $J$.
Note the name collision with the AlphaGenesis dressing response, where a different $g$ satisfies $g(0)=1$ (unit response, no dressing at zero load). That identity lives in a separate module and is not used here; the present $g$ is the local Seven Gaps kernel with value $0$ at the origin.
proof idea
One-line wrapper: simp [g] unfolds the definition of the local kernel and reduces the goal to a trivial arithmetic identity. No external lemmas are applied.
why it matters
This is the basepoint identity that turns monotonicity of $g(s,\cdot)$ into the sign lemmas g_nonneg_of_nonneg and g_nonpos_of_nonpos in the same module. Those sign facts feed the sourced-tick quadratic-well and approximate tick-distance arguments that bound the diameter of sourced minimizers.
Downstream, the same zero-at-origin shape is recorded in the JCostLogSpaceCert structure (field $g,0=0$), which certifies convexity of the Recognition J-cost in logarithmic coordinates. That certificate sits on the path from the T5 J-uniqueness landmark ($J(x)=(x+x^{-1})/2-1$) toward quantitative control of defects in log space. The declaration itself is purely local bookkeeping; it does not force the exponential dressing response of AlphaGenesis (where a different $g$ has $g(0)=1$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.