`refinement_discharge_inherits`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence
domain: Foundation
line: 191 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence on GitHub at line 191.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 188    faces to divide the hypercube into simplices does not change
 189    the Regge action *provided* the new faces have zero deficit.
 190    Our `extra_trivial` predicate is exactly that provision. -/
 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
 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. -/
 210theorem refinement_calibrated {n : ℕ}
 211    (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 212    (R_at : ∀ ε : LogPotential n,
 213      SimplicialRefinement (cubicDeficitFunctional n)
 214        (conformal_edge_length_field a ha ε) (cubicHinges G)) :
 215    ∀ ε : LogPotential n,
 216      regge_sum (cubicDeficitFunctional n)
 217        (conformal_edge_length_field a ha ε) (R_at ε).hinges
 218      = jcost_to_regge_factor * laplacian_action G ε :=
 219  refinement_discharge_inherits a ha G R_at
 220
 221/-! ## §5. Diagnostic: the equivalence is fully invariant -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.