bridgeStatus
plain-language theorem explainer
Module-level status ledger for the Gap 2 labeled-weight bridge: four settled flags (general labeled-to-class bridge, Gibbs equals quotient sum, fiber excess vanishes, and the old Z is μ used at labeled level) plus one deliberately open flag (downstream physics intent). Anyone auditing SevenGaps closure cites it for honest tagging. It is a pure structure instance with literal booleans, not a derived proof.
Claim. After this module, the bridge status is: the general labeled-to-class bridge holds for every real weight; the Gibbs weight makes the labeled path sum equal the quotient-first sum; the fiber excess vanishes for that weight; the original path-sum $Z$ is the labeled sum at weight $\mu$ (a different object); and which object downstream physics intends remains unsettled.
background
Gap 2 concerns two path-sum constructions. The labeled sum weights each complex $K$ by a class quantity $\mu K = 1/|\mathrm{Aut}, K|$, so a class of $n$ labeled presentations contributes a fiber factor $n\cdot\mu$. The quotient-first sum works on classes directly. Their mismatch was booked as fiber excess when $\mu$ was used at the labeled level.
Gap2GaugeVolume supplies the unique relabeling-invariant labeled weight (Gibbs) whose class mass is $\mu$. This module proves that substituting it removes the fiber factor identically: the labeled Gibbs sum equals the quotient sum with no hypothesis on the class weight.
BridgeStatus is the five-flag structure that records what the module settles about those two path-sum objects, including an explicit open bit for downstream intent.
proof idea
Definitional instance, not a tactic proof. Each field of the status structure is set to a literal boolean: four true flags for the proved bridge facts and false for downstream intent. Downstream status_* theorems are one-line rfl reads of those fields; the mathematical content lives in the sibling theorems (labeledSum_eq_classMass_sum, gibbsZ_eq_Zq, gibbs_fiberExcess_vanishes, etc.), not here.
why it matters
Closes the honest-tagging layer of Gap 2. Parent consumers are the five status_* theorems (status_bridge, status_gibbs_matches, status_excess, status_Z_is_mu, status_intent_open), each a reflexivity check that the ledger matches the proved (or deliberately open) claims.
In the SevenGaps gravity stack this separates a resolved technical tension (fiber excess was a mis-level use of $\mu$, not a defect of the quotient) from an open modeling choice: which path-sum object downstream physics should read. The module doc states that intent is not settled here because the module does not inspect downstream users of $Z$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.