lorentzianSectorStatus_flags
plain-language theorem explainer
The Lorentzian-sector status record reports four fixed flags: causal tetrahedron classes defined, Wick rotation certified on that class, Euclidean nondegeneracy proved, and Lorentzian action continuation still open. Auditors of the QG Seven-Gaps Lorentzian lane cite this as the module-level checklist. The proof is four reflexivity steps against the structure definition.
Claim. The Lorentzian-sector status flags equal $(\mathrm{true},\mathrm{true},\mathrm{true},\mathrm{true})$ in the order: causal class defined; Wick certified on that class; Euclidean nondegeneracy proved; Lorentzian action continuation open.
background
This module opens the Lorentzian lane of the QG Seven-Gaps campaign. Prior discrete-gravity work in the monolith is Euclidean. Here one builds CDT-style tetrahedron classes in $D=3$: type $(3,1)$ (three vertices on slice $t$, one on $t+1$) and type $(2,2)$ (two on each slice), with spacelike squared lengths $a^2$ and timelike squared lengths $-\alpha a^2$ for $\alpha>0$.
The Wick map flips the sign of timelike squared lengths and is the algebraic continuation $\alpha\mapsto -\alpha$ on the causal class. The module also proves Euclideanized nondegeneracy on a hand-derived parameter range and a deficit-angle reality corollary at $\alpha=1$.
Upstream, lorentzianSectorStatus is the concrete status record whose four Boolean fields are set by hand to encode which of those deliverables are closed versus left open.
proof idea
Pure term proof: the goal is a four-way conjunction of equalities of Booleans to true. Each conjunct is discharged by rfl against the corresponding field of the status structure definition, packaged as a single anonymous constructor ⟨rfl, rfl, rfl, rfl⟩. No lemmas are invoked.
why it matters
This is the module-level scoreboard for the first certified Lorentzian layer in the Seven-Gaps gravity program. It records that causal class combinatorics, Wick involution on that class, and Euclidean nondegeneracy are treated as closed inside the file, while Lorentzian action continuation remains explicitly open.
No downstream theorems currently depend on it (used_by is empty); its role is audit and campaign tracking rather than a computational lemma. In framework terms it sits under the $D=3$ discrete-gravity lane (T8 forces three spatial dimensions) and marks how far the Euclidean-to-Lorentzian bridge has been formalized. The open flag is the natural next target: continue the Regge-type action through the Wick map to a genuine Lorentzian sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.