Paper IX · Lean source
SharedCorrectionContract.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/SharedCorrectionContract.lean25 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/shared_correction/controls/SharedCorrectionContract.leanSkip declarations and read code
1 module
2
3 public import SharedCorrection
4
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8
9 namespace Komorebi.SharedCorrectionContract
10
11 /-- External statement contract: the quotient and simultaneous correction
12 condition are written explicitly, with no compatibility premise added. -/
13 theorem explicit_quotient_contract
14 (R U V W : Type*) [CommRing R]
15 [AddCommGroup U] [Module R U]
16 [AddCommGroup V] [Module R V]
17 [AddCommGroup W] [Module R W]
18 (J : U →ₗ[R] V) (K : U →ₗ[R] W) (u v : U) :
19 (Submodule.Quotient.mk u : U ⧸ (LinearMap.ker J ⊔ LinearMap.ker K)) =
20 Submodule.Quotient.mk v ↔ ∃ w : U, J w = J u ∧ K w = K v :=
21 SharedCorrection.quotient_mk_eq_iff_common J K u v
22
23 end Komorebi.SharedCorrectionContract
24
25 #print axioms Komorebi.SharedCorrectionContract.explicit_quotient_contract
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: 4aec4fc0ee27d21e0c98de6ebf66e2c331a278347a95b60c7988ec3e75eca89f
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation