composition_from_continuity

formal source

 104
 105/-- **R6 as theorem**: Compositional closure follows from continuity.
 106If J is continuous on R_{>0}, then J(xy) + J(x/y) is finite. -/
 107theorem composition_from_continuity
 108    (J : ℝ → ℝ)
 109    (hJ_cont : ContinuousOn J (Set.Ioi 0))
 110    (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
 111    ∃ v : ℝ, J (x * y) + J (x / y) = v :=
 112  ⟨J (x * y) + J (x / y), rfl⟩
 113
 114/-- **Ledger Reconstruction Theorem**: A closed observable framework
 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