FieldHeightGradient.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Identification of the jointly constructed height gradient with the actual scalar magnetization. The terminal centering is retained explicitly.

lemma OAI.InvariantIsing.fieldFinite_centered_coordinate_derivative line 15
theorem OAI.InvariantIsing.fieldHeight_gradient_identification line 38
Source documentation
The exact literal-height gradient. F is derivative data constructed from the finite Gaussian recursion; the equality of its value is the only identification required here.
```
theorem fieldHeight_gradient_identification (h : FieldStep)
    {I : Set (Fin (h.depth + 1) → ℝ)} (F : FieldFiniteFamily (h.depth + 1) I)
    (hU : F.U = fieldFiniteValue (fieldHeightFiniteList h))
    (r : Fin (h.depth + 1) → ℝ) (hr : r ∈ I)
    (hs : r ∈ fieldStrictHeightCone h.depth) (i : Fin (h.depth + 1)) :
    F.P i (r, 0) - (if i = Fin.last h.depth then 1 / 2 else 0) =
      -(h.cut i.succ - h.cut i.castSucc) / 2 *
        fieldMagnetizationLevel (fieldStepOfStrictHeights h r hs) i := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.FieldFiniteFamily, OAI.InvariantIsing.fieldFiniteValue, OAI.InvariantIsing.fieldHeightFiniteList, OAI.InvariantIsing.fieldStrictHeightCone, OAI.InvariantIsing.fieldMagnetizationLevel, OAI.InvariantIsing.fieldStepOfStrictHeights