kronecker_off_diag
The declaration states that the Kronecker delta on indices from a finite set of size n equals zero whenever the indices differ. It would be invoked in coordinate-basis calculations on the manifold to drop off-diagonal contributions. The proof is a one-line simplification that unfolds the definition of kronecker and applies the supplied inequality.
claimLet $n$ be a natural number and let $μ, ν$ be elements of the finite set with $n$ elements. If $μ ≠ ν$, then the Kronecker delta $δ_{μν}$ equals 0.
background
The module supplies placeholder type definitions for manifold objects (points, tangent vectors, covectors, spacetime indices via Fin n) to support relativity geometry infrastructure. The Kronecker delta itself is introduced by the sibling definition kronecker as the function that returns 1 when its two Fin n arguments are equal and 0 otherwise. The module documentation explicitly labels the entire file a scaffold that is not part of the verified certificate chain and warns against citing its contents as rigorous mathematics. Upstream structures supply context on J-cost convexity, spectral emergence of gauge groups, and nuclear density tiers, but none of these are invoked by the present theorem.
proof idea
The proof is a one-line wrapper that invokes the simp tactic on the definition of kronecker together with the hypothesis that the indices are unequal, which reduces the expression directly to 0 by the if-then-else case in the definition.
why it matters in Recognition Science
The result supplies an elementary index identity used in any tensor manipulation that relies on the Kronecker delta within the manifold layer. It stands next to the sibling declarations kronecker_symm and kronecker_diag. Because the module is declared a scaffold outside the certificate chain, the theorem does not feed any downstream verified result and does not close any step in the T0-T8 forcing chain or the Recognition Composition Law. It merely supports placeholder index arithmetic in a setting that ultimately aims at D = 3 spatial dimensions.
scope and limits
- Does not formalize any differential geometry beyond typed placeholders.
- Does not prove properties of the metric or curvature tensors.
- Does not connect to J-uniqueness, phi-ladder, or the eight-tick octave.
- Does not supply physical constants or mass formulas.
- Does not participate in the verified certificate chain.
formal statement (Lean)
77theorem kronecker_off_diag {n : ℕ} (μ ν : Fin n) (h : μ ≠ ν) :
78 kronecker μ ν = 0 := by
proof body
Term-mode proof.
79 simp [kronecker, h]
80
81/-- Partial derivative of a scalar function using a directional derivative along the basis vector. -/