def
definition
equivZModTwo
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 928.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
925 fin_cases i <;> simp [reciprocal_ne_id]
926
927/-- **Closed automorphism theorem**: `Aut(J)` is exactly `ℤ/2ℤ`. -/
928noncomputable def equivZModTwo : JAut ≃ ZMod 2 :=
929 equivFinTwo.trans (ZMod.finEquiv 2).toEquiv
930
931end JAut
932
933/-- Paper-facing closed automorphism theorem:
934 the only continuous multiplicative bijections on `ℝ_{>0}` preserving `J`
935 are the identity and reciprocal maps. The continuity and bijectivity
936 assumptions are stronger than needed; the proof uses the sharper `JAut`
937 classification above. -/
938theorem continuous_bijective_preserves_J_eq_id_or_inv
939 {f : PosReal → PosReal} (_hCont : Continuous f) (_hBij : Function.Bijective f)
940 (hmul : ∀ x y : PosReal, f (posMul x y) = posMul (f x) (f y))
941 (hJ : ∀ x : PosReal, J (f x).1 = J x.1) :
942 f = (fun x => x) ∨ f = posInv := by
943 let g : JAut := ⟨f, ⟨hmul, hJ⟩⟩
944 rcases JAut.eq_id_or_reciprocal g with hg | hg
945 · left
946 funext x
947 have hx : g x = JAut.id x := by
948 simpa using congrArg (fun h : JAut => h x) hg
949 simpa [g, JAut.id] using hx
950 · right
951 funext x
952 have hx : g x = JAut.reciprocal x := by
953 simpa using congrArg (fun h : JAut => h x) hg
954 simpa [g, JAut.reciprocal] using hx
955
956/-! ## §9. Summary Certificate -/
957
958/-- **COST ALGEBRA CERTIFICATE**