Pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.BlockReduction

show as:
view Lean formalization →

Finite-n block reduction for the cost-induced projector: the undeformed diagonal inverse Dinv, two-sparse test vectors, and the mixed-tensor action of P. Generalizes the 2D non-parallelism certificate (Theorem 1a) to arbitrary ambient dimension. Downstream curvature work imports it to drop the 2-sparsity restriction. Argument is direct array algebra plus the projector quadratic law from the Projector module.

claimOn $\mathbb{R}^n$, let $D=\mathrm{diag}(\cosh t_0,\ldots,\cosh t_{n-1})$ be the undeformed Hessian metric and $D^{-1}$ its diagonal inverse. For the cost-induced mixed projector $P_\lambda$ built from a covector and $D^{-1}$, the module supplies two-sparse test data and proves $P_\lambda$ is not parallel to the flat connection in every dimension $n\ge 2$.

background

Recognition cost geometry works with a one-parameter family of metrics $h_\lambda=D+\lambda\tilde g$ on $\mathbb{R}^n$. Here $D$ is the diagonal Hessian of $\sum_i\cosh(t_i)$ (the uncoupled $\lambda=0$ piece of the potential $\Phi_\lambda$), so $D^{-1}$ is elementary and diagonal. The Projector module packages the rank-one picture: a covector $\beta$ and inverse kernel determine the sharp vector, the operator $A=h^{-1}\tilde g$ with $A^2=\mu A$, and the normalized projector $P$.

ScalarCertificates already proved, by direct scalar computation on the 2D slice $\alpha=(1,1)$, that $P_\lambda$ is not parallel w.r.t. the flat connection $D$ (Theorem 1a) nor the Levi-Civita connection of $h_\lambda$ (Theorem 1b). BlockReduction lifts the ambient space from that slice to general $n$, keeping the undeformed inverse $D^{-1}$ and the mixed-tensor applicator $P\mathrm{Apply}$ as the working objects.

Sibling definitions introduce $D^{-1}$, the two-sparse support pattern, the standard basis vectors $e$, the pairing $\mathrm{dot}_e$, and the scalar $\mu$ of the $D^{-1}$-sharpened two-sparse data.

proof idea

Definition layer first: $D^{-1}$ as the reciprocal diagonal, TwoSparse as the support mask, and the elementary identities sharp_Dinv_apply, sum_twoSparse, mu_Dinv_twoSparse. The bridge identities PApply_e_eq_P00Gen and PApply_not_parallel_gen then compare the mixed-tensor action of $P$ on the two-sparse test vector against the 2D scalar certificate. Non-parallelism in dimension $n$ reduces to the already-proved 2-slice non-vanishing of $dP_{00}$, because the extra coordinates sit in the kernel of the two-sparse data. No curvature or full $h_\lambda$ inverse is built here.

why it matters in Recognition Science

CurvatureBridge imports this module and states the role explicitly: BlockReduction generalizes Theorem 1a (non-parallelism of $P_\lambda$) to arbitrary ambient dimension $n$ via PApply and the undeformed inverse Dinv. That frees the subsequent non-flatness argument (Theorem 2) to work with the genuine deformed metric $h_\lambda=D+\lambda\tilde g$ as a full $n\times n$ array, its Sherman-Morrison inverse, and the Riemann tensor, without retaining a 2-sparsity hypothesis. In the cost domain this is the dimensional bridge between the golden/metallic $\lambda$-family certificates and the general-$n$ curvature package.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)