fixedStressFlux
plain-language theorem explainer
Local name for the direction-indexed flux of a fixed 4×4 stress matrix along a covector: the quadratic contraction T_μν k^μ k^ν. Gravity authors cite it when packaging fixed-stress scalar maps without importing HorizonIndexedRecordFlux. The body is a one-line definitional alias of the bridge quadratic contraction.
Claim. For a real $4\times 4$ matrix $T$ and a covector $k\in\mathbb{R}^4$, the fixed stress flux is the quadratic contraction $\sum_{i,j} T_{ij}\,k_i k_j$ (i.e. $T_{\mu\nu}k^\mu k^\nu$).
background
This module is the Phase-5 algebraic prerequisite: finite-dimensional real linear algebra showing that the values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix modulo a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$. It is a rigidity package only. It does not identify matrices with Ricci or stress-energy, construct horizons, or close the Einstein equation.
The quadratic contraction quadContr from ClausiusEinsteinBridge is $A_{\mu\nu}k^\mu k^\nu=\sum_{i,j}A_{ij}k_i k_j$. Nullness uses the standard $(-,+,+,+)$ Minkowski metric. The present definition packages that same scalar map under the fixed-stress name used in HorizonIndexedRecordFlux, kept local so this file imports only the bridge module.
Honesty tags mark Tier A OPEN until a symmetric geometric $G$ is built from Recognition area/focusing ancestry independently of fixed stress. Forbidden shortcuts include $G:=T$ and renaming finite responses into Ricci.
proof idea
Definitional one-liner: the body is exactly the quadratic contraction of $T$ with $k$. No tactics, no lemmas. Downstream proofs typically simpa [fixedStressFlux] to reduce goals about this name back to theorems stated for quadContr.
why it matters
Supplies the scalar-map shape that lets every fixed symmetric stress instantiate an algebraic null-quadratic class. Downstream, fixedSymmetricStress_determinesAlgebraicNullQuadraticClass states that any symmetric $T$ determines its class modulo $\eta$ via this map, specializing immediately to the HorizonIndexedRecordFlux witness once Symmetric4 is known. Uniqueness of that class is fixedSymmetricStress_null_class_unique. The same name appears in the Phase-5 certificate structure, which records only rigidity and future-to-all extension.
The module doc is explicit: this statement supplies no independently geometric $G$. Tier A, continuum Ricci, C-gap1, and EFE remain open. Framework-wise this is pure algebraic scaffolding under the gravity domain, not a forcing-chain step (T0–T8) and not a claim about RS-native $G=\phi^5/\pi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.