Paper IX · Lean source

InvalidGlobalUniqueness.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/InvalidGlobalUniqueness.lean11 lines

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/polynomial_prescribed/controls/InvalidGlobalUniqueness.lean

1 module
2 public import PolynomialDeformationControls
3 @[expose] public section
4 open Komorebi.PolynomialDeformationControls MvPolynomial
5 
6 -- Invalid: the checked bijective Jacobian at one does not make X²−1 globally injective.
7 -- The positive control proves two actual p-adic roots in different residue balls.
8 example : ∀ a b : Fin 1 → ℤ_[3],
9     (∀ i, eval₂ (Int.castRingHom ℤ_[3]) a (squareMinusOne i) = 0) →
10     (∀ i, eval₂ (Int.castRingHom ℤ_[3]) b (squareMinusOne i) = 0) → a = b := by
11   exact square_minus_one_not_global_unique

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: 6b06c8bf5c74c36a9a8d389246614ade672b852b0328d7a51e471a98a7f70744

Original source on GitHub

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