module module

`IndisputableMonolith.Holography.TurnRatioCarrier`

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.SeamTransferCore module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Holography.DeficitFreePeriod module_import
IndisputableMonolith.Holography.EightTickSubperiodExclusion module_import

declarations in this module (39)

def turnRatio L76
def turnRatioCost L81
theorem turnRatio_pos L84
theorem turnRatio_eq_one_iff L90
theorem turnRatioCost_nonneg L102
theorem turnRatioCost_eq_zero_iff L110
theorem turnRatioCost_pos_of_ne_period L118
theorem turnRatioCost_reciprocal L127
theorem turnRatio_cover L134
theorem Jcost_cover_value L142
theorem turnRatioCost_cover_pos L150
theorem lattice_period_zero_cost_iff L163
def phaseCost L177
theorem phaseCost_eq L181
theorem phaseCost_nonpos L192
theorem phaseCost_vanishes_on_covers L199
def JextRe L206
theorem JextRe_agrees L209
def Jprime L218
def Jsecond L222
theorem Jprime_agrees L224
theorem Jsecond_agrees L229
theorem JextRe_I L238
theorem Jprime_I L243
theorem Jsecond_I L248
theorem u1_extension_not_unique L255
theorem u1_extension_zero_set_not_forced L268
theorem euclideanPeriod_unbounded L282
theorem turnRatioCost_unbounded_near_zero_kappa L300
def accumulatedCost L339
theorem accumulatedCost_unbounded L343
def visitCount L356
def witnessWalk L361
theorem eight_tick_multiple_exclusion L371
def CensusPricing L395
theorem turnRatioCost_censusPricing L399
theorem b2_unique_zero_of_censusPricing L407
structure TurnRatioCarrierCert L421
theorem turnRatioCarrierCert L438