contract
plain-language theorem explainer
The contract definition maps any tensor of type (p+1, q+1) to the zero tensor of type (p, q). It appears in the relativity geometry scaffold and is referenced by downstream results on torsion-free connections and analytic RH bridges. The implementation is a direct constant function that ignores its input.
Claim. For any tensor $T$ of type $(p+1, q+1)$ the contraction yields the zero tensor of type $(p, q)$.
background
Tensor is defined as the scaffold abbreviation $(Fin 4 → ℝ) → (Fin p → Fin 4) → (Fin q → Fin 4) → ℝ$, representing a (p, q) tensor field on 4D spacetime. The module header states it is a SCAFFOLD MODULE — NOT PART OF CERTIFICATE CHAIN. The sole upstream dependency is this Tensor abbreviation itself.
proof idea
One-line definition that directly returns the constant zero function on the target type.
why it matters
Supplies a placeholder contraction used by levi_civita_torsion_free (which invokes it to establish torsion-freeness of the Christoffel symbols) and by direct_rh_from_honestPhaseChargeZeroBridge. The module doc-comment explicitly marks the entire file as outside the certificate chain, so the definition does not advance any T0-T8 forcing step or Recognition Composition Law identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.