module module

`IndisputableMonolith.Holography.DeficitFreePeriod`

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 (2)

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

IndisputableMonolith.Holography.HorizonClockRate module_import
IndisputableMonolith.Holography.TurnRatioCarrier module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Holography.KeystoneFactorThree module_import

declarations in this module (20)

def holonomy L85
def deficitCost L92
def euclideanPeriod L96
def ClausiusForm L102
def HorizonRate L108
theorem deficitCost_eq_half_normSq L115
theorem deficitCost_nonneg L127
theorem deficitCost_eq_zero_iff L133
theorem deficitCost_pos_of_not_period L148
theorem deficitCost_hasDerivAt L158
theorem deficitCost_critical_at_zero L165
theorem deficitCost_second_deriv_pos_at_zero L171
theorem holonomy_eq_one_iff_lattice L178
theorem holonomy_deficit_free_iff L201
theorem holonomy_eq_one_iff L207
theorem euclideanPeriod_isLeast L226
theorem bekenstein_saturation_from_deficit_free_period L260
theorem totalEntropyBound_saturating_case L276
structure DeficitFreePeriodCert L292
theorem deficitFreePeriodCert L302