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

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/polynomial_prescribed/controls/InvalidRectangularUniqueness.lean

1 module
2 public import PolynomialTowerControls
3 @[expose] public section
4 open Komorebi.PolynomialTowerControls MvPolynomial
5 
6 -- Invalid: a surjective rectangular Jacobian permits free coordinates inside one residue ball.
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: 83a72d186c8000f224e7be38482a54c65280098f49e41dccd36ae8921fcdf457

Original source on GitHub

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