eta
plain-language theorem explainer
The eta definition supplies the flat Minkowski metric as a BilinearForm with signature (-,+,+,+). Workers in Regge calculus and linearized gravity cite it as the background for perturbations and Schläfli identities. It is introduced by direct case analysis on the index selector low.
Claim. The Minkowski metric is the bilinear form satisfying η(v₁, v₂, λ) = −1 when λ(0) = λ(1) = 0, +1 when λ(0) = λ(1) ∈ {1,2,3}, and 0 otherwise, where λ : Fin 2 → Fin 4 selects the two indices.
background
BilinearForm is the abbreviation (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ in Foundation.Hamiltonian, serving as a local non-sealed interface for bilinear forms; the Tensor module identifies it with Tensor 0 2. The Metric module imports Tensor and Derivatives to equip spacetime geometry with this tensor. The unrelated baryon-to-photon eta in Nucleosynthesis is a separate real constant and plays no role here.
proof idea
One-line definition that performs case distinction on whether the two indices chosen by low coincide, then on whether that index is zero.
why it matters
Eta supplies the flat background required by InverseMetric, by schlafli_identity in ReggeCalculus, and by linearizedDeficit and linear_regge_vanishes in DeficitLinearization. It anchors the eight-fold way constructions and directed-flux identities. The declaration realizes the flat metric consistent with the Recognition Science derivation of D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.