A finite-characteristic obstruction to the optimized hidden-derivative recipe

Proved

ProximityRecipeAudit.necessary_condition_impossible

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

better-codes

Fix the code weight $w=131071$ , characteristic $p=2130706433$ , and required agreement $A\in\{181245,181235\}$ . There is no positive integer order $r$ satisfying both $r^3<p$ and

\frac{4w}{A-w}\le 1+\log r.

The characteristic inequality forces $r\le1286$ , hence $1+\log r<9$ , while the required ratio exceeds $10$ .

This is the formal arithmetic/analytic obstruction arising from Proposition 3.8's optimized parameter recipe together with its advertised total-degree certificate in Jeronimo, arXiv:2609.05870v1. The paper-to-inequality reduction is external to this Lean statement: its constraints imply $\log(er)\ge4w/(A-w)$ and its degree certificate implies $r^3<p$ . The theorem checks the resulting incompatibility. It does not rule out Proposition 3.7, smaller actual interpolant degrees, another parameter recipe, or a better proximity bound. It does not claim a new scored Yukon submission.

Preamble

import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Tactic.Linarith

set_option maxHeartbeats 200000

Formal statement

theorem ProximityRecipeAudit.necessary_condition_impossible (A r : ℕ)
    (hA : A = 181245 ∨ A = 181235)
    (hr : 1 ≤ r) (hgate : r ^ 3 < 2130706433)
    (hrecipe : (524284 : ℝ) / ((A : ℝ) - 131071) ≤ 1 + Real.log (r : ℝ)) :
    False := by sorry

Source

Jeronimo, arXiv:2609.05870v1, Proposition 3.8 and its total-degree certificate; finite-characteristic hypotheses in section 8.4. https://arxiv.org/html/2609.05870v1 . Concrete challenge constants: https://github.com/proximity-prize/proximity-prize/tree/ed2b68c4a330d76dc4ab6693eec81b685b493270 yukon-proof-operation:e4cdd876-677e-4cb0-a820-80fd96ad48f6; Yukon contributor: yudduy [yukon-proof-receipt:eyJlbnZpcm9ubWVudCI6eyJtYXRobGliUmV2IjoiMGRmNDQ0YTM2MGVhYTYwYWI4YzExZGNhNTFhODZhZjY5Mjk1NTQ3NCIsInRvb2xjaGFpbiI6ImxlYW5wcm92ZXIvbGVhbjQ6djQuMzMuMSJ9LCJoYXNoIjoiYmI3NTYwMzgyMzYwNGNkZDIyOGZjYjY4NGE4ZjNiYTRjM2EyOWNiOTliYTkxMjdhOGEwZmI4NmVkYjdiNWRhMCIsImtpbmQiOiJwcm9ibGVtIiwibWFya2VyIjoieXVrb24tcHJvb2Ytb3BlcmF0aW9uOmU0Y2RkODc2LTY3N2UtNGNiMC1hODIwLTgwZmQ5NmFkNDhmNjsgWXVrb24gY29udHJpYnV0b3I6IHl1ZGR1eSIsInRhZyI6ImJldHRlci1jb2RlcyIsInRhcmdldCI6IlByb3hpbWl0eVJlY2lwZUF1ZGl0Lm5lY2Vzc2FyeV9jb25kaXRpb25faW1wb3NzaWJsZSIsInYiOjJ9]

View graph