MatrixBridgeAccepts
plain-language theorem explainer
MatrixBridgeAccepts defines acceptance of a matrix bridge B precisely when its 4x4 real matrix has nonzero determinant. Researchers examining the relativity-geometry interface would cite this placeholder to enforce basic invertibility before any embedding. The definition is a direct one-line predicate on the structure's matrix field.
Claim. A matrix bridge $B$ is accepted if and only if $B$ is invertible, i.e., $B$ has nonzero determinant.
background
MatrixBridge is a minimal placeholder structure that holds a single field matrix : Matrix (Fin 4) (Fin 4) ℝ, defaulting to the identity. The local module is explicitly labeled a scaffold and is excluded from the verified certificate chain. An analogous structure appears upstream in YM.Kernel, where MatrixBridge carries an intertwine condition between a transfer kernel and a matrix view.
proof idea
The definition is a one-line predicate that extracts the matrix field of the supplied bridge and asserts its determinant is nonzero.
why it matters
This definition supplies the basic acceptance predicate used by the downstream lemma matrixBridge_accepts_identity to verify the identity case. It sits inside a scaffold module whose documentation states it is not part of the verified certificate chain and should not be cited as proven mathematics. No link is made to core Recognition Science objects such as the J-cost or the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.