ProximityPrize.SubmissionLower.squaredCode_minDistance

Proved

Yukon_f95a7d0592e97b0bdf84bedc

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

better-codes

Theorem ProximityPrize.SubmissionLower.squaredCode_minDistance from ProximityPrize.SubmissionLower.Solution.

Preamble

import Definitions.Def_Yukon_3a959d45e3b1473bdd011f50

Formal statement

theorem Yukon_f95a7d0592e97b0bdf84bedc : type_of% @ProximityPrize.SubmissionLower.squaredCode_minDistance := by sorry

Source

https://github.com/proximity-prize/proximity-prize/blob/207eb2212d947e27871c25e60dd3c1ad927955a1/ProximityPrize/SubmissionLower/Solution.lean#L29-L41 yukon-proof-operation:a441e72d-b55b-43a2-aa66-0e80d89c2cdb; Yukon contributor: anonymous [yukon-proof-receipt:eyJlbnZpcm9ubWVudCI6eyJtYXRobGliUmV2IjoiMGRmNDQ0YTM2MGVhYTYwYWI4YzExZGNhNTFhODZhZjY5Mjk1NTQ3NCIsInRvb2xjaGFpbiI6ImxlYW5wcm92ZXIvbGVhbjQ6djQuMzMuMSJ9LCJoYXNoIjoiNTI2ZjlhZjhiZTBkM2JiN2RlMmE4ZjExMjBmMzllODM5NDRkNzE1OTI3Y2IyMzRkNTFjOGUzMDZjOTA5ZDE1MSIsImtpbmQiOiJwcm9ibGVtIiwibWFya2VyIjoieXVrb24tcHJvb2Ytb3BlcmF0aW9uOmE0NDFlNzJkLWI1NWItNDNhMi1hYTY2LTBlODBkODljMmNkYjsgWXVrb24gY29udHJpYnV0b3I6IGFub255bW91cyIsInRhZyI6ImJldHRlci1jb2RlcyIsInRhcmdldCI6Ill1a29uX2Y5NWE3ZDA1OTJlOTdiMGJkZjg0YmVkYyIsInYiOjJ9]