BridgeStatus
plain-language theorem explainer
A five-flag status record for Gap 2: which claims about labeled versus quotient path sums this module has closed. Four flags mark proved equalities (general labeled-to-class bridge, Gibbs weight matching the quotient sum, vanishing fiber excess, and that PathSumMeasure.Z is μ at the labeled level). The fifth records that downstream physics intent is still open. Cited by the module's bridgeStatus instance as an honest audit tag, not a mathematical theorem.
Claim. A record of five Boolean status bits: (1) the general labeled-to-class bridge holds for every real weight; (2) the Gibbs weight makes the labeled path sum equal the quotient-first sum; (3) the fiber excess vanishes for that Gibbs weight; (4) the path-sum partition function $Z$ is the labeled sum at weight $\mu$, a distinct object; (5) whether downstream physics has settled which object it intends (left open).
background
Gap 2 concerns a mismatch between two path-sum constructions in the gravity ledger. The labeled sum PathSumMeasure.Z B w runs over labeled complexes but historically weighted each by the class quantity $\mu K = 1/|\mathrm{Aut}, K|$. A class with $n$ labeled presentations then contributes $n\cdot\mu$, so the labeled sum equals the quotient sum only up to a mandatory fiber factor. That residue was booked as fiberExcess.
Gap2GaugeVolume supplies the missing weight: the unique relabeling-invariant labeled weight whose class mass is $\mu$ (the Gibbs weight). Substituting it removes the fiber factor identically, with no hypothesis on the complex weight and no cancellation assumed. The fiber excess was therefore a diagnostic that $\mu$ had been used at the labeled level, where it does not belong.
This structure is the module's honest status board for those closures, not a computational object.
proof idea
No proof: this is a structure definition with five Boolean fields and field doc-comments. The companion definition bridgeStatus instantiates it by setting the four proved flags to true and downstream_intent_settled to false. The mathematical content lives in the sibling theorems (labeledSum_eq_classMass_sum, classMass_gibbs_eq_mu, gibbsZ_eq_Zq, gibbs_fiberExcess_vanishes, and the contrast muZ_eq_Zq_iff_fibers_trivial).
why it matters
In the Seven Gaps gravity program this is the audit tag for Gap 2 after the labeled-weight bridge is closed. Downstream, bridgeStatus is the sole consumer: it freezes the module's self-assessment so later panels can read which equalities are proved and which intent question remains open.
The four true flags certify that the general bridge, the Gibbs-to-quotient identity, excess vanishing, and the identification of $Z$ as $\mu$ at labeled level are settled with zero sorry on the base triple. The false flag keeps the physics choice honest: the module does not decide whether downstream continuum or Regge-side constructions should use the labeled Gibbs sum or the quotient-first sum. That separation prevents silently reintroducing $\mu$ at the labeled level, the error that created the original tension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.