physicalReggeEHD2MasterWitnessOneStatementProjectionCount_eq_three
plain-language theorem explainer
The one-statement projection count on the physical Regge–Einstein–Hilbert D2 master witness equals three by definitional equality. Gravity auditors tracking residual bookkeeping on Track 1.B-PHY cite it when they need the fixed projection cardinality. The proof is pure reflexivity: the count unfolds to the numeral 3.
Claim. The one-statement projection count attached to the physical Regge–Einstein–Hilbert $D_2$ master witness equals $3$.
background
Track 1.B-PHY packages physical finite-probe Regge-to-Einstein–Hilbert residual theorems beyond the flat-substrate witness of Track 1.B-C. The module records normalized full nonlinear Regge finite aggregates converging to the canonical finite EH/Dirichlet action once edge-stencil local correspondence holds, with an explicit residual tending to zero.
The surrounding path uses six-tet cubic Dirichlet data and product-filter refinement packages (CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData) that supply a uniform product residual for one global limit. The D2 master witness is the bookkeeping object that packages the one-statement projection layer for that residual upgrade; its projection count is a fixed natural number used as a structural constant in the residual ledger.
Upstream scaffolding includes polarized birth interface counts and hinge-aware zero-mode geometry on the periodic tet mesh, but this declaration only freezes the projection cardinality itself.
proof idea
Term-mode reflexivity. The left-hand side is a definitionally reduced natural-number constant; rfl closes the equality once that constant unfolds to the numeral 3. No lemmas are applied.
why it matters
Inside the Recognition gravity track, residual and witness objects must expose fixed, auditable cardinalities so later residual-to-zero and finite-to-continuum bridges do not hide dimension or projection bookkeeping. Freezing the one-statement projection count at three pins that ledger entry for the physical Regge–EH D2 master witness on Track 1.B-PHY.
No downstream consumers are recorded yet (used_by is empty). The module still leaves open the unconditional manifold Einstein–Hilbert target: the concrete periodic Freudenthal refinement family must still discharge the remaining manifold-integral weight target. This count equality is pure structural hygiene on the way to that closure; it does not itself touch T0–T8, the RCL, or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.