ledger_reconstruction

formal source

 115canonically carries a zero-parameter comparison ledger.
 116R1, R2, R5, R6 are proved; the remaining seam is tracked as three explicit
 117finite-description obligations rather than one broad regularity hypothesis. -/
 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 :=
 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⟩ }