Paper IX · Lean source
InvalidQuotientEquality.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.
shared_correction/controls/InvalidQuotientEquality.lean9 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/shared_correction/controls/InvalidQuotientEquality.lean1 import SharedCorrectionControls
2
3 open Komorebi.SharedCorrection Komorebi.SharedCorrectionControls
4
5 -- EXPECTED FAILURE: the missing compatibility cannot be proved by reflexivity.
6 example : (Submodule.Quotient.mk (0 : Two) : Common identity identity) =
7 Submodule.Quotient.mk (1 : Two) := by
8 apply (quotient_mk_eq_iff_common identity identity 0 1).mpr
9 exact ⟨0, rfl, rfl⟩
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: 1277303386a4ec98d8b5a0110fbc3e6f15e02aab5cc5757696b5750efeedb6b6
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation