classPhase
plain-language theorem explainer
A phase model supplies a real phase on labeled bounded complexes that is invariant under relabeling; this definition descends that phase to a well-defined real function on triangulation classes. Anyone building oscillatory weights for the quotient-first path sum Zq cites it. The construction is the standard quotient lift, using the model's invariance hypothesis as the well-definedness certificate.
Claim. Given a phase model $P$ at complexity bound $B$ (a real-valued phase on labeled bounded complexes together with the property that relabeling-equivalent complexes receive the same phase), there is a well-defined map from triangulation classes to $\mathbb{R}$ obtained by descending the labeled phase along the relabeling quotient.
background
Lane D3 of the Seven Gaps gravity program equips the quotient-first path sum $Z_q$ with an explicit oscillatory phase structure at fixed complexity cap $B$. The continuum limit remains open; the theorems here are finite-sum statements at fixed $B$.
A triangulation class is a combinatorially distinct bounded triangulation: the quotient of the labeled scoped configuration class by the relabeling setoid. A phase model packages a real phase on labeled bounded complexes together with the stated relabeling-invariance property. The phase function itself is an input; a substrate-derived phase is left open.
This definition is exactly the place where that invariance is consumed: it turns the labeled phase into a class-level phase so that unitary weights $\exp(i\cdot\mathrm{phase})$ can be assigned to classes without representative dependence.
proof idea
One-line definition by quotient lift: apply Quotient.lift to the labeled phase of the model, discharging well-definedness with the model's invariance field (equal phases on relabeling-equivalent complexes). No further arithmetic; the lift is the entire content. The companion lemma that evaluation on a representative recovers the labeled phase is definitional (rfl).
why it matters
This is the bridge from labeled phase data to class-level oscillatory weights. Downstream, the unitary class weight is $\exp(i\cdot\mathrm{classPhase})$, proved to have modulus one; empty-class and one-point-class witness weights evaluate to $+1$ and $-1$ via this descent; CapShellBridge transports the phase across the cap-to-shell carrier equivalence; and the grounding status theorem records that every phase model satisfies representative recovery and unit modulus.
In the Recognition gravity lane this enables the conditional pairing bounds on $Z_q$ (exact cancellation under opposite-phase pairs, strictly better than the triangle inequality), with a concrete $B=2$ witness. It does not close the open question of a substrate-derived phase; the model remains an input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.