det_sub_smul_one
plain-language theorem explainer
For any real 2×2 matrix W and scalar y, the characteristic determinant expands as det(W − y I) = y² − (tr W) y + det W. Seam-transfer holography cites this to turn a real eigenvalue into a root of the monic quadratic λ² − Tr λ + det. The proof is a direct Fin-2 expansion: rewrite det and trace by components, simplify entries, then ring.
Claim. For every real $2\times 2$ matrix $W$ and every real scalar $y$, $\det(W - y I) = y^{2} - (\operatorname{tr} W)\, y + \det W$, where $I$ is the $2\times 2$ identity.
background
SeamTransferCore develops the panel's Phase-B claim that the per-closure recognition cost of a seam crossing is the character anomaly $C = \operatorname{Tr}(W)/2 - 1$ of a transfer $W$ acting on the seam's double-entry pair fiber. The program refuses to posit $W = \operatorname{diag}(x,x^{-1})$; balance ($\det W = 1$) plus one real eigenvalue must force the reciprocal leg and then the trace identity that recovers the T5 cost $J$.
The characteristic polynomial of a $2\times 2$ matrix is the monic quadratic $\lambda^{2} - (\operatorname{tr} W)\lambda + \det W$. This lemma is the evaluated form of that polynomial: it identifies $\det(W - y I)$ with that quadratic at $y$. Downstream, a real eigenvalue $x$ means $W - x I$ kills a nonzero vector, hence has determinant zero, so $x$ is a root.
The module sits in the holography layer that reduces CensusPricing to structural facts about a balanced 2d transfer (unit determinant, delivered-leg eigenvalue, trace reading) without naming $J$ in the inputs.
proof idea
Tactic proof by component expansion on Fin 2. Rewrite the left-hand determinant and both the trace and determinant of $W$ via the standard two-by-two formulas. Unfold subtraction, scalar multiplication, and the identity matrix entrywise (sub_apply, smul_apply, one_apply, smul_eq_mul). Clear numeric coefficients with norm_num, then finish by ring on the resulting polynomial identity in the four entries of $W$ and the scalar $y$. No external RS lemmas are required; it is pure matrix algebra.
why it matters
This is the algebraic hinge between "has a real eigenvalue" and "satisfies the characteristic equation." The immediate consumer eigen_char states that a real eigenvalue $x$ is a root of $x^{2} - (\operatorname{tr} W)x + \det W = 0$, by showing $\det(W - x I) = 0$ and rewriting via this identity.
That root relation feeds balanced_conjugate, the circularity fence of the module: if $\det W = 1$ and $x \neq 0$ is a real eigenvalue, then $x^{-1}$ is also an eigenvalue, because the product of eigenvalues is the determinant. From there balanced_trace forces $\operatorname{Tr} W = x + x^{-1}$, and charAnomaly_eq_J identifies the character anomaly with the T5 cost $J(x) = (x + x^{-1})/2 - 1$. J appears nowhere in the inputs; it emerges from balance plus one eigenvalue.
In the broader forcing chain this is local linear algebra supporting the holography reduction of census pricing to seam-transfer structure, not a new physical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.