posting_pos

formal source

  65  simp [inv_one]
  66
  67/-- Π(x) > 0 for all x > 0. -/
  68theorem posting_pos (x : ℝ) (hx : 0 < x) : 0 < PostingPotential x := by
  69  unfold PostingPotential Jcost
  70  have hx_ne : x ≠ 0 := ne_of_gt hx
  71  have h := sq_nonneg (x - x⁻¹)
  72  have hx_inv_pos : 0 < x⁻¹ := inv_pos.mpr hx
  73  nlinarith [mul_pos hx hx_inv_pos]
  74
  75/-- The d'Alembert identity for the posting potential:
  76Π(xy) + Π(x/y) = 2 Π(x) Π(y).
  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 : ℕ) :