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

CubicSimplicialInvarianceCert

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)

 233structure CubicSimplicialInvarianceCert where
 234  regge_append : ∀ {n : ℕ}
 235    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 236    (h₁ h₂ : List (HingeDatum n)),
 237    regge_sum D L (h₁ ++ h₂)
 238      = regge_sum D L h₁ + regge_sum D L h₂
 239  trivial_hinge_drop : ∀ {n : ℕ}
 240    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 241    (hinges extra : List (HingeDatum n)),
 242    (∀ h ∈ extra, HingeTrivial D L h) →
 243    regge_sum D L (hinges ++ extra) = regge_sum D L hinges
 244  refinement_invariant : ∀ {n : ℕ}
 245    (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 246    (original : List (HingeDatum n))
 247    (R : SimplicialRefinement D L original),
 248    regge_sum D L R.hinges = regge_sum D L original
 249  refinement_discharge : ∀ {n : ℕ}
 250    (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 251    (R_at : ∀ ε : LogPotential n,
 252      SimplicialRefinement (cubicDeficitFunctional n)
 253        (conformal_edge_length_field a ha ε) (cubicHinges G)),
 254    ∀ ε : LogPotential n,
 255      regge_sum (cubicDeficitFunctional n)
 256        (conformal_edge_length_field a ha ε) (R_at ε).hinges
 257      = jcost_to_regge_factor * laplacian_action G ε
 258

used by (1)

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.