`of`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
domain: Foundation
line: 42 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.DAlembert.LedgerFactorization on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  39
  40/-- Regrouping invariance: the combiner is symmetric and satisfies the
  41boundary and normalization conditions forced by the abelian group
  42structure of `(ℝ₊, ×)` and the calibration of `J`. -/
  43structure RegroupingInvariance (J : ℝ → ℝ) extends ContextualSubstitutivity J where
  44  symmetric : ∀ u v, combiner u v = combiner v u
  45  zero_boundary : ∀ u, combiner u 0 = 2 * u
  46  unit_diagonal : combiner 1 1 = 6
  47  right_affine : ∀ u, ∃ α β, ∀ v, combiner u v = α * v + β
  48
  49/-- Contextual substitutivity is forced by the ledger's comparison
  50structure: if `J(x₁) = J(x₂)`, then for any `y > 0`,
  51
  52  `J(x₁ y) + J(x₁/y) = J(x₂ y) + J(x₂/y)`
  53
  54because the compound cost depends only on the mismatch, not on the
  55specific ratio realizing it.  Therefore the compound cost descends
  56to a function of `(J(x), J(y))`. -/
  57def substitutivity_forces_factorization
  58    (J : ℝ → ℝ) (hJ0 : J 1 = 0)
  59    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
  60    (P : ℝ → ℝ → ℝ)
  61    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
  62      J (x * y) + J (x / y) = P (J x) (J y)) :
  63    ContextualSubstitutivity J :=
  64  ⟨P, hComp⟩
  65
  66/-- Symmetry of the combiner follows from commutativity of `(ℝ₊, ×)`:
  67`J(xy) + J(x/y) = J(yx) + J(y/x)` because `xy = yx` and
  68`J(x/y) = J(y/x)` by reciprocal symmetry. -/
  69theorem combiner_symmetric
  70    (J : ℝ → ℝ)
  71    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
  72    (P : ℝ → ℝ → ℝ)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.