pith. machine review for the scientific record. sign in
theorem proved term proof

exact_flat_agrees_with_linearized

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 238theorem exact_flat_agrees_with_linearized {n : ℕ}
 239    (G : WeightedLedgerGraph n) :
 240    exactJCostAction G (fun _ => (0 : ℝ))
 241      = laplacian_action G (fun _ => (0 : ℝ)) := by

proof body

Term-mode proof.

 242  rw [exact_decomposition, laplacian_action_flat G]
 243  unfold quarticRemainder coshRemainder
 244  simp
 245
 246/-! ## §5. The non-linear J ↔ Regge hypothesis
 247
 248In the weak-field regime, `CubicDeficitDischarge.cubic_linearization_discharge`
 249makes the J ↔ Regge identity a theorem. Beyond that regime, one needs
 250the corresponding non-linear statement, which is what Cayley-Menger
 251calculations on a simplicial mesh produce in the limit.
 252
 253We package that as an explicit hypothesis, NOT an axiom. -/
 254
 255/-- A *non-linear deficit-angle functional*: an extension of the
 256    linear functional to strong-field configurations. Concretely
 257    it is a `DeficitAngleFunctional` that additionally satisfies
 258    the non-linear matching identity below. -/

depends on (35)

Lean names referenced from this declaration's body.

… and 5 more