Pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.ScalarCertificates

show as:
view Lean formalization →

Certificate lemmas for the reciprocal cost projector on a fixed 2D slice: values, first derivatives, and curvature of P at the background point (t,0) with equal weights and unit scale. Supplies the non-vanishing and non-parallelism facts that BlockReduction lifts from n=2 to arbitrary ambient dimension for 2-sparse weight vectors. Proofs are direct calculus on the closed-form scalar kernel plus elementary algebraic identities.

claimOn the two-dimensional slice with background $(t,0)$, weights $\alpha=(1,1)$ and scale $\lambda=1$, the module records the scalar projector value $P^0_0$, its first derivatives, the mixed second derivative (curvature) $R_{0101}$, and the corresponding non-vanishing statements; parallel certificates are given for a general two-weight pair $\alpha=(a,b)$.

background

Recognition Science builds multi-component cost from a scalar reciprocal kernel $J$ by a weighted log aggregate (the N-dimensional reciprocal cost of Cost.Ndim.Core). The projector $P_\lambda$ and the associated connection data $h_\lambda$ are the geometric objects that encode how that cost sits relative to the flat connection $D$.

This module specializes to ambient dimension $n=2$ and evaluates everything at the slice point where the second coordinate vanishes. The equal-weight unit-scale case $\alpha=(1,1)$, $\lambda=1$ is written out first; a parallel family of definitions covers a general pair of positive weights. Trigonometric derivative lemmas from Mathlib supply the calculus infrastructure for the closed forms.

proof idea

The module is a certificate pack, not a single theorem. Closed-form expressions for $P^0_0$, its first derivatives, and the mixed curvature $R_{0101}$ are obtained by specializing the scalar kernel on the slice $(t,0)$. Differentiability is recorded via HasDerivAt facts; non-vanishing of the first derivative and of the curvature follow by direct algebraic inspection of those closed forms (and a sign-flip identity for the curvature). The general-weight variants repeat the same pattern with parameters $(a,b)$ in place of $(1,1)$.

why it matters in Recognition Science

BlockReduction imports this module as the $n=2$ base case. Its doc-comment states that ScalarCertificates proves non-parallelism and non-flatness of $P_\lambda/h_\lambda$ on a 2-dimensional slice, and that BlockReduction lifts Theorem 1a (non-parallelism of $P_\lambda$ w.r.t. the flat connection $D$) to arbitrary ambient dimension for any 2-sparse weight vector by reducing the abstract projector PApply at a background with one coordinate zero back to these certificates. Without the non-vanishing curvature and derivative facts here, the higher-dimensional reduction has nothing to specialize to. In the broader cost geometry this is the concrete calculus step that keeps the multi-component reciprocal cost from collapsing to a flat or parallel projector on sparse supports.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (19)