starEdgeOriginsStatus_flags
plain-language theorem explainer
The star-edge-origins status record is locked to tables landed, gap-action recovery off, and base-0 half-repair forbidden. Gravity analysts tracking the 4D Regge–Bloch fold-repair blocker cite it as the machine-checked flag triple. The proof is a single decidable evaluation of the concrete status structure.
Claim. The star-edge-origins status satisfies $\mathrm{tablesLanded}=\mathrm{true}$, $\mathrm{gapActionRecovery}=\mathrm{false}$, and $\mathrm{base0Forbidden}=\mathrm{true}$.
background
This module treats position-resolved star edge origins in the 4D Regge–Bloch fold-repair setting. Seed star edges carry lattice origins; covering permutations transport both class index and origin into the deficit phase for non-$t_{11}$ orbits. The typed blocker is fold_position_resolved_star_phase.
The status record packages three boolean gates from the Python gate script: whether origin tables have landed, whether gap-action recovery is claimed, and whether a base-0 half-repair is allowed. Module policy is explicit: the work does not flip gap-action recovery, and base-0 half-repair is forbidden.
Upstream, starEdgeOriginsStatus is the concrete structure with those three fields fixed to true, false, and true respectively. This theorem only asserts that those field values are as written.
proof idea
One-line decidable proof: decide evaluates the three boolean equalities on the concrete starEdgeOriginsStatus structure (tables landed true, gap-action recovery false, base-0 forbidden true). No lemmas beyond the definition of the status record are required.
why it matters
In the Recognition Science gravity stack this freezes the fold-repair status for position-resolved star edge origins: tables are in, gap-action recovery is not claimed, and base-0 half-repair stays forbidden. That matches the module contract and the banked Python gate (gauges to 0; TT plus=cross=$-1/4$ on the symbol direction; $t_{11}$ untouched).
No downstream Lean consumers are wired yet (used_by empty), so the theorem is a status seal rather than a lemma in a longer chain. It still documents the closed flag triple for anyone auditing the Regge–Bloch 4D fold path against the typed blocker and the non-claim on gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.