posting_dalembert

formal source

  77
  78This is the fundamental identity governing how posting potentials
  79compose.  It is equivalent to the RCL via the shift J = Π − 1. -/
  80theorem posting_dalembert (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
  81    PostingPotential (x * y) + PostingPotential (x / y) =
  82      2 * PostingPotential x * PostingPotential y := by
  83  unfold PostingPotential Jcost
  84  have hx_ne : x ≠ 0 := ne_of_gt hx
  85  have hy_ne : y ≠ 0 := ne_of_gt hy
  86  field_simp [hx_ne, hy_ne]
  87  ring
  88
  89/-! ## Extensivity in the Self-Similar Regime -/
  90
  91/-- For a geometric scale sequence with ratio σ, the posting potential
  92at level k is Π(σ^k).  The d'Alembert identity becomes:
  93
  94  Π(σ^{j+k}) + Π(σ^{j-k}) = 2 Π(σ^j) Π(σ^k)
  95
  96This is the RS-native form of "scale composition is governed by
  97the posting potential's multiplicative structure." -/
  98theorem posting_scales_compose (σ : ℝ) (hσ : 0 < σ) (j k : ℕ) :
  99    PostingPotential (σ ^ j * σ ^ k) + PostingPotential (σ ^ j / σ ^ k) =
 100      2 * PostingPotential (σ ^ j) * PostingPotential (σ ^ k) :=
 101  posting_dalembert (σ ^ j) (σ ^ k) (pow_pos hσ j) (pow_pos hσ k)
 102
 103/-! ## Additive Scale Composition from Closure -/
 104
 105/-- **Theorem**: Closure of a geometric scale sequence under additive
 106composition forces `scale 0 + scale 1 = scale 2`.
 107
 108This is the RS-internal replacement for the `HasAdditiveComposition`
 109axiom.  The additive structure is not assumed; it follows from the
 110physical requirement that composing level-0 and level-1 events must