Paper X · Lean source
NormResidueBoundary.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
PaperX/NormResidueBoundary.lean29 lines
Original source path
current_continuation/lean/PaperX/NormResidueBoundary.leanSkip declarations and read code
1 import PaperX.NormResidueArithmetic
2
3 /-!
4 # Why the norm sign is part of a residue filter
5
6 The rational integers `-1` and `2` agree modulo `3`. Their signed norms agree
7 modulo `3`, but their principal ideal norms do not. This is an actual ideal
8 counterexample to omitting the sign hypothesis.
9 -/
10
11 namespace PaperX.NormResidue
12
13 theorem opposite_sign_elements_congruent :
14 (-1 : ℤ) - 2 ∈ modulusIdeal ℤ 3 := by
15 change (-1 : ℤ) - 2 ∈ Ideal.span {(3 : ℤ)}
16 exact Ideal.mem_span_singleton.mpr ⟨-1, by norm_num⟩
17
18 theorem opposite_sign_signed_norms_congruent :
19 (Algebra.norm ℤ (-1 : ℤ) : ZMod 3) = (Algebra.norm ℤ (2 : ℤ) : ZMod 3) := by
20 norm_num
21 decide
22
23 theorem opposite_sign_principal_norms_differ :
24 (Ideal.absNorm (Ideal.span {(-1 : ℤ)}) : ZMod 3) ≠
25 (Ideal.absNorm (Ideal.span {(2 : ℤ)}) : ZMod 3) := by
26 norm_num [Ideal.absNorm_span_singleton]
27 decide
28
29 end PaperX.NormResidue
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: bd8f56001e0298952b80caa4b01b17969989da9104a22fcc1363dc098b94e8fc
Back to Paper X: Universal Residual Seeds and Conditional Occupied-System Completion