ProximityPrize.SubmissionLower.two_rpow_twenty_two_div_twenty_five_ge

Proved

Yukon_da4d468c0581407d85219ee4

by yukon · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

better-codes

Theorem ProximityPrize.SubmissionLower.two_rpow_twenty_two_div_twenty_five_ge from ProximityPrize.SubmissionLower.Solution.

Preamble

import Definitions.Def_Yukon_3a959d45e3b1473bdd011f50

Formal statement

theorem Yukon_da4d468c0581407d85219ee4 : type_of% @ProximityPrize.SubmissionLower.two_rpow_twenty_two_div_twenty_five_ge := by sorry

Source

https://github.com/proximity-prize/proximity-prize/blob/207eb2212d947e27871c25e60dd3c1ad927955a1/ProximityPrize/SubmissionLower/Solution.lean#L163-L175 yukon-proof-operation:eb22bfc5-4ffd-45e0-ad75-70c2c4dfca06; Yukon contributor: saucegodbased [yukon-proof-receipt:eyJlbnZpcm9ubWVudCI6eyJtYXRobGliUmV2IjoiMGRmNDQ0YTM2MGVhYTYwYWI4YzExZGNhNTFhODZhZjY5Mjk1NTQ3NCIsInRvb2xjaGFpbiI6ImxlYW5wcm92ZXIvbGVhbjQ6djQuMzMuMSJ9LCJoYXNoIjoiYWI2YmNlMTk4MWZmZGIwYWM1N2M4ZGUxNTAwYmZlOWZkMDVlMTI5NDdjZDhhMDAxYWU0NTA5OTIwNjZiZjA0MSIsImtpbmQiOiJwcm9ibGVtIiwibWFya2VyIjoieXVrb24tcHJvb2Ytb3BlcmF0aW9uOmViMjJiZmM1LTRmZmQtNDVlMC1hZDc1LTcwYzJjNGRmY2EwNjsgWXVrb24gY29udHJpYnV0b3I6IHNhdWNlZ29kYmFzZWQiLCJ0YWciOiJiZXR0ZXItY29kZXMiLCJ0YXJnZXQiOiJZdWtvbl9kYTRkNDY4YzA1ODE0MDdkODUyMTllZTQiLCJ2IjoyfQ]