IndisputableMonolith.Foundation.DeltaSpine.LadderRatioBounds

declarations in this module (17)

• def phiPow L56
• theorem phiPow_zero L60
• theorem phiPow_succ L62
• theorem phiPow_one L64
• theorem phiPow_five L67
• theorem phiPow_eight L70
• theorem phiPow_eq_phiZpow L75
• def ratWitness L90
• def RatLt L94
• def RatGt L98
• theorem phi_lower L112
• theorem phi_upper L115
• theorem phi5_lower L118
• theorem phi5_upper L121
• theorem phi8_lower L124
• theorem phi8_upper L127
• theorem ladder_ratio_brackets L135