action_level_still_open
plain-language theorem explainer
The kinematical status record still marks action-level Wick continuation as open. Anyone citing the B3 hinge-data completeness package must also cite this flag: cosine and area-squared continuation of single-simplex hinges is closed, but the continued Regge action (deficits summed over multi-simplex interior hinges) is not. The proof is a one-line `rfl` against the hand-set status field.
Claim. In the causal 4-simplex status record, the boolean flag recording that action-level Wick continuation remains open equals $\mathrm{true}$. Equivalently: hinge-data certificates do not discharge the open question of continuing the Regge action itself.
background
Lane B3 of the QG Seven-Gaps campaign packages hinge-DATA Wick continuation over both causal 4-simplex types (4+1 and 3+2) and all twenty triangular hinges. What is certified is continuation of dihedral cosines and areas-squared of the hinges of a single causal 4-simplex of each type, along the canonical upper-half-plane arc at the physical point $a=1$, $\alpha=1$.
Action-level continuation is a strictly stronger claim: deficit angles summed over every simplex sharing an interior hinge, hence the continued Regge action. That requires a genuine three-or-more-pent interior-hinge complex (the C12 lane prerequisite) and is untouched here.
The status record causalSimplex4DStatus is the module's deliverable ledger. Its field action_level_continuation_open is set to true by construction; the three packaged B3 theorems (cosine continuation, area-squared closed forms, product-form kill certificates) deliberately leave that field unchanged.
proof idea
One-line definitional proof: rfl unfolds the status record and matches the hand-set field action_level_continuation_open := true. No lemmas are applied. The three sibling completeness theorems are listed only as axiom-audit neighbors; they are not used in the term.
why it matters
This is the mandated honesty gate for the B3 deliverable. The module doc requires that no FullTheoryLedger flag change and that action_level_continuation_open stay true. Without this documentation theorem, a reader could misread hinge-data completeness as action-level completeness.
Downstream, nothing yet consumes the flag (used-by is empty); its role is referee-facing disclosure inside the Seven-Gaps finishing charter. It keeps the open C12 question visible: multi-simplex interior-hinge complexes and the continued Regge action remain outside the present scope. In the broader Recognition gravity program this separates kinematical Wick data on single simplices from dynamical action continuation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.