ZeroMomTrueWeightMatchOpen
plain-language theorem explainer
Records the open claim that the transported all-orbit Bloch fold at zero momentum equals the committed true-weight zero-momentum quadratic, for every 4×4 matrix. Gravity analysts matching the multi-orbit Regge fold to the Hessian assembly would cite it. It is a bare Prop definition: no proof, only the equality statement, banked separately from the m² continuum symbol.
Claim. For every real $4\times 4$ matrix $H$, the transported multi-orbit Bloch fold of $H$ evaluated at vanishing momentum equals the true-weight zero-momentum quadratic form assembled from the orbit-wise zero-momentum quadratics of $H$.
background
This module builds a continuum-facing multi-orbit 4D Bloch fold. Each hinge-orbit slot transports its seed area covector and star deficit kernel by the orbit covering permutation (first $S_4$ cover of the orbit representative into difference masks). The full fold sums the per-orbit transported folds over all hinge-orbit types.
At zero momentum the fold is compared to a committed assembly object: the true-weight zero-momentum quadratic, defined as the sum over orbit types of the orbit-wise zero-momentum quadratic. That assembly lives in the flat 4D Hessian assembly module and is the target continuum weight at vanishing momentum.
The local status note flags this equality as open. Reindexing the pushforward class pairing yields a weighted sum of class coefficients along the permutation; that recovers the unpermuted class pairing only if class coefficients are invariant along the covering, which fails in general. The module deliberately does not use the factorized transport permutation for non-$(1,1)$ orbits.
proof idea
No proof: the declaration is a Prop definition whose body is the universal equality between the zero-momentum all-orbit fold and the true-weight zero-momentum quadratic. There are no tactics, lemmas, or wrappers. Discharge would require proving that equality for general $H$, which the doc-comment notes is blocked by missing class-coefficient invariance under the covering permutation.
why it matters
Pins an open matching step between the transported all-orbit fold and the committed true-weight Hessian quadratic at zero momentum. The module status lists continuum Einstein-Hilbert isotropy and all-orbit m² Tendsto as still open; this Prop is the zero-momentum weight half of that continuum dictionary, banked separately from the m² continuum symbol.
No downstream consumers are wired yet. Closing it would feed any later theorem that identifies the discrete fold weight with the continuum quadratic form used in EH recovery. It does not flip gap-action recovery, and it sits downstream of the covering-based transport definitions and the flat Hessian assembly rather than of the cost-functional $H$ (name collision only).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.