Degree-five Independence and a Nonzero Explicit Jacobian Class

Algebraic milestone note, version 1.1. For a field K and k ≠ 0, the classes of y^5, xy^4, x^2y^3 and x^3y^2 are linearly independent in the quotient K[x,y]/(5kx^4y, kx^5 + 6y^5). The proof uses degree-five coefficient functionals L_0(p) = k·coeff_(0,5)(p) − 6·coeff_(5,0)(p) and L_i(p) = coeff_(i,5−i)(p), i = 1, 2, 3, which annihilate every element of the full ideal (arbitrary polynomial multipliers). In characteristic zero, the Stage 3 section identity and the Stage 2 exact coefficient certificate then imply that the quotient class of HW is nonzero at every root of the degree-24 modulus, and a complex root exists (non-vacuity). What Lean checks. The 13 theorems of Hodge/ExplicitJacobianIndependence.lean, including degreeFiveClasses_linearIndependent, section_HW_class_ne_zero and exists_complex_nonzero_HW_class. No basis, nontriviality, independence or geometric hypothesis is assumed; the hypothesis-to-assumption table is in README.md (no mismatch). Not proved: a spanning theorem for the degree-five component or a basis of the quotient. Not claimed. No residue, cohomology, Hodge-type, cycle-class, descent or Hodge-conjecture statement is proved or claimed. In the HODGE repository the geometric bridges (for example ChainSexticCharacterBridge and the cycle class map) remain explicit hypotheses, not theorems; this record does not change that. Reproducibility. Full Lean source: BenFrohman/HODGE at 4c768890dc88bc180bf10887e4ba1b426f33a41a (tip of main on 11 November 2026; a git archive zip of that commit is attached). The paper cites code commit 52325b0; the Lean sources, scripts, lakefile, manifest and toolchain are byte-identical between that commit and 4c76889. Lean leanprover/lean4:v4.22.0, Mathlib 79e94a093aff4a60fb1b1f92d9681e407124c2ca. One-command rebuild from the repository root: lake exe cache get && lake build && python3 scripts/check_residue_axioms.py. GitHub Actions on main at 4c76889 passed (Lean certificate 42935333059, Lean 42935333161, Paper 42935333072). On 11 November 2026 the pinned commit was rebuilt locally from scratch for the project modules (attached build.log); the attached axiom output (axiom-output-residue.txt: PASS, 78 incremental declarations; axiom-output-root.txt: 699 of 699 declarations) shows only propext, Classical.choice and Quot.sound (or a subset), and the attached scan found no sorry, admit, native_decide or axiom declarations. SHA256SUMS lists every attached file. Limits. A kernel check shows that the stated Lean propositions follow from the stated Lean definitions. It does not show that those definitions model any geometric or physical object.