srsConvergesEH4DStatus_flags
plain-language theorem explainer
Status certificate that all five ledger flags for 4D weak-field SRS-to-Einstein-Hilbert recovery are true: edge time-time decomposition named and inhabited, SRS-converges-EH named and inhabited, and gap-action recovery on. Gravity auditors cite it as the boolean export that the named closers are live on the ledger. Proof is a one-line decidability check on the status record literals.
Claim. The 4D SRS-converges-to-Einstein-Hilbert status record has every flag true: the edge time-time decomposition is named and inhabited, the SRS-converges-EH theorem is named and inhabited, and gap-action recovery is enabled.
background
This module is the ledger-facing export for the QG full-theory campaign on weak-field quadratic action recovery. The two named closers are the edge time-time decomposition and the statement that the discrete recognition-mesh action converges to the Einstein-Hilbert quadratic form in 4D. The Props are preflight names; this file is the sole place that may inhabit them for the ledger flip.
Honest scope is narrow: weak-field quadratic action convergence only, not sourced Einstein equations, continuum Ricci or stress, horizons, coframes, arbitrary-curvature GR, or full nonlinear Wick continuation. Gap-action recovery flips only when both named theorems are inhabited under focused axiom audits.
The upstream status definition hard-codes all five booleans to true: edge-TT named, SRS named, edge-TT inhabited, SRS inhabited, and gap-action recovery. This theorem merely reifies those field equalities as a single conjunction.
proof idea
One-line wrapper: decide discharges the five boolean equalities because each field of the status record is the literal true. No lemmas are applied; the proof is pure decidable equality on the structure values.
why it matters
In the Recognition gravity stack this is the ledger flip signal for 4D weak-field quadratic recovery. Module doc states that gap-action recovery flips with this inhabitant (MEASURED-native decide via m² table certificates), and never via a j-independent constant face. Banked upstream work includes the closed edge-TT decomposition, R2 symbol-zero, R3 Rayleigh faces, R4 discrete torus-family bridge to ContinuumSymbolIs at m² Rayleigh, Option-C m² faces, and the honest SRS-converges-EH statement. No downstream consumers are wired yet; the theorem exists so external ledger tooling can read a single proved conjunction rather than inspect the status record by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.