Pith. sign in
theorem

recognitionMeshHingeKappa4DStatus_flags

proved
show as:
module
IndisputableMonolith.Gravity.Analysis.RecognitionMeshHingeKappa4D
domain
Gravity
line
226 · github
papers citing
none yet

plain-language theorem explainer

Status snapshot for the 4D recognition-mesh hinge-kappa residual (Wave B R2). It records that the source-dominated unit-coupling bound is closed, the continuum Einstein-scale join stays open, and the Gap-1 bridge is not derived. Residual-DAG auditors cite it to freeze honest completion flags. Proof is a one-line decidability check on the status record literals.

Claim. The 4D recognition-mesh hinge-kappa status record satisfies: R2 residual closed equals true, Einstein-scale join open equals true, and Gap-1 bridge derived equals false.

background

Wave B of the QG residual program attacks the hinge-kappa identification residual. After R1 reshaped the carrier to real star deficit (no separate hinge carrier type), this module packages hinge coupling as the constant unit map, matching the banked stationarity-bridge pattern that every hinge has coupling one. Geometric content is the star deficit; admissibility is the source-dominated bound with four bridge channels and mesh scale $\pi/2$, using $|\arcsin|\le\pi/2$ so the deficit is at most $2\pi$ in absolute value.

The status structure is a three-bit ledger of what this module claims to have finished. Upstream, the status definition hard-codes the three booleans; the theorem only freezes them as proved equalities. Mesh context still requires the exact-$J$/true-Regge-Hessian bridge and flat angle sum $2\pi$, same as R1. Continuum matching of hinge-local unit coupling to an Einstein-scale kappa is deliberately left open.

proof idea

One-line decidability proof. The status definition sets the three boolean fields by structure literal; decide discharges the conjunction of field equalities against true/false. No lemmas beyond the definition itself.

why it matters

Freezes honest completion flags for Wave B residual R2 on hinge kappa with source-dominated admissibility. Module doc is explicit: kappa naming is the banked unit-coupling identification; theorem content is the source-dominated inequality against banked star geometry, plus nontriviality and decoys. Continuum Einstein-scale join remains open by design, and Gap-1 bridge derivation is not flipped. No downstream consumers yet; the flag theorem is the audit seal for the residual DAG draft entry on typed residual hinge-kappa identification. It sits in the gravity analysis stack beside geometric-deficit and exact-$J$ bridge modules, not in the T0–T8 forcing chain.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.