  89/-! ## §2. A single-edge hinge datum -/
  90
  91/-- Build a hinge datum carrying a single ordered edge and its weight. -/
  92def singletonHinge {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
  93    HingeDatum n :=
  94  { edges := [(i, j)]
  95  , weight := fun e => if e = (i, j) then w else 0
  96  , weight_nonneg := by
  97      intro e
  98      by_cases h : e = (i, j)
  99      · simp [h, hw]
 100      · simp [h]
 101  }
 102
 103theorem singletonHinge_weight {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 104    (singletonHinge i j w hw).weight (i, j) = w := by
 105  unfold singletonHinge; simp
 106
 107theorem singletonHinge_edges {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 108    (singletonHinge i j w hw).edges = [(i, j)] := by
 109  unfold singletonHinge; rfl
 110
 111/-! ## §3. The cubic deficit functional via pattern matching -/
 112
 113/-- Deficit at a hinge: if the hinge carries a single edge `(i, j)`,
 114    return `(ε_i − ε_j)²`; otherwise return 0. -/
 115def cubicDeficit {n : ℕ} (L : EdgeLengthField n) (h : HingeDatum n) : ℝ :=
 116  match h.edges with
 117  | [(i, j)] => (recoverEps L i - recoverEps L j) ^ 2
 118  | _ => 0
 119
 120/-- Area at a hinge: if the hinge carries a single edge `(i, j)`,
 121    return `(κ/2) · (h.weight (i, j))`; otherwise return 0. -/
 122def cubicArea {n : ℕ} (_L : EdgeLengthField n) (h : HingeDatum n) : ℝ :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.