status_intent_open
plain-language theorem explainer
Records that the Gap-2 labeled-weight bridge leaves downstream intent about the partition function Z unsettled. Auditors of SevenGaps status tiers cite it as the explicit open flag. The proof is reflexivity against the status record, which hard-codes that field to false because this module never inspects downstream users of Z.
Claim. In the Gap-2 labeled-weight bridge status record, the flag that downstream intent about $Z$ is settled equals $\mathrm{false}$.
background
Gap 2 asks which labeled weight makes the labeled path sum equal the quotient-first sum. The labeled measure sums over labeled complexes with class weights $\mu K = 1/|\mathrm{Aut}, K|$, so a class of $n$ presentations contributes a fiber factor $n\cdot\mu$. That excess was booked as fiberExcess until the Gibbs weight from Gap2GaugeVolume was shown to be the unique relabeling-invariant labeled weight whose class mass is $\mu$, removing the factor identically (gibbsZ_eq_Zq).
The module tags its own closure with a small status record: general bridge proved, Gibbs matches quotient, excess vanishes, and the contrast that $\mu$ at labeled level only works for trivial fibers. One remaining bit is whether downstream consumers of $Z$ have had their intent settled by this choice of weight. The module header states it does not read those users, so that bit stays open by construction.
proof idea
One-line term proof by rfl. The status definition sets downstream_intent_settled := false; equality to false is definitional.
why it matters
Honest status tier for the Gap-2 bridge: the proved core (general labeled-to-class bridge, Gibbs class mass equals $\mu$, labeled Gibbs $Z$ equals quotient $Z$, fiber excess vanishes) is marked true, while downstream intent about which $Z$ consumers should adopt remains explicitly false. No parent theorems currently depend on this flag (used_by is empty); it is a grounding assertion so panels and auditors cannot misread the module as having closed the full $Z$ story. In the SevenGaps gravity stack this keeps the labeled-versus-quotient resolution local and prevents silent overclaim about posting-layer or hinge-aware consumers of the partition function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.