PhaseModel
plain-language theorem explainer
A phase model at complexity cap B is a real-valued phase on labeled bounded complexes together with the stated relabeling-invariance property. Anyone attaching unitary weights to the quotient-first path sum Zq cites it: invariance is exactly what lets the phase descend to triangulation classes. Pure structure definition; the phase map is an input, not derived.
Claim. A phase model at complexity cap $B$ is a pair $(\theta,\mathrm{inv})$ where $\theta$ assigns a real phase to every labeled bounded complex of size at most $B$, and $\mathrm{inv}$ asserts that $\theta(K)=\theta(K')$ whenever $K$ and $K'$ are related by a relabeling equivalence.
background
Lane D3 of the Seven Gaps program works on the quotient-first object Zq: a finite sum over triangulation classes at fixed complexity cap B, rather than over labeled complexes. Classes are the quotient of BoundedComplex B by the relabeling setoid (Equivalent). The module status is theorem-level at fixed cap; the continuum limit remains open.
An oscillatory phase is needed to form unitary class weights exp(i θ). The structure packages that phase on the labeled carrier plus the invariance that makes descent legal. Downstream, classPhase is the Quotient.lift of the labeled phase, and phasedWeight is the complex exponential of that class phase (modulus exactly 1).
The phase function itself is model input. A substrate-derived phase (from eight-tick structure or recognition calculus) is explicitly left open in the doc-comment.
proof idea
No proof body: this is a structure declaration. It bundles a map phase : BoundedComplex B → ℝ with a Prop field requiring equality of phases on Equivalent pairs. Downstream defs (classPhase via Quotient.lift, phasedWeight via Complex.exp) consume the bundle; the invariance field is the exact hypothesis Quotient.lift needs.
why it matters
This is the interface object for all phased Zq work in the module. classPhase and classPhase_mk use the invariance field to descend to TriangulationClass; phasedWeight and phasedWeight_norm build unit-modulus class weights; totalClassMass bounds and Zq_phased_wellDefined then control ‖Zq‖ at fixed cap.
CapShellBridge.phaseModelAtCap transports shell-level phases into this structure. ZqContinuumBlocker.CapPhaseFamily is literally ∀ B, PhaseModel B. The B=2 witness (witnessPhaseModel, phased_Zq_witness_chain) discharges a concrete pairing hypothesis against this interface, giving a strict improvement over the triangle inequality.
Framework role: supplies the oscillatory data for cancellation on the quotient-first path sum without claiming a continuum or a derived phase. Substrate-derived phase and continuum coherence stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.