Minimal Positive Repair

Abstract

The sharp positive repair of the Fibonacci eigenform, with the corrected uniqueness scope.

Theorem 1.1 (Sharp norm bound, attainment, and spectral minimality).

$$\begin{array}{r}\mathrm{PosSemidef}\left(R\right)\wedge \mathrm{PosSemidef}\left(F+R\right)\Rightarrow |R{|}_{op}\ge {\phi }^{-1},\\ Rmin={\phi }^{-1}\cdot P_{-},\\ F+Rmin=\phi \cdot P_{+},\\ \exists Ralt,Ralt\ne Rmin\wedge |Ralt{|}_{op}={\phi }^{-1}.\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Eigenstructure/MinimalPositiveRepair.minimal_positive_repair (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Fibonacci form is represented in its expanding and contracting eigenbasis. Positivity on the contracting coordinate forces every feasible repair to have operator norm at least phi inverse.

The negative-part repair attains the bound, leaves phi times the expanding projection, is positive semidefinite, and has rank one. The proof uses Mathlib’s L2 matrix operator norm rather than an entrywise norm.

The source’s unrestricted uniqueness assertion is false: phi inverse times the identity is a distinct feasible repair with the same norm. The Lean theorem records this counterexample and proves uniqueness only for the coefficientwise least repair diagonal in the Fibonacci eigenbasis.

References

• Truth anchor: D5/S1/Eigenstructure/MinimalPositiveRepair.minimal_positive_repair
• Dependency: D5/S1/Scale/FibonacciEigen