J_log

formal source

  64This is what makes J-cost equivalent to the Regge action. -/
  65
  66/-- J-cost in log coordinates: J(eᵋ) = cosh(ε) − 1 -/
  67def J_log (ε : ℝ) : ℝ := Jcost (Real.exp ε)
  68
  69/-- The quadratic approximation of J in log coordinates. -/
  70def J_log_quadratic (ε : ℝ) : ℝ := ε ^ 2 / 2
  71
  72/-- The quartic error bound. For |ε| < 1, the error in the
  73    quadratic approximation is bounded by ε⁴/24.
  74    This is the standard Taylor remainder for cosh. -/
  75def J_log_error_bound (ε : ℝ) : ℝ := |ε| ^ 4 / 24
  76
  77/-! ## The Coupling Cost
  78
  79The cost of a mismatch between neighboring simplices. -/
  80
  81/-- The coupling cost between two simplices with log-potentials ε₁, ε₂.
  82    J(ψ₁/ψ₂) = J(e^(ε₁−ε₂)) ≈ (ε₁−ε₂)²/2 at leading order. -/
  83def coupling_cost (ε₁ ε₂ : ℝ) : ℝ := Jcost (Real.exp (ε₁ - ε₂))
  84
  85/-- The quadratic approximation of the coupling cost. -/
  86def coupling_quadratic (ε₁ ε₂ : ℝ) : ℝ := (ε₁ - ε₂) ^ 2 / 2
  87
  88/-! ## Discrete Laplacian Structure
  89
  90The quadratic J-cost coupling is a discrete Laplacian action.
  91On a simplicial complex with N simplices and adjacency weights w_ij:
  92
  93  S_quadratic = (1/2) Σ_{i~j} w_ij · (ε_i − ε_j)²
  94
  95This is the standard graph Laplacian energy. -/
  96
  97/-- A weighted simplicial graph representing the ledger. -/