506theorem dirichletForm_flat 507 {n : ℕ} (M : Fin n → Fin n → ℝ) : 508 dirichletForm M (fun _ : Fin n => (0 : ℝ)) = 0 := by
proof body
Tactic-mode proof.
509 unfold dirichletForm 510 have : ∀ i j : Fin n, M i j * ((0 : ℝ) - (0 : ℝ)) ^ 2 = 0 := by 511 intro i j; ring 512 simp only [this, Finset.sum_const_zero, mul_zero] 513 514/-! ## §5. Connection to the existing infrastructure 515 516The reduction here is the *concrete second-order content* of the 517hypothesis `EdgeLengthFromPsi.ReggeDeficitLinearizationHypothesis`. We 518record the connection: a `WeakFieldReggeData` together with the 519Schläfli row-sum property gives a candidate discharge of the 520linearization hypothesis at the bilinear level. -/ 521 522/-- The Dirichlet weights `A_{ij}` derived from `WeakFieldReggeData` 523 define a `WeightedLedgerGraph` provided they are non-negative. 524 Non-negativity is a property of the lattice (e.g., automatic for 525 regular cubic lattices where `A_{ij}` is a true area), so we 526 package it as an explicit hypothesis. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.