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