contracted_bianchi
plain-language theorem explainer
The declaration defines the contracted Bianchi identity as the statement that the divergence of the Einstein tensor vanishes identically in every component. A general-relativity theorist cites this geometric fact when extracting stress-energy conservation from the Einstein equations without invoking dynamics. The definition directly encodes the zero-divergence condition on the supplied divergence function.
Claim. The contracted Bianchi identity holds when the divergence of the Einstein tensor satisfies $div_G^nu = 0$ for every index $nu$, where the Einstein tensor is constructed from the metric tensor, its inverse, the Christoffel symbols, and their first derivatives.
background
The module defines the stress-energy tensor from the variation of the matter action and derives its conservation law. It introduces the metric tensor met, its inverse ginv, coordinate Christoffel symbols gamma, and their derivatives dgamma; div_G stands for the coordinate divergence of the Einstein tensor built from these objects. The local setting is the conservation chain that proves Axiom 3 (matter coupling) in the Recognition framework: the geometric Bianchi identity plus the Einstein field equations plus metric compatibility imply nabla^mu T_mu nu = 0.
proof idea
This is a one-line definition that directly asserts the property forall nu : Idx, div_G nu = 0. No lemmas or tactics are applied; the body simply states the zero-divergence condition that constitutes the contracted Bianchi identity.
why it matters
The definition supplies the geometric premise required by the downstream sibling conservation_from_efe_and_bianchi, which combines it with the Einstein field equations to obtain stress-energy conservation. It fills the purely geometric step in the proof of Axiom 3 (matter coupling) inside the Recognition Science framework; the identity follows from Riemann-tensor symmetries and holds independently of the phi-ladder or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.