pathSumProbesStatus_flags
plain-language theorem explainer
Records the seven boolean outcomes of the path-sum probes C3 and C6 as a single conjunction: the periodic Freudenthal torus attaches to the path-sum state space with counts and incidence preserved; edge-in-tet slots, per-tet metrics, and simpliciality of the image are not preserved or proved; translations embed; unnormalized μ-torus claims are inadmissible. Anyone auditing Seven Gaps Phase 2b lane O cites this as the frozen status snapshot. Proof is pure reflexivity against the status record.
Claim. The path-sum probe status record satisfies: torus attached to the state space is true; vertex/edge/tet counts and incidence maps are preserved is true; edge-in-tetrahedron slot data preserved is false; per-tetrahedron metric preserved is false; simpliciality of the image proved is false; translations embed is true; and unnormalized $\mu(T_N)\cdot e^{iS}$ claims are admissible is false.
background
Module PathSumProbes is a non-flag-bearing provenance lane inside Gravity Seven Gaps Phase 2b. It connects the canonical periodic Freudenthal torus (Geometry.PeriodicFreudenthalTorus) to the scoped path-sum state space BoundedComplex from PathSumMeasure, without claiming measures, limits, or continuum values.
Probe C3 packages the torus at side $N\ge 1$ as freudenthalBoundedComplex N : BoundedComplex (7 N^3). Counts $nV=N^3$, $nE=7N^3$, $nT=6N^3$ and the incidence maps edgeVerts, tetVerts match the canonical triangulation definitionally. BoundedComplex drops edgeInTet slots and per-tet metric data; simpliciality of the image is not proved.
Probe C6 checks the Aut-vacuity landmine: the translation group $\mathbb{Z}_N^3$ embeds into Aut of the torus image (translationAut_injective), so $|\mathrm{Aut}(T_N)|\ge N^3$ and $\mu(T_N)\le 1/N^3$. The status def freezes these outcomes as booleans.
proof idea
One-line term proof: the seven-field conjunction is witnessed by seven rfls. Each conjunct is definitionally equal to the corresponding field of the structure value pathSumProbesStatus, which hard-codes those booleans. No lemmas are applied; the proof is pure definitional unfolding of the status record.
why it matters
Freezes the honest C3/C6 probe ledger so later Seven Gaps work cannot silently upgrade dropped data or claim unnormalized path-sum weights. Module doc states the lane is PROBES ONLY: attachment and Aut-embedding are recorded; edge-slot, metric, and simpliciality gaps stay false; unnormalized $\mu(T_N)\cdot e^{iS}$ claims stay inadmissible because of the $1/|\mathrm{Aut}|$ suppression from the translation embedding.
No downstream consumers yet (used_by empty). The declaration is the machine-checkable seal on the provenance record, not a physics derivation. It sits upstream of any future normalized path-sum or continuum limit argument that must confront the dropped incidence shape and the Aut lower bound. Framework landmarks (T0–T8, RCL, mass ladder) are not touched here; this is pure gravity-side scaffolding hygiene.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.