status_count_finite
plain-language theorem explainer
Records that count-finiteness for the scoped path-sum configuration class is proved in this module: the status flag is definitionally true. Anyone tracking the Seven Gaps ledger for Z_RS cites it as the machine-checkable discharge of the growthBase finiteness obligation. The proof is pure reflexivity against the status record.
Claim. The path-sum measure status record sets the count-finiteness flag to true: configurations in the bounded incidence class are finite in number, so the corresponding gap field is marked proved.
background
Lane 2 of the Seven Gaps program builds an honest path-sum measure $Z_{\mathrm{RS}}$ for Recognition Science gravity. Configurations live in the scoped class BoundedComplex B: fixed bounds on vertices, edges, and tetrahedra, with incidence maps in the shape of a 3D Regge triangulation (metric dropped). The recognition substrate fixes edge length at the minimum mesh, so the sum is combinatorial and CDT-style.
Finiteness of that class is established earlier in the module by an explicit coding equivalence to a finite type, yielding a Fintype instance. That fact discharges the count-finiteness content formerly postulated in the growthBase field of PathSumUVBound.AdmissibleTriangulationFamily. The status record pathSumMeasureStatus packages five boolean flags summarizing what this module closes; the first flag is count-finiteness.
proof idea
One-line reflexivity. The definition of pathSumMeasureStatus hard-codes count_finite_proved := true, so equating that projection to true is rfl. No lemmas are applied; the theorem is a ledger witness, not a new mathematical argument.
why it matters
Closes the count-finiteness line item on the path-sum-measure gap for $Z_{\mathrm{RS}}$. The module doc states that finiteness of the bounded incidence superclass gives finiteness of every subclass and thereby replaces a postulated cardinal bound by a proved finite cardinal. Downstream consumers of the status record can branch on this flag without re-auditing the Fintype construction. Sharper exponential-growth semantics for exact simplicial classes remain open; this flag only certifies raw finiteness of the scoped superclass. No used-by edges are recorded yet; the declaration is a status pin rather than a lemma in a forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.