module module

`IndisputableMonolith.Gravity.SevenGaps.ZqPhaseStructure`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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