PApply_not_parallel_gen
plain-language theorem explainer
For any ambient dimension n at least 2, a 2-sparse covector alpha on distinct indices i0, i1, and a slice with t at i1 equal to 0, the (i0,i0) entry of the n-dimensional projector P_lambda, as a function of the free coordinate at i0, has derivative equal to the 2D form dP00Gen, and that derivative is nonzero when both alpha components and the free coordinate are nonzero. Cited for general-n non-parallelism of P_lambda versus the flat connection D. Proof: reduce to P00Gen, then transport the 2D derivative certificate.
Claim. Fix $n \in \mathbb{N}$, background $t \in \mathbb{R}^n$, covector $\alpha \in \mathbb{R}^n$, $\lambda \neq 0$, and distinct indices $i_0 \neq i_1$. Assume $\alpha$ vanishes off $\{i_0,i_1\}$, $\alpha_{i_0} \neq 0$, $\alpha_{i_1} \neq 0$, and $t_{i_1} = 0$. Then $s \mapsto (P_\lambda(D^{-1}(t[i_0 \mapsto s]), \alpha)\, e_{i_0})_{i_0}$ is differentiable at every $s$ with derivative $dP_{00}^{\mathrm{gen}}(\alpha_{i_0}, \alpha_{i_1}, s)$, and that derivative is nonzero whenever $s \neq 0$.
background
The module lifts non-parallelism of the recognition projector $P_\lambda$ from the pure 2D slice of ScalarCertificates to arbitrary ambient dimension. The undeformed metric is the diagonal $D = \mathrm{diag}(\cosh t_0, \ldots, \cosh t_{n-1})$, with inverse kernel $D^{-1}$. The abstract projector builds $P_\lambda$ from any inverse-metric kernel and covector in any dimension $n$.
A vector $\alpha$ is two-sparse on $(i_0, i_1)$ when it vanishes off those two coordinates: the general-$n$ stand-in for the 2D pair $(a,b)$. The indicator $e_{i_0}$ extracts the $(i_0,i_0)$ matrix entry. Upstream, the block-reduction identity states that on the slice $t_{i_1}=0$, the $(i_0,i_0)$ entry of $P_\lambda(D^{-1}t, \alpha)$ applied to $e_{i_0}$ equals exactly the 2D closed form $P00Gen(\alpha_{i_0}, \alpha_{i_1}, t_{i_0})$. The 2D scalar derivative $dP00Gen(a,b,s) = -(a^2 b^2 \sinh s)/(a^2 + b^2 \cosh s)^2$ and its nonvanishing certificate are already proved in ScalarCertificates.
proof idea
First establish pointwise functional equality: for every free value $s'$, the $n$-dimensional evaluation at the updated background equals the closed form $P00Gen(\alpha_{i_0}, \alpha_{i_1})$. This uses that updating the $i_0$ slot preserves $t_{i_1}=0$ (via $i_0 \neq i_1$), then applies the block-reduction theorem, and rewrites the free slot by the update-at-self identity.
With both sides identical as functions of $s$, rewrite the derivative goal along that equality and invoke the 2D certificate that $P00Gen$ has derivative $dP00Gen$. The nonvanishing conjunct is a direct application of the 2D nonvanishing lemma under $\alpha_{i_0} \neq 0$, $\alpha_{i_1} \neq 0$, and $s \neq 0$. No new differentiation is performed in ambient dimension $n$.
why it matters
This is the panel-greenlit general-$n$ form of Theorem 1a: non-parallelism of $P_\lambda$ with respect to the flat connection $D$. The module frames it as the correct architecture for the lift: the $n$-dimensional projector is the 2D closed form on the two-sparse slice, so the already-proved 2D nonvanishing of the $(0,0)$ derivative transports verbatim for every $n \geq 2$.
In the Recognition cost calculus, failure of $D$-parallelism along the free coordinate means the projector (and the induced almost-product structure) cannot be absorbed into the undeformed diagonal Hessian of $\sum_i \cosh t_i$. That geometric content is needed before higher-curvature certificates can be stated in ambient dimension $n$ rather than only on a hard-coded 2-plane. No downstream consumers are wired yet; the declaration closes the reduction path announced by the block-reduction identity and stands as the general-$n$ endpoint of the Theorem 1a chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.