J

formal source

 153/-! ## Why Additive Composition? A J-Cost Argument -/
 154
 155/-- The J-cost of a scale ratio -/
 156noncomputable def J (x : ℝ) : ℝ := Cost.Jcost x
 157
 158/-- Exact decomposition of the J-cost composition identity.
 159
 160This is the concrete RCL form specialized to `J`:
 161`J(ab) + J(a/b) = 2JaJb + 2Ja + 2Jb`. -/
 162theorem J_composition_decomposition (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
 163    J (a * b) + J (a / b) = 2 * J a * J b + 2 * J a + 2 * J b := by
 164  unfold J Cost.Jcost
 165  have ha0 : a ≠ 0 := ha.ne'
 166  have hb0 : b ≠ 0 := hb.ne'
 167  field_simp [ha0, hb0]
 168  ring
 169
 170/-- Additive regime for independent events.
 171
 172When the interaction term vanishes (`J a * J b = 0`), the pairwise
 173composition law reduces to pure additivity (up to the canonical factor 2). -/
 174theorem J_additive_for_independent (a b : ℝ) (ha : 0 < a) (hb : 0 < b)
 175    (h_independent : J a * J b = 0) :
 176    J (a * b) + J (a / b) = 2 * (J a + J b) := by
 177  have hcomp := J_composition_decomposition a b ha hb
 178  nlinarith [hcomp, h_independent]
 179
 180/-- **KEY INSIGHT**: The additive structure of J-cost motivates
 181    the additive structure of scale composition.
 182
 183For the scale sequence to "respect" the J-cost structure,
 184the composition of scales should parallel the composition of costs.
 185
 186When we compose events at scales a and b: