pathSumProbesStatus
plain-language theorem explainer
Records the Boolean outcome vector for path-sum probes C3 and C6 on the periodic Freudenthal torus. C3 attaches the torus to the bounded-complex state space with counts and incidence preserved; edge-in-tet slots, per-tet metric, and image simpliciality are not claimed. C6 holds on branch (a): translations embed, so unnormalized μ(T_N)·exp(iS) claims are inadmissible. Downstream flag theorems and cardinality lemmas cite this provenance record.
Claim. The probe-status record for the path-sum lane sets: torus attached to the state space = true; vertex/edge/tet counts and incidence maps preserved = true; edge-in-tetrahedron slots preserved = false; per-tetrahedron metric preserved = false; simpliciality of the image proved = false; translation group embeds into automorphisms = true; unnormalized $\mu(T_N)\cdot e^{iS}$ claims admissible = false.
background
Module lane O (Seven Gaps, Phase 2b) is probes-only: it attaches the canonical periodic Freudenthal torus at side $N$ to the scoped path-sum state space BoundedComplex and records two cheap honest facts. It makes no claim about measures, continuum limits, or the value of any path sum.
Probe C3 packages the torus as freudenthalBoundedComplex N inside BoundedComplex (7 N^3). Preserved definitionally: $nV = N^3$, $nE = 7 N^3$, $nT = 6 N^3$, plus edge-endpoint and tet-corner incidence. Dropped by shape mismatch: edge-slot-in-tet assignment and per-tet squared-edge metric; simpliciality of the image is not proved.
Probe C6 checks the Aut-vacuity landmine. Outcome branch (a): the translation group $\mathbb{Z}_N^3$ embeds into relabeling automorphisms of the image, so $|\mathrm{Aut}(T_N)| \ge N^3$ and $\mu(T_N) \le 1/N^3$. The structure ProbeStatus is the Boolean outcome record for these two probes; every flag is forced by rfl at the definition site.
proof idea
Definitional structure instance, not a proof. Each field of ProbeStatus is assigned a literal Boolean matching the module's documented C3/C6 outcomes: attachment and count/incidence preservation true; edge-slot, metric, and simpliciality false; translations embed true; unnormalized $\mu$-claims admissible false. No lemmas are applied; the values are the provenance record itself.
why it matters
This is the single provenance vector for lane O. Downstream, pathSumProbesStatus_flags re-exports the seven equalities as a conjunction, so later gravity or path-sum developments can pattern-match on honest non-claims (edge slots dropped, metric dropped, simpliciality open, unnormalized $\mu(T_N) e^{iS}$ blocked). The Aut-embedding flag underwrites the proved bounds $|\mathrm{Aut}| \ge N^3$ and $\mu \le N^{-3}$, which close the C6 landmine on branch (a): any continuum or measure claim that ignores the $1/|\mathrm{Aut}|$ suppression is inadmissible.
In the broader Seven Gaps gravity program this keeps the Freudenthal-torus attachment honest relative to the path-sum state space without smuggling continuum or measure content. It does not touch T0–T8 forcing, RCL, or the $\phi$-ladder mass formula; it is scaffolding hygiene for discrete gravity path sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.