pith. machine review for the scientific record. sign in
def definition def or abbrev

CalibratedAgainstGraph

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)

  80def CalibratedAgainstGraph {n : ℕ}
  81    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
  82    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=

proof body

Definition body.

  83  ∀ ε : LogPotential n,
  84    regge_sum D (conformal_edge_length_field a ha ε) hinges
  85      = jcost_to_regge_factor * laplacian_action G ε
  86
  87/-- Trivial observation: `CalibratedAgainstGraph` and
  88    `ReggeDeficitLinearizationHypothesis` are definitionally the same
  89    statement. The rename clarifies that the matching is a *property*
  90    of the functional, not a result of the linearization per se. -/

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (24)

Lean names referenced from this declaration's body.