module module

`IndisputableMonolith.CrossDomain.PhiInverseInvariants`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (18)

def phiInv L31
theorem phiInv_pos L33
theorem phiInv_lt_one L37
theorem phiInv_lt_phi L41
theorem phiInv_eq_phi_minus_one L50
theorem phiInvSq_eq_two_minus_phi L60
theorem phiInvCubed_eq_two_phi_minus_three L69
def senolyticTargetRatio L80
def giniCeiling L83
def policyBalance L86
def stemCellDecay L89
def circadianDecay L92
def cabibboFactor L95
theorem all_phiInv_instances_equal L98
theorem all_phiInv_in_unit_interval L105
theorem cabibbo_in_unit L109
structure PhiInverseInvariantsCert L121
def phiInverseInvariantsCert L135