A registered result in its source context

FORM.FLAVOR.FEEDBACK.01

Original ledger classification: Formal [F] (Lean kernel; the action identities, the inverse-free conjugation, charpoly in Z[X], the SNF determinantal divisors -- with the Z2^2-not-mu4 typing doc-level)

Original claim text

LEAN 4 FORMALISATION of the feedback normal form (2026-08-08 round 36; TfptCarrier/FlavorFeedback.lean, 16 declarations, 11 theorems) -- AUDIT: PASS, no sorry, no native_decide, no domain axioms (#print axioms = propext, Classical.choice, Quot.sound on every theorem; lake build green 3418 jobs). Kernel-checked over Z with a SYMBOLIC s (no numeric specialization smuggled in): the three action identities R_s b0 = (s+4) b0 + 4 b2, R_s b1 = b2, R_s b2 = 3 b0 - 2 b1 + 5 b2 (the deformation enters ONLY through b0); THE CONJUGATION P F_s = R_s P (the inverse-free house form -- det P = -4 != 0 makes it P^{-1} R_s P = F_s over Q); THE CHARACTERISTIC POLYNOMIAL chi_{R_s}(X) = (X - (s+4))(X^2 - 5X + 2) - 12X in Z[X] via Matrix.charpoly and the 3x3 determinant expansion, with the s = 6 instance chi_L = X^3 - 15X^2 + 40X - 20; and THE LATTICE INDEX facts det P = -4, gcd(entries) = 1, gcd(2x2 minors) = 2 -- the determinantal divisors d1 = 1, d1 d2 = 2, d1 d2 d3 = 4 forcing the invariant factors (1, 2, 2), SNF diag(1,2,2), quotient Z2 (+) Z2. THE HONEST TYPING deliberately NOT a claimed isomorphism: Z2^2 has the CARDINALITY of mu4 but is not mu4 as a group -- the SNF computed in Lean is what makes that distinction kernel-checked rather than blurred. Mirrored numerically in v874 part C.

Original classification detail

Formal [F]: the feedback normal form is a Lean theorem family (11 theorems), standard axioms only, no sorry, full build green.

Dependencies as recorded

FLAVOR.FEEDBACK.NORMALFORM.01; FORM.QGEO.01