classPhase_mk
plain-language theorem explainer
On any phase model, the descended class phase of a relabeling orbit equals the phase of a labeled representative. Citation target for well-definedness of oscillatory weights on triangulation classes in the quotient-first path sum. Proof is pure definitional equality (rfl).
Claim. Fix a complexity cap $B\in\mathbb{N}$, a phase model $P$ (real phase on labeled bounded complexes, invariant under relabeling), and a labeled complex $K$. Then the class phase of the relabeling orbit of $K$ equals $P$'s phase on $K$: $\mathrm{classPhase}(P,[K])=P.\mathrm{phase}(K)$.
background
Lane D3 of the Seven Gaps program equips the quotient-first path sum $Z_q$ with an explicit oscillatory phase. A PhaseModel at fixed cap $B$ is a real-valued phase on labeled bounded complexes together with the stated invariance: equivalent (relabeled) complexes receive the same phase. That invariance is exactly what lets the phase descend to triangulation classes.
The descended map is classPhase: it assigns a phase to each class in the quotient by the relabeling setoid. Configurations live in BoundedComplex B; classes are Quotient.mk of that setoid. The module proves unit-modulus phased weights, fixed-cap boundedness of phased $Z_q$, and conditional pairing cancellation; continuum limit remains open.
Doc-comment on the model: "the phase function itself is an input; a substrate-derived phase is OPEN." This lemma only records how descent evaluates on representatives.
proof idea
One-line term proof by rfl. By construction, classPhase is the quotient lift of the labeled phase using the model's invariance proof; evaluating the lift on Quotient.mk K is definitionally the phase of $K$. No lemmas are applied.
why it matters
Feeds the grounding theorem zqPhaseStructureStatus_grounded, which requires that every true status flag ties to a kernel statement: in particular, for all $B$ and all phase models $P$, class phase on the class of $K$ equals $P$'s phase on $K$, and phased weights have unit modulus. Without this identity the descent story is incomplete and the status flag cannot be set.
In the Seven Gaps gravity lane this is bookkeeping that makes oscillatory structure on $Z_q$ honest at fixed complexity cap. It does not derive a physical phase from the Recognition substrate (that remains open per the PhaseModel doc). Framework landmarks nearby are the eight-tick octave and path-sum measures; this lemma itself is pure quotient algebra, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.