`phiInverseInvariantsCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.PhiInverseInvariants
domain: CrossDomain
line: 135 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.PhiInverseInvariants on GitHub at line 135.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 132    stemCellDecay = circadianDecay
 133  cabibbo_smaller : 0 < cabibboFactor ∧ cabibboFactor < phiInv
 134
 135noncomputable def phiInverseInvariantsCert : PhiInverseInvariantsCert where
 136  phiInv_pos := phiInv_pos
 137  phiInv_lt_one := phiInv_lt_one
 138  phiInv_lt_phi := phiInv_lt_phi
 139  fib_identity := phiInv_eq_phi_minus_one
 140  inv_sq_identity := phiInvSq_eq_two_minus_phi
 141  inv_cubed_identity := phiInvCubed_eq_two_phi_minus_three
 142  five_instances_equal := all_phiInv_instances_equal
 143  cabibbo_smaller := cabibbo_in_unit
 144
 145end IndisputableMonolith.CrossDomain.PhiInverseInvariants

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.