physicalReggeEHD2MasterWitnessProjectionCount
plain-language theorem explainer
Audit constant equal to 7 that records how many physical D2 master-witness projection theorems sit in the Track 1.B-PHY package: four witness-field projections and three certificate projections. Gravity auditors and residual-upgrade reviewers cite it as the Session 549 headcount. The body is a one-line natural-number assignment.
Claim. The audit count of physical $D_2$ master-witness projection theorems equals $7$, namely four witness-field projections together with three certificate projections.
background
Track 1.B-PHY packages physical finite-probe Regge-to-Einstein-Hilbert residual theorems drawn from the six-tetrahedron cubic Dirichlet instance. It upgrades the flat-substrate structural witness: once edge-stencil local correspondence holds, normalized full nonlinear Regge finite aggregates converge to the canonical finite EH/Dirichlet action with an explicit residual tending to zero, and the same correspondence feeds a finite-to-continuum bridge under a Riemann-sum identification.
The remaining gap for an unconditional manifold EH theorem is the canonical periodic finite EH/Dirichlet limit-weight integral target on a concrete periodic Freudenthal refinement family. Inside that residual-upgrade layer, D2 master-witness projections split into witness-field projections and certificate projections; this definition simply freezes their total count for audit.
proof idea
Pure definitional assignment: the natural number is set to 7. No lemmas, tactics, or algebraic reduction are involved.
why it matters
Gives Session 549 a fixed headcount for the seven physical D2 master-witness projection theorems (four witness-field plus three certificate) inside the Track 1.B-PHY residual upgrade. Reviewers use it to confirm the projection inventory that sits above the flat structural witness and below the still-open manifold-integral remaining target. It does not itself advance the Regge-to-EH convergence or the continuum bridge; it only locks the audit tally those projection theorems are expected to match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.