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

refinement_discharge_inherits

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)

 191theorem refinement_discharge_inherits {n : ℕ}
 192    (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 193    (R_at : ∀ ε : LogPotential n,
 194      SimplicialRefinement (cubicDeficitFunctional n)
 195        (conformal_edge_length_field a ha ε) (cubicHinges G)) :
 196    ∀ ε : LogPotential n,
 197      regge_sum (cubicDeficitFunctional n)
 198        (conformal_edge_length_field a ha ε) (R_at ε).hinges
 199      = jcost_to_regge_factor * laplacian_action G ε := by

proof body

Term-mode proof.

 200  intro ε
 201  rw [regge_sum_refinement_invariant (cubicDeficitFunctional n)
 202        (conformal_edge_length_field a ha ε) (cubicHinges G) (R_at ε)]
 203  exact cubic_linearization_discharge a ha G ε
 204
 205/-- **COROLLARY.** Under the same conditions, the refinement-level
 206    calibration against the ledger graph `G` holds: the Regge sum
 207    on the refined hinge list equals `κ · laplacian_action`.
 208    This means the `CalibratedAgainstGraph` predicate (from
 209    `SimplicialDeficitDischarge.lean`) carries over to refinements. -/

used by (2)

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

depends on (19)

Lean names referenced from this declaration's body.