module module

`IndisputableMonolith.Verification.CPT.ForcedFactorization`

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.Verification.CPT.Exports module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Verification.CPT.Core module_import

declarations in this module (19)

structure RatioCostSpace L29
def ratio L38
def canonicalCost L42
def CostImage L46
abbrev CostCode L50
structure CertificateHypotheses L57
structure RigidityHypotheses L73
structure PrimitiveCertificateHypotheses L79
structure PrimitiveRigidityHypotheses L94
theorem primitive_to_certificate L98
theorem primitive_to_rigidity L109
theorem certificate_depends_on_ratio L119
theorem exists_monotone_reparam L128
theorem existsUnique_cost_reparam L197
theorem phi_independent_of_state L223
theorem existsUnique_state_profile L234
theorem forced_factorization L248
theorem forced_factorization_unique L265
theorem forced_factorization_unique_of_primitives L279