kappaGen
plain-language theorem explainer
Defines the shared positive denominator base κ(a,b,λ,t) = a²λ cosh(at) + b²λ cosh t · cosh(at) + cosh t for the general-α closed forms of (∇^λ)_0 P^0_0 and R^0_{1,0,1} on the 2-slice. Anyone citing the general-α non-parallelism or non-flatness certificates (or the Stage B curvature reduction) needs this scalar. Pure definition: three hyperbolic summands, no proof obligations.
Claim. For real parameters $a,b,\lambda,t$, set $$\kappa(a,b,\lambda,t) := a^{2}\lambda\cosh(at) + b^{2}\lambda\cosh t\cdot\cosh(at) + \cosh t.$$ This is the common denominator factor appearing in the general-$\alpha=(a,b)$ formulas for $(\nabla^{\lambda})_{0}P^{0}_{0}$ and $R^{0}_{1,0,1}$ at the slice point $(t,0)$.
background
The module supplies scalar certificates for the Golden/Metallic note: on the 2-slice with potential $\Phi_\lambda(t_0,t_1)=\cosh t_0+\cosh t_1+\lambda(\cosh(t_0+t_1)-1)$, metric $h_\lambda=D+\lambda\tilde g$, and projector $P_\lambda$ onto $\mathrm{span}(1,1)$, one evaluates at $(t_0,t_1)=(t,0)$.
For the special case $\alpha=(1,1)$, $\lambda=1$ the closed forms $P^{0}{0}$, $\partial_0 P^{0}{0}$, $(\nabla^\lambda)0 P^{0}{0}$, and $R^{0}_{1,0,1}$ are already written. The general-$\alpha=(a,b)$ family needs a common positive denominator so that the covariant-derivative and Riemann expressions stay well-defined and sign-controllable.
That denominator is $\kappa$: three nonnegative hyperbolic terms, the last strictly positive. Downstream positivity (kappaGen_pos) and the general closed forms for $\nabla P$ and $R$ are built directly on it.
proof idea
Definition only: expand the three-term formula
$a^{2}\lambda\cosh(at)+b^{2}\lambda\cosh t\cdot\cosh(at)+\cosh t$
and stop. No tactics, no lemmas. Positivity and nonvanishing are proved later by unfolding this def and applying positivity / cosh_pos.
why it matters
κ is the algebraic glue for the general-α certificates. It appears in the numerator/denominator of nablaP000Gen and R0101Gen, so the nonvanishing theorem (Theorem 1b general α) and the strict negativity of $R^{0}_{1,0,1}$ (Theorem 2 general α) both route through kappaGen_pos.
Downstream, the Stage B capstone RiemannMixedApply_reduce collapses the abstract $n$-dimensional mixed Riemann component on any 2-sparse slice to R0101Gen a b lam (t i0), which is written in terms of κ. Thus non-flatness of $h_\lambda$ for the whole $(a,b)$ family, not just $(1,1)$, rests on this scalar.
Within Recognition cost geometry this is the denominator that lets the λ-deformed metric stay non-flat and the projector stay non-parallel without constructing special numerical points inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.