kronecker
plain-language theorem explainer
Kronecker delta definition on Fin n indices, equal to 1 on the diagonal and 0 off it. Post-Newtonian metric inverse checks cite it when bounding contraction error below 0.001. The implementation is a direct conditional on index equality with no lemmas or tactics.
Claim. The Kronecker delta function on indices in Fin n is defined by $d = 1$ if the two indices coincide and $d = 0$ otherwise.
background
The module supplies placeholder manifold, point, tangent vector, and index structures for relativity geometry. It is explicitly a scaffold for type-checking only and lies outside the verified Recognition Science certificate chain. The Kronecker delta is introduced to support index contractions in coordinate-based expressions for post-Newtonian approximations.
proof idea
The declaration is a direct definition by cases on whether the two indices are equal.
why it matters
It supplies the index delta used by the diagonal, off-diagonal, and symmetry lemmas, which in turn support the inverse_1PN_correct bound on the 1PN metric contraction. The definition fills a structural placeholder role in the relativity geometry scaffold without touching the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.