J_composition_decomposition

formal source

 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:
 187- Costs add: J_total = J(a) + J(b)
 188- For consistency, scales should also combine additively
 189
 190This is the physical motivation for Axiom 2. -/
 191theorem J_cost_motivates_additive_composition :
 192    ∀ a b : ℝ, 0 < a → 0 < b → J a * J b = 0 →