fieldTheoryStub
plain-language theorem explainer
This definition supplies a stub instance of the FieldTheoryFacts structure in the relativity fixtures module. It would be referenced by any proof that needs to assume trace-free stress-energy and conservation without committing to a concrete Lagrangian. The implementation satisfies both properties through direct simplification after introducing the field, metric, volume, and coupling parameters.
Claim. A noncomputable definition that furnishes an instance of the field theory facts interface in which the stress-energy tensor is trace-free and the conservation theorem holds for arbitrary fields, metrics, volumes, and mass-squared parameters.
background
The module NewFixtures supplies stub instances for hypothesis classes that replace sorries while keeping them outside production namespaces. FieldTheoryFacts is the structure whose two fields are stress_energy_trace_free (asserting the trace vanishes) and conservation_theorem (asserting the divergence identity). The stub therefore lets relativity derivations proceed under a minimal interface without yet specifying dynamics.
proof idea
One-line wrapper that applies simp after introducing the variables for each field. The first field uses intro ψ g vol α x followed by simp [FieldTheoryFacts]; the second uses intro ψ g vol α m_squared h then intro ν x and the same simp.
why it matters
The stub closes a scaffolding gap in the relativity section so that downstream theorems can cite FieldTheoryFacts without unresolved sorries. It therefore supports the larger program of deriving gravitational and field equations from the Recognition functional equation while preserving a clean trust boundary between hypothesis interfaces and proved content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.