module module

`IndisputableMonolith.Foundation.GlobalCoIdentityConstraint`

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

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Papers.GCIC.GraphRigidity module_import
IndisputableMonolith.Papers.GCIC.ReducedPhasePotential module_import

declarations in this module (14)

def wrapPhase L104
theorem wrapPhase_bounds L107
theorem wrapPhase_add_int L113
theorem wrapPhase_eq_of_int_diff L121
theorem gcic_global_phase_unique L155
theorem gcic_existence_of_global_phase L172
theorem gcic_global_phase_independent_of_basepoint L197
theorem gcic_global_phase_independent_of_path L218
def lam_canonical L234
theorem lam_canonical_ne_zero L237
theorem gcic_canonical L246
structure GlobalCoIdentityConstraintCert L264
def gcicCert L287
theorem gcic_one_statement L305