Cost Ndim Projector Papply Idempotent

The idempotent projector

In linear algebra, a projector is a linear map that is its own square: applying it twice has the same effect as applying it once. The declaration PApply_idempotent proves that the operator P, built from a covector β and an inverse metric kernel hInv, has exactly this property. Concretely, for any vector v, P(P(v)) = P(v). This is the defining property of a projection onto a subspace: the first application drops the vector onto the subspace, and the second application leaves it there.

The construction starts with a rank-one operator A = λ h⁻¹ (β ⊗ β), where λ is a scalar and β ⊗ β is the outer product of β with itself. The scalar μ = λ β·(h⁻¹β) is the coefficient in the quadratic relation A² = μA. The projector P is the normalized version, P = μ⁻¹ A, which exists only when μ ≠ 0. The theorem PApply_idempotent states this normalization works: under the condition μ ≠ 0, the operator P satisfies P² = P.

This idempotence is what makes P a genuine projection onto the one-dimensional subspace spanned by the sharp vector β♯ = h⁻¹β. The operator A sends any vector to a multiple of β♯, and P scales that multiple to be exactly the component along β♯. The theorem also supports the derived operators: the almost-product F = 2P − I satisfies F² = I, and the golden operator G = (1/2)I + (√5/2)F satisfies G² = G + I. These identities are proved in the same module, building the operator algebra that underlies the rank-one tensor picture.

What the declaration does not claim is just as important. It does not assert that P is a projector for all choices of the inputs: the condition μ ≠ 0 is essential, and when μ = 0 the normalization fails. It does not claim that P is orthogonal with respect to any particular inner product, nor that the subspace it projects onto is unique. The theorem is purely algebraic, holding for any real vector space of finite dimension n, with no metric or geometric structure assumed beyond the given kernel hInv.

theorem PApply_idempotent {n : ℕ}
    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
    PApply lam hInv β (PApply lam hInv β v) = PApply lam hInv β v := by
  ext i
  simp [PApply, AApply_smul, AApply_sq, hμ, mul_comm]

theorem AApply_sq {n : ℕ}
    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v : Vec n) :
    AApply lam hInv β (AApply lam hInv β v) = mu lam hInv β • AApply lam hInv β v := by
  funext i
  have hdot :
      dot β (fun k => lam * sharp hInv β k * dot β v) = mu lam hInv β * dot β v := by
    simpa [AApply] using dot_AApply lam hInv β v
  unfold AApply
  rw [hdot]
  simp [mu]
  ring

theorem FApply_square {n : ℕ}
    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
    FApply lam hInv β (FApply lam hInv β v) = v := by
  ext i
  have hPFi : PApply lam hInv β (FApply lam hInv β v) i = PApply lam hInv β v i := by
    simpa using congrFun (PApply_FApply lam hInv β hμ v) i
  calc
    FApply lam hInv β (FApply lam hInv β v) i
        = (2 • PApply lam hInv β (FApply lam hInv β v) - FApply lam hInv β v) i := by
            simp [FApply]
    _ = (2 • PApply lam hInv β v - FApply lam hInv β v) i := by
          simp [hPFi]
    _ = v i := by
          simp [FApply]

What this page does not claim

P is not claimed to be an orthogonal projection for any particular inner product. The theorem does not assert existence of the projector for all parameter choices, only under μ ≠ 0. No claim is made about the physical significance of the subspace onto which P projects.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/Projector.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: