minkowskiMatrix
plain-language theorem explainer
Defines the Minkowski metric matrix as the 4 by 4 diagonal with signature (-,+,+,+). Any attempt to embed flat spacetime into the Recognition ledger would reference this placeholder. The implementation is a direct diagonal construction that distinguishes the time component by index value.
Claim. $η_{μν} = diag(-1,1,1,1)$
background
The module supplies a minimal placeholder for matrix representations in relativity geometry. Module documentation states the file is a scaffold and not part of the verified certificate chain. Upstream dependencies consist of structural 'is' declarations from OptionAEmpiricalProgram, SimplicialLedger.EdgeLengthFromPsi, MechanismDesignFromSigma, RamanujanBridge.MockThetaPhantom, and RecogSpec.Core.Bridge that function as hypothesis interfaces or combinatorial extensions.
proof idea
The definition is a one-line wrapper that applies the diagonal matrix constructor with a conditional on the index value.
why it matters
This placeholder occupies the matrix bridge slot in the relativity section but carries no verified status. Module documentation explicitly warns against citing these definitions as proven mathematics. No parent theorems or downstream results depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.