status_modulus_bound
plain-language theorem explainer
Records that the path-sum measure gap status has its modulus-bound flag set to true. Anyone auditing Seven Gaps lane 2 (the proved Z_RS path-sum measure) cites this as the bookkeeping witness that ‖Z‖ bounds were discharged in-module. The proof is pure reflexivity against the GapStatus record literal.
Claim. In the path-sum measure status record, the field asserting that a modulus bound on the path sum has been proved equals $\mathrm{true}$.
background
Lane 2 of the Seven Gaps program builds an honest, finite path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of bounded combinatorial complexes. Configurations live in BoundedComplex B (incidence data at fixed lattice scale, CDT-style), which is finite; the quotient by relabeling is finite; and the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ is positive, at most one, and relabeling-invariant.
The path sum is $Z B w=\sum_K \mu(K)\cdot w(K)$. Two modulus bounds are proved in-module: $|Z|\le\sum\mu$ and $|Z|\le|\mathrm{BoundedComplex},B|$. For unitary weights $w(K)=e^{iS(K)}$ one has $|w(K)|=1$, so the bounds apply and $Z_{\mathrm{RS}}$ is well-defined on the scoped class.
The upstream definition pathSumMeasureStatus packages five boolean discharge flags for this gap (count finite, quotient finite, measure defined, measure positive, modulus bound). This theorem reads the last of those flags.
proof idea
One-line reflexivity. The status record is defined with modulus_bound_proved := true, so equating that projection to true is definitional (rfl). No lemmas are applied; the theorem is pure bookkeeping against the record literal.
why it matters
Closes the status-tag side of the modulus-bound discharge for Seven Gaps lane 2. The module doc lists the analytic content already proved: $|Z|\le\sum\mu$ and $|Z|\le\mathrm{card}(\mathrm{BoundedComplex},B)$, plus the unitary instance that makes $Z_{\mathrm{RS}}$ well-defined. This flag lets downstream gap dashboards and honest-tagging machinery read that the bound tier is green without re-inspecting the analytic proofs.
No parent theorems currently depend on the flag (used-by is empty); its role is audit and status aggregation. It does not touch the still-open sharper exponential-growth semantics of growthBase for exact simplicial subclasses, nor the geometric (metric) layer dropped from the Regge-style incidence shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.