posting_one

formal source

  60noncomputable def PostingPotential (x : ℝ) : ℝ := Jcost x + 1
  61
  62/-- Π(1) = 1: the posting potential is normalized. -/
  63theorem posting_one : PostingPotential 1 = 1 := by
  64  unfold PostingPotential Jcost
  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