liftedPhase
plain-language theorem explainer
A relabeling-invariant real action on exact labeled complexes descends to a well-defined real function on each exact complexity shell. Anyone writing the regulated path-sum phase weight cites this as the honest parameter entry. The body is a one-line Quotient.lift using the invariance hypothesis on the shell's quotient component.
Claim. Let $S_{v,e,t}$ assign a real number to every exact complex of signature $(v,e,t)$, and assume $S$ is constant on global relabeling equivalence classes. Then for every complexity level $n$ there is an induced map from the exact complexity shell at $n$ (disjoint union over shell signatures of the quotient by global equivalence) to $\mathbb{R}$, sending each class to the common value of $S$ on any labeled representative.
background
This module builds the quotient-class path-sum configuration space as exact complexity shells: no size caps in the shell definition, then a Gaussian UV regulator $\exp(-\rho n^2)$ for the shell-resummed series. An exact complex of signature $(v,e,t)$ is a labeled incidence structure with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra. Global equivalence means existence of a relabeling isomorphism (bijections of index sets commuting with incidence). The exact complexity shell at level $n$ is the disjoint union, over signatures of complexity $n$, of the quotient of labeled exact complexes by that equivalence.
The phase entering unitary weights is deliberately a free parameter: any GlobalEquivalent-invariant real function on labeled complexes, equivalently any real function on classes. The same invariance pattern appears as the well-definedness hypothesis for the scoped path-sum measure. Module honesty rules state the regulator is mathematical (not derived physics) and regulator removal remains an open named flag.
proof idea
One-line definitional wrapper. For each shell level, ignore the level index and apply Quotient.lift to the quotient component of the shell sigma-type: the labeled map $S$ at the signature of the class, with the supplied invariance hypothesis discharging the lift's well-definedness obligation. No further lemmas or arithmetic.
why it matters
This is the clean interface by which a phase parameter enters Stage 2 of the seven-gaps path sum: the Gaussian-regulated shell term and its modulus bound treat phase as an arbitrary class function obtained exactly this way. It mirrors the invariance hypothesis of the scoped path-sum measure, so the UV-regularized series stays honest about what is derived versus parameterized. Downstream shell summability and cutoff convergence sit on top of such class weights; nothing here claims a physical continuum limit, mesh refinement, or regulator removal. In the broader Recognition stack the eight-tick octave and $D=3$ forcing are upstream landmarks for discrete structure, but this declaration only organizes combinatorial shells and does not flip any full-theory ledger flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.