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))`. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.