HasseWeil · projects/HasseWeil/HasseWeil/Foundation/WronskianAux.lean · wronskian_aux_four.
From #7205 (PR #8328): the lemma carries set_option maxHeartbeats 350000 — the measured minimum on v4.32.0 (300000 fails at synthesize pending MVars, i.e. ring's normalization of the degree-30 residual against the degree-26 multiplier; removal attempts documented in-file). Getting to the default 200000 needs a structural change, not golf.
The route the module docstring itself recommends (its TODO, options analysed in the header): formalize the quotient ring ℤ[b₂,b₄,b₆,b₈] / (4b₈ − b₂b₆ + b₄²) where b_relation becomes a ring identity — the certificate then works over 3 atoms instead of 4 and the ring normalization shrinks; alternatively a bounded-degree coefficient-extraction tactic (doesn't exist in mathlib), or a manual algebraic split of the m=4 identity (research-level). The statement of wronskian_aux_four must stay byte-identical; wronskian_aux_three (default budget) is the template.
Bar: statement byte-identical; set_option removed (that's the point); module + OmegaPullbackCoeff consumer + HasseWeil green; zero new sorry; axioms unchanged = {propext, Classical.choice, Quot.sound}. Re-measure the 350000 baseline after the #8327 toolchain bump (v4.33.0-rc1) first — ring performance may shift; if the new toolchain fits 200000 outright, this ticket collapses to deleting the set_option.
HasseWeil·projects/HasseWeil/HasseWeil/Foundation/WronskianAux.lean·wronskian_aux_four.From #7205 (PR #8328): the lemma carries
set_option maxHeartbeats 350000— the measured minimum on v4.32.0 (300000 fails atsynthesize pending MVars, i.e.ring's normalization of the degree-30 residual against the degree-26 multiplier; removal attempts documented in-file). Getting to the default 200000 needs a structural change, not golf.The route the module docstring itself recommends (its TODO, options analysed in the header): formalize the quotient ring
ℤ[b₂,b₄,b₆,b₈] / (4b₈ − b₂b₆ + b₄²)whereb_relationbecomes a ring identity — the certificate then works over 3 atoms instead of 4 and theringnormalization shrinks; alternatively a bounded-degree coefficient-extraction tactic (doesn't exist in mathlib), or a manual algebraic split of the m=4 identity (research-level). The statement ofwronskian_aux_fourmust stay byte-identical;wronskian_aux_three(default budget) is the template.Bar: statement byte-identical;
set_optionremoved (that's the point); module +OmegaPullbackCoeffconsumer +HasseWeilgreen; zero new sorry; axioms unchanged = {propext, Classical.choice, Quot.sound}. Re-measure the 350000 baseline after the #8327 toolchain bump (v4.33.0-rc1) first — ring performance may shift; if the new toolchain fits 200000 outright, this ticket collapses to deleting the set_option.