ProbeStatus
plain-language theorem explainer
Outcome record bundling seven Boolean flags for path-sum probes C3 and C6 on the periodic Freudenthal torus. Gravity and discrete-geometry workers cite it as the typed status board for what the torus attachment preserves versus drops. It is a plain structure definition; concrete values are filled by a sibling definition via definitional equality.
Claim. A record type with seven Boolean fields: whether the periodic Freudenthal torus attaches into the path-sum state space; whether vertex/edge/tet counts and incidence maps are preserved; whether edge-in-tet slots are preserved; whether per-tet metric data are preserved; whether simpliciality of the image is proved; whether the translation group embeds into automorphisms; and whether unnormalized $\mu(T_N)\cdot e^{iS}$ claims are admissible.
background
Module lane O of Seven Gaps Phase 2b runs two cheap probes only. It makes no claim about measures, continuum limits, or path-sum values. Probe C3 packages the canonical periodic Freudenthal torus at side $N\ge 1$ as a BoundedComplex of size $7N^3$, attaching it to the scoped path-sum state space. Counts $nV=N^3$, $nE=7N^3$, $nT=6N^3$ and the edge/tet incidence maps match the canonical triangulation definitionally; edge-in-tet slots, per-tet metrics, and 2-face lists are dropped by shape mismatch, and simpliciality of the image is not claimed.
Probe C6 checks the automorphism landmine. The translation group $\mathbb{Z}_N^3$ embeds injectively into relabeling automorphisms of the torus image, so $|\mathrm{Aut}(T_N)|\ge N^3$ and the normalized measure satisfies $\mu(T_N)\le 1/N^3$. Unnormalized $\mu(T_N)\cdot e^{iS}$ claims are therefore not admissible without the $1/|\mathrm{Aut}|$ factor.
proof idea
No proof body: this is a structure declaration. Seven named Boolean fields form a provenance board. Downstream, a single definition instantiates every field by true/false literals forced by rfl against the C3 attachment lemmas and the C6 translation-embedding theorems already proved in the module. There are no True shells and no axioms.
why it matters
Gives a single typed status object for the C3/C6 probe outcomes so later gravity path-sum work can read off what was attached, what was dropped, and that unnormalized torus measure claims fail the Aut-suppression check. The sole consumer is pathSumProbesStatus, which records C3 attached with counts and incidence preserved, edge-slot and metric data dropped, simpliciality unproved, translations embedding (C6 branch a), and unnormalized $\mu(T_N)\cdot e^{iS}$ claims inadmissible. In the Recognition gravity program this is bookkeeping for discrete path sums on the eight-tick / $D=3$ side, not a forcing-chain step. It closes no open physics claim; it prevents silent overclaim on measures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.