Paper IX · Lean source

InvalidDroppingLowerResidue.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

polynomial_counts/controls/InvalidDroppingLowerResidue.lean9 lines

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/polynomial_counts/controls/InvalidDroppingLowerResidue.lean

1 module
2 public import PolynomialCountControls
3 @[expose] public section
4 open Komorebi.PolynomialCountControls
5 
6 -- Invalid: the prescribed-lower-residue count cannot count every root modulo four.
7 example : Nat.card {y : Fin 1 → ZMod 4 //
8     ∀ i, (4 : ℤ) ∣ MvPolynomial.eval (fun k => ((y k).val : ℤ)) (zeroSystem i)} = 2 := by
9   exact unrestricted_zero_root_count

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 1850d768a4336dc30da9dd144e74150f8ef9359621f0084b725dead481c996ca

Original source on GitHub

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation