Paper IX · Lean source

InvalidRectangularUniqueness.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_towers/controls/InvalidRectangularUniqueness.lean11 lines

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/polynomial_towers/controls/InvalidRectangularUniqueness.lean

1 module
2 public import PolynomialTowerControls
3 @[expose] public section
4 open Komorebi.PolynomialTowerControls MvPolynomial
5 
6 -- Invalid: surjectivity for the one-by-two projection Jacobian does not eliminate its free coordinate.
7 example : ∀ a b : Fin 2 → ℤ_[2],
8     (∀ i, eval₂ (Int.castRingHom ℤ_[2]) a (projectionSystem i) = 0) →
9     (∀ i, eval₂ (Int.castRingHom ℤ_[2]) b (projectionSystem i) = 0) →
10     (∀ i, (2 : ℤ_[2]) ∣ b i - a i) → a = b := by
11   exact projection_two_padic_roots

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: ad7dc8795152436ac6febf1e7abc2b4acd963cd11b7e1b691bf016a33865d40f

Original source on GitHub

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