SingleCandidateComparison.lean

1 import PaperXI.LocalFactorIdentification
2 
3 /-! The one-candidate local-factor comparison used in the manuscript.
4 The candidate and its admissibility are supplied. Matching factors are required
5 only for this candidate. No atom-realization existence field is consumed.
6 The separating factor system remains an explicit classical input. -/
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperXI.SingleCandidateComparison
11 open LocalFactorIdentification
12 
13 variable {Atom Test Value : Type*} {s : Setoid Atom}
14 
15 /-- Equality of the declared factor profile identifies this supplied candidate
16 with the reference in the declared isomorphism quotient. -/
17 theorem source (S : FactorSystem s Test Value)
18     (candidate reference : Atom)
19     (hcandidate : S.admissible candidate) (hreference : S.admissible reference)
20     (expected : Test → Value)
21     (h5 : S.profile candidate = expected)
22     (href : S.profile reference = expected) :
23     Quotient.mk s candidate = Quotient.mk s reference := by
24   apply (class_eq_iff S hcandidate hreference).mpr
25   exact h5.trans href.symm
26 
27 end PaperXI.SingleCandidateComparison

Back to source controls