def
definition
def or abbrev
ledger_reconstruction
show as:
view Lean formalization →
formal statement (Lean)
118noncomputable def ledger_reconstruction
119 (F : ClosedObservableFramework)
120 (J : ℝ → ℝ)
121 (hJ_sym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
122 (hJ_unit : J 1 = 0)
123 (hJ_reg : FiniteDescriptionRegularity J)
124 (hJ_suff : ∀ (x₁ x₂ y : ℝ), 0 < x₁ → 0 < x₂ →
125 J x₁ = J x₂ → 0 < y →
126 J (x₁ * y) + J (x₁ / y) = J (x₂ * y) + J (x₂ / y)) :
127 ZeroParameterComparisonLedger :=
proof body
Definition body.
128 let hJ_legacy := hJ_reg.toRegularityCert
129 let ⟨hJ_cont, hJ_conv, hJ_cal⟩ := hJ_legacy
130 { Carrier := F.S
131 carrier_nonempty := by obtain ⟨s₁, _, _⟩ := F.nontrivial; exact ⟨s₁⟩
132 carrier_countable := F.S_countable
133 cost :=
134 { J := J
135 reciprocal_sym := hJ_sym
136 unit_norm := hJ_unit
137 strict_convex := hJ_conv
138 continuous := hJ_cont
139 calibration := hJ_cal }
140 charge :=
141 { charge := F.charge
142 charge_conserved := fun _ _ _ => trivial }
143 no_free_knobs := F.no_continuous_moduli
144 cost_sufficient := hJ_suff
145 has_composition := fun x y hx hy =>
146 ⟨fun a _ => J (x * y) + J (x / y), rfl⟩
147 composition_continuous := fun x y hx hy =>
148 ⟨fun a _ => J (x * y) + J (x / y), continuous_const, rfl⟩ }
149
150end ClosedFramework
151end Foundation
152end IndisputableMonolith