Repository navigation
lean(#16752): migrer 4 theoremes GenEFT (PR #16968) dans EffectiveTheory/* sans module parallele #17480
Description
Activity
- added a commit that references this issue
on Sep 23, 2026 [VERIFIED DELIVERED] Verification par contenu sur
origin/main(8849ce1e27) avant close — grain de cette lane, aucun claim concurrent.Livrable livre par #17494 (
feat(lean,#17480): migrer 4 theorèmes GenEFT dans EffectiveTheory/*, MERGED 2026-09-23T10:09:13Z), non close depuis.Les 4 theoremes du tableau, sur main avec preuves reelles (0
sorrydans les deux zones verifiees) :Theoreme Emplacement main Preuve mem_aut_iffEffectiveTheory/InfoBits.lean:185corps tactique complet (stabilizer <-> preservation d'adjacence) card_orbit_mul_card_autEffectiveTheory/InfoBits.lean:216exact MulAction.card_orbit_mul_card_stabilizer_eq_card_groupdescLength/descLength_eqEffectiveTheory/InfoBits.lean:229/:235def noncomputable + quotient `n! / rel_eqn_autonomous(Eq. 16)EffectiveTheory/Repons.lean:133derivation F(x1-x2), section Dynamics Dissolution :
GenEFT.leanabsent degit ls-tree origin/main(seul reste un notebook homonyme, hors perimetre).lakefile.lean:62-73documente la digestion et ne reference plus aucun module GenEFT.Exceptions respectees :
clustering/competition_invariantnon dupliques (couverts par #16968).Verdict : livrable complet sur main, conforme a l'arbitrage (option 3 restreinte, sans module parallele). Close par la lane du grain.
Grain: DEEP/lean -- lane myia-po-2026:CoursIA -- prev: DEEP/lean #16968
Arbitrage ai-01 2026-09-23 (DM msg-20260923T005705-98ehlt, thread po2026-arb-16752-doublons) : option 3 restreinte — enrichissement de
EffectiveTheory/*apportant UNIQUEMENT les theoremes absents de #16968 (GenEFT.lean), rebase sur main, sans module parallele : dissolution du moduleGenEFT.lean, preuves migrees dans l'arbre existant, lakefile mis a jour.Theoremes absents de main (tableau poste sur #16968, c.5787370336)
mem_aut_iffcard_orbit_mul_card_autdescLength/descLength_eqrel_eqn_autonomous(Eq. 16 Appendice C)Repons.lean(section Dynamics, a cote de conservedHyperbola_deriv_zero)Exceptions au tableau (COUVERTS, NE PAS migrer) :
clustering= Repons.clustering_iff_injective_decoder ;competition_invariant= Repons.conservedHyperbola_deriv_zero (iteration precedente #16968).Acceptance
EffectiveTheory/*(fichiers existants, pas de nouveau module top-level)GenEFT.lean/GenEFT_en.leansupprimes ; lakefilelearning_theory_leansans globs GenEFTlake buildSUCCESS local (regle H) +grep -c sorryavant/apres = 0_enpour les modules enrichis (convention i18n, cf issue lean(i18n,#4980): siblings _en manquants pour les modules de #16794 (EffectiveTheory) #17481)See #16752, See #16794, See #16968.