IndisputableMonolith.Gravity.SevenGaps.Gap2LabeledWeightBridge
Bridge between the labeled path sum (real weights on labeled triangulations) and the quotient-first class sum with class-constant complex weights. Relates the full labeled partition function to the gauge-volume-weighted class sum via orbit masses and Aut factors. Gravity and path-sum auditors cite it when matching labeled and quotient formulations of Gap 2. The argument is algebraic identities on sums over orbits plus status flags for when the two Z objects coincide.
claimDefine the labeled path sum $Z_{\mathrm{lab}}$ with explicit real labeled weights, and compare it to the quotient-first sum $Z_q=\sum_q |\mathrm{Aut}(q)|^{-1} w_q(q)$ with class-constant complex weights. Establish equalities relating labeled sums to class-mass sums, Gibbs factors to $\mu=1/|\mathrm{Aut}|$, and conditions under which $Z=Z_{\mathrm{lab}}\cdot\mu$ or the two formulations differ on nontrivial orbits.
background
Gap 2 in the Seven Gaps gravity stack concerns how gauge volume enters the path sum. Upstream, Gap2GaugeVolume takes a pair-counting principle: class mass equals labeled copies per unit of gauge volume, and derives $\mu K=1/|\mathrm{Aut} K|$ from that model premise. The gauge volume counts pairs $(K',r)$ of an orbit member and a relabeling witness.
QuotientFirstZ builds the P2c-locked quotient-first object
$Z_q B w_q=\sum_{q:\mathrm{TriangulationClass},B}(1/|\mathrm{Aut}(\mathrm{out},q)|)\cdot w_q(q)$.
That is the class-side partition function with Aut-normalized weights.
This module sits between those two: it introduces an explicit labeled weight path sum and a bridge status that records when labeled and class-constant formulations agree, when fiber excess vanishes, and when nontrivial orbits force the Gibbs and $\mu$ pictures apart.
proof idea
Definition-plus-identity module, not a single theorem. It introduces the labeled sum object and a small suite of comparison lemmas: labeled sum equals class-mass sum after grouping; class-mass Gibbs weight equals $\mu$; Gibbs $Z$ equals $Z_q$ under the quotient-first weighting; fiber excess vanishes in the Gibbs picture; $Z$ factors as labeled $Z$ times $\mu$ when orbits are controlled; class mass times $\mu$ recovers orbit multiplicity times $\mu$; and $\mu Z=Z_q$ when all orbits are trivial. A status inductive or enum packages the bridge outcome (match vs nontrivial-orbit mismatch). Proofs are sum rewrites and orbit-stabilizer bookkeeping over the Aut action.
why it matters in Recognition Science
Closes the Gap 2 comparison between the physicist's labeled path sum and the quotient-first object required by the P2c panel lock. Without this bridge, $\mu=1/|\mathrm{Aut}|$ from gauge volume and $Z_q$ from QuotientFirstZ remain formally disconnected from an explicit real labeled weight. Downstream gravity path-sum arguments that need a single $Z$ can read the bridge status and the equalities $Z=Z_{\mathrm{lab}}\mu$ or $\mathrm{gibbs}Z=Z_q$ rather than re-deriving orbit sums. No further used-by edges are recorded yet; the module is infrastructure for later Gap 2 closure rather than a leaf theorem. It does not itself force $D=3$ or the eight-tick structure; those live elsewhere in the forcing chain.
scope and limits
- Does not prove the pair-counting principle; that remains a model premise in Gap2GaugeVolume.
- Does not construct $Z_q$ itself; it imports QuotientFirstZ and compares against it.
- Does not claim labeled and quotient $Z$ always coincide on nontrivial Aut orbits.
- Does not derive gravitational dynamics or mass ladders; only path-sum weight bookkeeping.
- Does not discharge Gap 2 fully; it only supplies the labeled-versus-class bridge layer.
depends on (2)
declarations in this module (18)
-
class
of -
def
Zlabeled -
theorem
labeledSum_eq_classMass_sum -
theorem
classMass_gibbs_eq_mu -
theorem
gibbsZ_eq_Zq -
theorem
gibbs_fiberExcess_vanishes -
theorem
Z_eq_Zlabeled_mu -
theorem
classMass_mu_eq_orbit_mul_mu -
theorem
muZ_eq_Zq_of_trivial_orbits -
theorem
gibbs_ne_mu_of_nontrivial_orbit -
structure
BridgeStatus -
def
bridgeStatus -
theorem
status_bridge -
theorem
status_gibbs_matches -
theorem
status_excess -
theorem
status_Z_is_mu -
theorem
status_intent_open -
theorem
bridge_grounded