of
plain-language theorem explainer
Gap 2 asks which labeled weight makes the labeled path sum match the quotient-first sum. Using the class factor μ=1/|Aut| on labeled complexes overcounts by the fiber size; the unique relabeling-invariant Gibbs weight with class mass μ cancels that factor identically. Gravity and path-sum authors cite the bridge. The extracted declaration is a sorry stub with no proof body.
Claim. In the Gap-2 labeled-weight bridge, the labeled path sum $Z_{\mathrm{labeled}}(B,v,w_q)=\sum_K v(K)\,w_q([K])$ against a class-constant complex weight equals the class sum of the weight's class mass. Instantiating $v$ by the unique relabeling-invariant Gibbs weight with class mass $\mu=1/|\mathrm{Aut}|$ yields $Z_{\mathrm{labeled}}(B,v_{\mathrm{Gibbs}},w_q)=Z_q(B,w_q)$ with no hypothesis on $w_q$, so the fiber excess vanishes for that weight.
background
Path-sum gravity here has two summation orders. The labeled sum $Z$ runs over labeled bounded complexes and multiplies each by $\mu(K)=1/|\mathrm{Aut},K|$, a quantity constant on relabeling classes. A class with $n$ labeled presentations therefore contributes $n\cdot\mu$. Quotient-first $Z_q$ sums once per class. The identity relating them inserts a mandatory fiber-cardinality factor; the residual mismatch was recorded as fiber excess after an unconditional equality claim failed.
Gap2GaugeVolume supplies gibbsWeight: by the invariant-weight characterization, it is the unique relabeling-invariant real labeled weight whose class mass equals $\mu$. The bridge module's job is to show that substituting this weight removes the fiber factor with no cancellation hypothesis on the class weight $w_q$.
Sibling content defines $Z_{\mathrm{labeled}}$ as $\sum_K v(K),w_q([K])$ and states the general fact that any real labeled weight, paired with a class-constant complex weight, reduces to a class sum against that weight's class mass (class mass already folds the fiber).
proof idea
Claim status is scaffolding with proof style sorry_stub and an empty proof body. No tactics or upstream lemmas are discharged at this declaration. The intended route, read from the module plan, is: prove the general bridge (labeled sum equals class sum of class mass for any real labeled weight), instantiate class mass of gibbsWeight to $\mu$ on representatives, conclude gibbs-weighted labeled $Z$ equals $Z_q$, and rephrase vanishing fiber excess in the form QuotientFirstZ left open. Contrast: bare $\mu$ at labeled level matches $Z_q$ only if every fiber is trivial.
why it matters
SevenGaps Gap 2 is a bookkeeping tension inside Recognition gravity path sums, not a new force law. Closing it decides whether fiber excess is a defect of the quotient construction or a symptom of placing the class factor $\mu$ at the labeled level. The module argues the latter: gibbsWeight is the weight that belongs on labeled complexes if one wants the per-class $1/|\mathrm{Aut}|$ convention.
Downstream usage is empty in the graph right now. The module text is explicit that this does not rewrite existing bounds about bare $Z$; those still concern $Z$. It also refuses to legislate which object downstream physics meant. Landmarks touched are only organizational (gap ledger hygiene). No T5–T8 forcing step, RCL identity, or $\phi$-ladder mass formula is proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.