module module high

`IndisputableMonolith.Gravity.SevenGaps.ZqPhaseStructure`

Explicit oscillatory phase model for the quotient-first path sum on scoped triangulation classes. A real phase on labeled configurations, required to be relabeling-invariant, is taken as an external input; a substrate-derived phase remains open. Gravity path-sum workers cite this when attaching phases to Z_q and bounding the phased sum. The module defines the model, phased weights, class-mass controls, and well-definedness of the phased pairing.

claimA phase model assigns to each labeled configuration a real phase that is invariant under relabeling of the configuration. The phased weight on a triangulation class is the Aut-normalized sum of $e^{i\theta}$ over labeled representatives, and the phased quotient path sum $Z_q^{\mathrm{phased}}(B,w_q,\theta)$ is well-defined on classes. Its complex modulus is bounded by the total class mass $\sum_q (1/|\mathrm{Aut}(q)|)\,|w_q(q)|$.

background

Seven Gaps work on the gravity path sum splits into pillars. Pillar 2 promotes a quotient-first object: sum over triangulation classes with the symmetry factor $1/|\mathrm{Aut}|$, rather than summing labeled configurations and then quotienting. Upstream, QuotientFirstZ constructs

$Z_q(B,w_q)=\sum_{q:\mathrm{TriangulationClass},B}(1/|\mathrm{Aut}(\mathrm{out},q)|)\cdot w_q(q)$.

Lane D1 (MeasureInvarianceNoGo) kills the claim that relabeling invariance plus positivity and normalization alone force the measure $\mu=1/|\mathrm{Aut}|$; explicit witnesses show other invariant measures exist. Phase structure therefore cannot be smuggled in as a uniqueness corollary of invariance.

This module supplies the missing oscillatory layer as an explicit model: a real phase on labeled configurations with a stated relabeling-invariance property. The phase function itself is an input parameter. Deriving that phase from the Recognition substrate is left open.

proof idea

Definition-and-lemmas module, not a single deep theorem. It introduces a PhaseModel structure (phase on labeled configs plus the invariance hypothesis), a class-level phase via any labeled representative, and the phased weight (Aut-normalized complex weight). Supporting facts: phased-weight norm equals the absolute class weight under unit-modulus phases; total class mass is positive and at most the class cardinality; the phased $Z_q$ norm is at most total class mass; well-definedness of the phased sum on the quotient; and a pairing decomposition that separates magnitude and phase contributions. Proofs are mostly algebraic unwinding of the quotient-first sum and the invariance hypothesis.

why it matters in Recognition Science

Feeds the downstream continuum blocker ZqContinuumBlocker (Seven Gaps P2-a). That module isolates analytic and API obligations for removing the complexity cutoff from the phased quotient path sum: the fixed-cap API expresses a family of phase models and hence a sequence of finite quotient sums; completeness of $\mathbb{C}$ reduces existence of the continuum limit to the Cauchy criterion on that sequence.

Without an explicit, relabeling-invariant phase model and the associated well-defined phased $Z_q$, the cutoff-removal argument has nothing to take limits of. The module also records the modeling gap stated in its header: phase is an input, not yet forced by the Recognition composition law or the T0–T8 chain. Closing that gap would connect oscillatory gravity weights to the same J-cost and eight-tick structure used elsewhere in the monolith.

scope and limits

Does not derive the phase from the Recognition substrate or J-cost; phase is an external model input.
Does not prove uniqueness of the path-sum measure from invariance alone (that claim is already killed upstream).
Does not remove the complexity cutoff or construct a continuum limit of phased sums.
Does not claim the phase is complex-analytic or comes from a Berry connection.
Does not fix numerical values of masses, G, or alpha; pure path-sum structure only.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo module_import
IndisputableMonolith.Gravity.SevenGaps.QuotientFirstZ module_import

declarations in this module (41)

structure PhaseModel L104
def classPhase L110
theorem classPhase_mk L114
def phasedWeight L118
theorem phasedWeight_norm L123
def totalClassMass L131
theorem totalClassMass_pos L136
theorem totalClassMass_le_card L142
theorem Zq_norm_le_totalClassMass L153
theorem at L170
theorem Zq_phased_wellDefined L171
theorem Zq_pairing_decomposition L192
theorem Zq_pairing_bound L227
theorem Zq_pairing_beats_triangle L257
theorem opposite_phase_exp L278
theorem opposite_phase_pair_cancels L286
theorem opposite_phase_pair_strict L293
abbrev onePointComplex L318
instance instSubsingletonAutOnePoint L331
theorem mu_onePointComplex L338
def emptyClass L344
def pointClass L348
theorem emptyClass_ne_pointClass L352
theorem mu_out_emptyClass L360
theorem mu_out_pointClass L365
def witnessPhaseModel L372
theorem phasedWeight_emptyClass L380
theorem phasedWeight_pointClass L390
def witnessPaired L400
def witnessPairing L403
theorem witnessPairing_injOn L407
theorem witnessPairing_disj L414
theorem witnessPairing_cancel L422
theorem witnessPaired_mass L438
theorem phased_Zq_pairing_witness L455
theorem phased_Zq_beats_triangle_witness L468
theorem two_le_totalClassMass_two L479
theorem phased_Zq_witness_chain L499
structure ZqPhaseStructureStatus L511
def zqPhaseStructureStatus L530
theorem zqPhaseStructureStatus_grounded L542