Conversation
rjwalters
force-pushed
the
feature/enricher-1
branch
from
5961090 to
2fe8feb
Compare
rjwalters
changed the title
rjwalters
force-pushed
the
feature/enricher-1
branch
from
2fe8feb to
5d9e670
Compare
rjwalters
changed the title
rjwalters
force-pushed
the
feature/enricher-1
branch
from
5d9e670 to
0e34b95
Compare
rjwalters
changed the title
rjwalters
force-pushed
the
feature/enricher-1
branch
2 times, most recently
from
df6c40b to
53d9794
Compare
rjwalters
changed the title
…oricalContext - Added 6 annotations covering Lagrange's theorem foundations, Sylow I existence+order formula, Sylow II conjugacy, Sylow III counting constraints, partial converse to Lagrange, and Cauchy's theorem as corollary - Added 7 sections covering all proof regions (header, imports, Lagrange, Sylow existence, Sylow conjugacy, Sylow counting, partial converse) - Expanded historicalContext with Sylow (1832-1918) biography, 1872 paper, Burnside's systematization, Wielandt's 1959 proof, and classification context - Added 5th keyInsight about n_p ≡ 1 mod p counting from fixed-point analysis and its normality criterion consequence - Expanded conclusion with Hall's theorem and classification implications Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- Added ann-kummer-oq03-specific-rows: covers choose_prime_div and choose_prime_sq_div (lines 64-75) with Fermat's little theorem connection and Wieferich primes context - Added header section (lines 1-23) covering research question and references - Added summary section (lines 92-116) covering fractal structure discussion - Now 5 annotations with full mathContext/significance/relatedConcepts coverage - Now 6 sections covering all proof regions Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…tion - Added ann-pz-header annotation (lines 1-34): context annotation describing the Paley-Zygmund quantitative upgrade over the qualitative second moment method, with the classical probabilistic statement in LaTeX - Added header section (lines 1-34) covering research question and imports - Now 5 annotations with mathContext/significance/relatedConcepts coverage - Now 4 sections covering all proof regions Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…text/keyInsights - Added 6 annotations: Sylow I existence+order, Sylow II conjugacy+isomorphism, Sylow III counting constraints, normality-uniqueness equivalence, Cauchy's theorem, and classification applications (order 15 example) - Added 7 sections covering all proof regions (imports+header, Sylow structure, Sylow I-III, normality, Cauchy, applications) - Expanded historicalContext with Sylow (1832-1918), Burnside 1897, Wielandt 1959, and Wiedijk #72 context - Added 5th keyInsight about Lean 4's Sylow p G bundled structure type - Expanded conclusion with Schur-Zassenhaus and classification extensions - Added cross-reference to lagrange-theorem-oq-01 companion proof Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…/insights - Added 5 annotations: IsPQGroup structure, Sylow q uniqueness (n_q=1 proof), Sylow p analysis (coprimality criterion), core 80-line cyclicity proof (commutator argument + order product formula), and classification theorem - Added 7 sections: header, setup/helpers, Sylow q uniqueness, Sylow p analysis, cyclic proof, non-abelian classification, concrete examples - Expanded historicalContext with Burnside 1911, semidirect product construction, and order-6/15/21/35 examples - Added 5th keyInsight about IsPQGroup structure bundling design choice - Expanded conclusion with semidirect products and p²q classification Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…, expand context - Added 5 annotations: chord quadratic inner product expansion, Vieta product formula without explicit roots, opposite sign analysis for interior point, power of a point invariance theorem, explicit 3D Sphere3D corollary - Added 5 sections covering all proof regions (header, chord quadratic, Vieta product, power of point, 3D corollary, conclusion) - Expanded historicalContext with Jakob Steiner (1796-1863) and 'power of a point' (Potenz eines Punktes 1826), Greek origins in Euclid Elements III - Added 5th keyInsight about type-class polymorphism enabling dimension-free proof - Expanded conclusion with complex Hilbert space and exterior point extensions Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…d context - Add 7 sections covering all 250 lines (header, concrete verifications, boundary values, orbit-stabilizer lemma, Burnside main theorem, weighted partition identity, summary) - Add 5 annotations: module overview, native_decide witnesses, card_perm_fixing_point orbit-stabilizer proof, Burnside's lemma application, fiberwise double-counting for weighted identity - Expand historicalContext: Montmort 1708, de Moivre 1718, Burnside 1897, Chen-Stein Poisson(1) limit - Add 5th keyInsight: native_decide role as computational witness - Expand conclusion with Poisson approximation open question Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
rjwalters
force-pushed
the
feature/enricher-1
branch
from
dd118d1 to
346464b
Compare
…text - Add 7 sections covering all 277 lines (header, order/factorization, Sylow constraints, exact numbers, non-normality, conjugacy class decision, simplicity/corollaries) - Add 5 annotations: A₅ historical significance (Galois 1832, Abel-Ruffini, CFSG context), exact Sylow numbers via native_decide, Sylow.unique_of_normal reusable pattern, conjugacy class decide proof, not-solvable via S₅ short exact sequence - Expand historicalContext: Jordan 1870 Traité, Burnside 1897, PSL(2,5) isomorphism, CFSG connection - Add 5th keyInsight: Sylow.unique_of_normal → Fintype.card_unique contradiction idiom - Add 3rd openQuestion: PSL(2,p) generalization Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…and keyInsights - Add 7 sections covering all 277 lines (header, order/factorization, Sylow constraints, exact numbers, non-normality, conjugacy class decision, simplicity/corollaries) - Expand historicalContext: Galois 1832, Abel/Ruffini, Jordan 1870 Traite, Burnside 1897, PSL(2,5) isomorphism, CFSG connection - Add 5th keyInsight: Sylow.unique_of_normal -> Fintype.card_unique contradiction idiom - Add 3rd openQuestion: PSL(2,p) generalization Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…xpand context - Add 6 sections covering all 341 lines (header, pi-from-nesterenko, exp-pi + gamma-quarter, pi*exp-pi + irrationality, Schanuel conditional proofs, summary hierarchy) - Add 5 annotations: module overview, polynomial lifting technique (detailed template proof), e^pi transcendence (Gelfond 1929 via Nesterenko 1996), pi*exp-pi composite polynomial trick, Schanuel named-axiom pattern for conditional e+pi results - Expand historicalContext: Hermite 1873, Lindemann 1882, Gelfond 1929, Gelfond-Schneider 1934, Nesterenko 1996, Schanuel 1960s - Add 5th keyInsight: X0*X1 composite polynomial specialization trick - Add 5th openQuestion: e^e transcendence Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- Add 7 sections covering all 253 lines (header, definitions/basics, log bounds, Theisinger p-adic, sandwich gap/convergence rate, rational exclusion, documented Gamma/Zeta connections) - Add 5 annotations: 42-theorem overview and open status of γ irrationality, sandwich gap explicit convergence rate, Theisinger 2-adic valuation argument, systematic rational exclusion with 3/5 noted as unreachable by basic bounds, documented Gamma/Zeta connections excluded from >32GB build - Expand historicalContext was already good; keyInsights already 4 (no changes needed to overview sections) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…q-02 audited clean (#9516) New proof detected (Fodor's Pressing-Down Lemma). Gallery entry exists as untracked files on disk; Lean file is on feature/researcher-7 (PR #9500). Meta.json claims match Lean file: 1 sorry (diagInter_isUnbounded) confirmed. Script false-positive: "sorry mismatch" because Lean file not on main yet. Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
) * Enrich derangements-convergence: 5 annotations, 6 sections, expanded history Adds full annotation coverage and deepens all metadata sections for the Derangements Converge to 1/e gallery entry (Wiedijk #88). Annotations added (5): - ann-derang-conv-identity: D(n)=n!·altFactPartialSum strong induction bridge (lines 56-75) - ann-derang-conv-tsum: Linking e⁻¹ to alternating series via NormedSpace.exp_eq_tsum (lines 86-116) - ann-derang-conv-nonneg: Parity-splitting induction for alternating series bounds (lines 120-208) - ann-derang-conv-tail: Passing finite bounds to infinite tail via tendsto limits (lines 210-242) - ann-derang-conv-main: Composing the full convergence proof chain (lines 246-283) Meta enrichments: - 6 sections covering all 284 lines - 5th keyInsight: tsum_eq_partial_sum_add_tail as technical bridge - Expanded historicalContext: Montmort 1708, Euler 1751, Leibniz alternating series 1682, probabilistic interpretation, Wiedijk #88 significance - 4 crossReferences: derangements-oq-03-oq-02 (extends), derangements (related), e-transcendental (related), prob-method-expectation (related) - Expanded openQuestions: D_k(n) convergence rate, D(n)=round(n!/e) integer identity Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich lagrange-theorem-oq-01: 5 annotations, 6 sections, Sylow history Adds full annotation coverage and deepens all metadata sections for the Sylow Theorems as Partial Converse to Lagrange gallery entry. Annotations added (5): - ann-lagrange-oq01-lagrange: Lagrange as card_subgroup_dvd_card delegation (lines 34-44) - ann-lagrange-oq01-existence: First Sylow theorem and p-adic multiplicity (lines 56-67) - ann-lagrange-oq01-conjugacy: Second Sylow theorem via MulAut.conj (lines 79-82) - ann-lagrange-oq01-counting: Third Sylow theorem n_p ≡ 1 mod p via orbit counting (lines 94-101) - ann-lagrange-oq01-converse: Partial converse to Lagrange + Cauchy's theorem (lines 114-123) Meta enrichments: - 6 sections covering all 141 lines in 5 parts - 5th keyInsight: n_p ≡ 1 mod p constraints groups of order pq classification - Expanded historicalContext: Lagrange 1771, Cauchy 1845, Sylow 1872 (denied university post!), A₄ counterexample, Feit-Thompson 1963, classification program - 3 crossReferences: lagrange-theorem (extends), burnside-lemma (related, orbit-counting in Sylow III proof), cauchy-schwarz (related, Cauchy namesake) - Expanded openQuestions: pq classification, A₄ subgroup 6, Hall's theorem Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich derangements-oq-02-oq-02: 5 annotations, 5 sections, Burnside history Adds full annotation coverage and deepens all metadata sections for the Expected Fixed Points of a Random Permutation gallery entry. Annotations added (5): - ann-derang-oq02-oq02-concrete: native_decide concrete verifications (lines 51-89) - ann-derang-oq02-oq02-orbit-stab: Orbit-stabilizer (n-1)! fixing lemma (lines 103-138) - ann-derang-oq02-oq02-burnside: Burnside's lemma 3-rewrite proof (lines 158-177) - ann-derang-oq02-oq02-double-counting: sum_fiberwise weighted identity (lines 200-227) - ann-derang-oq02-oq02-summary: Generating function G_n'(1)=G_n(1)=n! (lines 230-248) Meta enrichments: - 5 sections covering all 250 lines - 5th keyInsight: the original sorry was resolved using card_perms_with_kfixed from parent, enabling the step1 fiber rewriting - Expanded historicalContext: Burnside-Cauchy-Frobenius attribution dispute (Burnside himself credited Frobenius), linearity of expectation proof of E[#fixed]=1 - 4 crossReferences: derangements-oq-02 (extends), derangements (related), burnside-lemma (uses), lagrange-theorem-oq-01 (related, orbit-stabilizer) - Expanded openQuestions: higher moments, generating function, Poisson(1) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
…ights - Add 6 sections covering all 445 lines (header, theta upper bound, central binomial + prime divisibility, power bound + pi connection, Bertrand lower bounds, binomial lower bound + log corollary) - Add 5 annotations: Chebyshev 1852 historical overview, theta(n) <= n*log(4) via primorial + log_prod, prime_in_interval_dvd_centralBinom core divisibility lemma, pi(n) >= log2(n) telescoping Bertrand proof, central binomial sandwich 4^n/(2n+1) <= C(2n,n) <= 4^n - Expand keyInsights to 5: add sandwich bound proof details with choose_le_middle and primorial_le_4_pow explanation Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Automated sync of research iteration counts and problem listings. Co-authored-by: Claude <noreply@anthropic.com>
… historical context - 7 sections covering all 254 lines (header, core results, bounded degree, exact degree, stratification, degree 1/monotone, cardinality/filtration) - 5 annotations: Cantor 1874 overview, one-line proof via Algebraic.countable, degree stratification + alternative proof, bounded vs exact degree filtration structure, cardinal paradox (algebraic ≅ ℚ ≅ ℕ despite proper containment) - Expanded historicalContext: Cantor's 'height' function approach, Liouville 1844 vs Cantor cardinality argument, pre-1874 lack of known transcendentals - Added 5th keyInsight: degree 1 = ℚ via isAlgebraic_algebraMap connecting stratification to denumerability Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- 6 sections covering all 599 lines (header, core definitions + cos20, strict hierarchy proof, tool degrees + Mohr-Mascheroni, 2-3 number theory + Pierpont, Poncelet-Steiner + polygon classification) - 5 annotations: five-level tool hierarchy overview, three_not_dvd_power_of_two arithmetic core, Mohr-Mascheroni/Poncelet-Steiner by rfl, 2-3 number closure + exclusion pattern, Pierpont primes as Fermat prime generalization - Expanded historicalContext: ancient neusis (Archimedes, Nicomedes), Mohr-Mascheroni 1672/1797, Poncelet-Steiner 1833, Gleason 1988 algebraic characterization, Huzita-Justin 1989/1991 - Added 5th keyInsight: eleven_not_pierpont/eleven_not_two_three via prime divisibility pattern Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
rjwalters
added a commit
that referenced
this pull request
Apr 4, 2026
…out-poly, CS-integral, prob-method (#9503) * Enrich lagrange-theorem-oq-01: 6 annotations, 7 sections, expand historicalContext - Added 6 annotations covering Lagrange's theorem foundations, Sylow I existence+order formula, Sylow II conjugacy, Sylow III counting constraints, partial converse to Lagrange, and Cauchy's theorem as corollary - Added 7 sections covering all proof regions (header, imports, Lagrange, Sylow existence, Sylow conjugacy, Sylow counting, partial converse) - Expanded historicalContext with Sylow (1832-1918) biography, 1872 paper, Burnside's systematization, Wielandt's 1959 proof, and classification context - Added 5th keyInsight about n_p ≡ 1 mod p counting from fixed-point analysis and its normality criterion consequence - Expanded conclusion with Hall's theorem and classification implications Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich kummer-theorem-oq-03: add 5th annotation, header/summary sections - Added ann-kummer-oq03-specific-rows: covers choose_prime_div and choose_prime_sq_div (lines 64-75) with Fermat's little theorem connection and Wieferich primes context - Added header section (lines 1-23) covering research question and references - Added summary section (lines 92-116) covering fractal structure discussion - Now 5 annotations with full mathContext/significance/relatedConcepts coverage - Now 6 sections covering all proof regions Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich prob-method-second-moment-oq-01: add header annotation and section - Added ann-pz-header annotation (lines 1-34): context annotation describing the Paley-Zygmund quantitative upgrade over the qualitative second moment method, with the classical probabilistic statement in LaTeX - Added header section (lines 1-34) covering research question and imports - Now 5 annotations with mathContext/significance/relatedConcepts coverage - Now 4 sections covering all proof regions Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich sylow-theorem: 6 annotations, 7 sections, expand historicalContext/keyInsights - Added 6 annotations: Sylow I existence+order, Sylow II conjugacy+isomorphism, Sylow III counting constraints, normality-uniqueness equivalence, Cauchy's theorem, and classification applications (order 15 example) - Added 7 sections covering all proof regions (imports+header, Sylow structure, Sylow I-III, normality, Cauchy, applications) - Expanded historicalContext with Sylow (1832-1918), Burnside 1897, Wielandt 1959, and Wiedijk #72 context - Added 5th keyInsight about Lean 4's Sylow p G bundled structure type - Expanded conclusion with Schur-Zassenhaus and classification extensions - Added cross-reference to lagrange-theorem-oq-01 companion proof Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich sylow-theorem-oq-01: 5 annotations, 7 sections, expand history/insights - Added 5 annotations: IsPQGroup structure, Sylow q uniqueness (n_q=1 proof), Sylow p analysis (coprimality criterion), core 80-line cyclicity proof (commutator argument + order product formula), and classification theorem - Added 7 sections: header, setup/helpers, Sylow q uniqueness, Sylow p analysis, cyclic proof, non-abelian classification, concrete examples - Expanded historicalContext with Burnside 1911, semidirect product construction, and order-6/15/21/35 examples - Added 5th keyInsight about IsPQGroup structure bundling design choice - Expanded conclusion with semidirect products and p²q classification Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich product-of-segments-of-chords-oq-01: 5 annotations, 5 sections, expand context - Added 5 annotations: chord quadratic inner product expansion, Vieta product formula without explicit roots, opposite sign analysis for interior point, power of a point invariance theorem, explicit 3D Sphere3D corollary - Added 5 sections covering all proof regions (header, chord quadratic, Vieta product, power of point, 3D corollary, conclusion) - Expanded historicalContext with Jakob Steiner (1796-1863) and 'power of a point' (Potenz eines Punktes 1826), Greek origins in Euclid Elements III - Added 5th keyInsight about type-class polymorphism enabling dimension-free proof - Expanded conclusion with complex Hilbert space and exterior point extensions Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich derangements-oq-02-oq-02: add 5 annotations, 7 sections, expand context - Add 7 sections covering all 250 lines (header, concrete verifications, boundary values, orbit-stabilizer lemma, Burnside main theorem, weighted partition identity, summary) - Add 5 annotations: module overview, native_decide witnesses, card_perm_fixing_point orbit-stabilizer proof, Burnside's lemma application, fiberwise double-counting for weighted identity - Expand historicalContext: Montmort 1708, de Moivre 1718, Burnside 1897, Chen-Stein Poisson(1) limit - Add 5th keyInsight: native_decide role as computational witness - Expand conclusion with Poisson approximation open question Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich sylow-theorem-oq-04: add 5 annotations, 7 sections, expand context - Add 7 sections covering all 277 lines (header, order/factorization, Sylow constraints, exact numbers, non-normality, conjugacy class decision, simplicity/corollaries) - Add 5 annotations: A₅ historical significance (Galois 1832, Abel-Ruffini, CFSG context), exact Sylow numbers via native_decide, Sylow.unique_of_normal reusable pattern, conjugacy class decide proof, not-solvable via S₅ short exact sequence - Expand historicalContext: Jordan 1870 Traité, Burnside 1897, PSL(2,5) isomorphism, CFSG connection - Add 5th keyInsight: Sylow.unique_of_normal → Fintype.card_unique contradiction idiom - Add 3rd openQuestion: PSL(2,p) generalization Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich sylow-theorem-oq-04: add 7 sections, expand historicalContext and keyInsights - Add 7 sections covering all 277 lines (header, order/factorization, Sylow constraints, exact numbers, non-normality, conjugacy class decision, simplicity/corollaries) - Expand historicalContext: Galois 1832, Abel/Ruffini, Jordan 1870 Traite, Burnside 1897, PSL(2,5) isomorphism, CFSG connection - Add 5th keyInsight: Sylow.unique_of_normal -> Fintype.card_unique contradiction idiom - Add 3rd openQuestion: PSL(2,p) generalization Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich e-transcendental-oq-01-oq-01: add 5 annotations, 6 sections, expand context - Add 6 sections covering all 341 lines (header, pi-from-nesterenko, exp-pi + gamma-quarter, pi*exp-pi + irrationality, Schanuel conditional proofs, summary hierarchy) - Add 5 annotations: module overview, polynomial lifting technique (detailed template proof), e^pi transcendence (Gelfond 1929 via Nesterenko 1996), pi*exp-pi composite polynomial trick, Schanuel named-axiom pattern for conditional e+pi results - Expand historicalContext: Hermite 1873, Lindemann 1882, Gelfond 1929, Gelfond-Schneider 1934, Nesterenko 1996, Schanuel 1960s - Add 5th keyInsight: X0*X1 composite polynomial specialization trick - Add 5th openQuestion: e^e transcendence Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich harmonic-divergence-oq-01: add 5 annotations, 7 sections - Add 7 sections covering all 253 lines (header, definitions/basics, log bounds, Theisinger p-adic, sandwich gap/convergence rate, rational exclusion, documented Gamma/Zeta connections) - Add 5 annotations: 42-theorem overview and open status of γ irrationality, sandwich gap explicit convergence rate, Theisinger 2-adic valuation argument, systematic rational exclusion with 3/5 noted as unreachable by basic bounds, documented Gamma/Zeta connections excluded from >32GB build - Expand historicalContext was already good; keyInsights already 4 (no changes needed to overview sections) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * chore(audit): cycle 50 tracker — cantor-diagonalization-oq-02-oq-03-oq-02 audited clean (#9516) New proof detected (Fodor's Pressing-Down Lemma). Gallery entry exists as untracked files on disk; Lean file is on feature/researcher-7 (PR #9500). Meta.json claims match Lean file: 1 sorry (diagInter_isUnbounded) confirmed. Script false-positive: "sorry mismatch" because Lean file not on main yet. Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich 2 proofs: derangements-convergence, lagrange-theorem-oq-01 (#9515) * Enrich derangements-convergence: 5 annotations, 6 sections, expanded history Adds full annotation coverage and deepens all metadata sections for the Derangements Converge to 1/e gallery entry (Wiedijk #88). Annotations added (5): - ann-derang-conv-identity: D(n)=n!·altFactPartialSum strong induction bridge (lines 56-75) - ann-derang-conv-tsum: Linking e⁻¹ to alternating series via NormedSpace.exp_eq_tsum (lines 86-116) - ann-derang-conv-nonneg: Parity-splitting induction for alternating series bounds (lines 120-208) - ann-derang-conv-tail: Passing finite bounds to infinite tail via tendsto limits (lines 210-242) - ann-derang-conv-main: Composing the full convergence proof chain (lines 246-283) Meta enrichments: - 6 sections covering all 284 lines - 5th keyInsight: tsum_eq_partial_sum_add_tail as technical bridge - Expanded historicalContext: Montmort 1708, Euler 1751, Leibniz alternating series 1682, probabilistic interpretation, Wiedijk #88 significance - 4 crossReferences: derangements-oq-03-oq-02 (extends), derangements (related), e-transcendental (related), prob-method-expectation (related) - Expanded openQuestions: D_k(n) convergence rate, D(n)=round(n!/e) integer identity Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich lagrange-theorem-oq-01: 5 annotations, 6 sections, Sylow history Adds full annotation coverage and deepens all metadata sections for the Sylow Theorems as Partial Converse to Lagrange gallery entry. Annotations added (5): - ann-lagrange-oq01-lagrange: Lagrange as card_subgroup_dvd_card delegation (lines 34-44) - ann-lagrange-oq01-existence: First Sylow theorem and p-adic multiplicity (lines 56-67) - ann-lagrange-oq01-conjugacy: Second Sylow theorem via MulAut.conj (lines 79-82) - ann-lagrange-oq01-counting: Third Sylow theorem n_p ≡ 1 mod p via orbit counting (lines 94-101) - ann-lagrange-oq01-converse: Partial converse to Lagrange + Cauchy's theorem (lines 114-123) Meta enrichments: - 6 sections covering all 141 lines in 5 parts - 5th keyInsight: n_p ≡ 1 mod p constraints groups of order pq classification - Expanded historicalContext: Lagrange 1771, Cauchy 1845, Sylow 1872 (denied university post!), A₄ counterexample, Feit-Thompson 1963, classification program - 3 crossReferences: lagrange-theorem (extends), burnside-lemma (related, orbit-counting in Sylow III proof), cauchy-schwarz (related, Cauchy namesake) - Expanded openQuestions: pq classification, A₄ subgroup 6, Hall's theorem Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich derangements-oq-02-oq-02: 5 annotations, 5 sections, Burnside history Adds full annotation coverage and deepens all metadata sections for the Expected Fixed Points of a Random Permutation gallery entry. Annotations added (5): - ann-derang-oq02-oq02-concrete: native_decide concrete verifications (lines 51-89) - ann-derang-oq02-oq02-orbit-stab: Orbit-stabilizer (n-1)! fixing lemma (lines 103-138) - ann-derang-oq02-oq02-burnside: Burnside's lemma 3-rewrite proof (lines 158-177) - ann-derang-oq02-oq02-double-counting: sum_fiberwise weighted identity (lines 200-227) - ann-derang-oq02-oq02-summary: Generating function G_n'(1)=G_n(1)=n! (lines 230-248) Meta enrichments: - 5 sections covering all 250 lines - 5th keyInsight: the original sorry was resolved using card_perms_with_kfixed from parent, enabling the step1 fiber rewriting - Expanded historicalContext: Burnside-Cauchy-Frobenius attribution dispute (Burnside himself credited Frobenius), linearity of expectation proof of E[#fixed]=1 - 4 crossReferences: derangements-oq-02 (extends), derangements (related), burnside-lemma (uses), lagrange-theorem-oq-01 (related, orbit-stabilizer) - Expanded openQuestions: higher moments, generating function, Poisson(1) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich chebyshev-bounds: add 5 annotations, 6 sections, expand keyInsights - Add 6 sections covering all 445 lines (header, theta upper bound, central binomial + prime divisibility, power bound + pi connection, Bertrand lower bounds, binomial lower bound + log corollary) - Add 5 annotations: Chebyshev 1852 historical overview, theta(n) <= n*log(4) via primorial + log_prod, prime_in_interval_dvd_centralBinom core divisibility lemma, pi(n) >= log2(n) telescoping Bertrand proof, central binomial sandwich 4^n/(2n+1) <= C(2n,n) <= 4^n - Expand keyInsights to 5: add sandwich bound proof details with choose_le_middle and primorial_le_4_pow explanation Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * chore: sync research listings and data (#9519) Automated sync of research iteration counts and problem listings. Co-authored-by: Claude <noreply@anthropic.com> * Enrich algebraic-numbers-countable: 5 annotations, 7 sections, expand historical context - 7 sections covering all 254 lines (header, core results, bounded degree, exact degree, stratification, degree 1/monotone, cardinality/filtration) - 5 annotations: Cantor 1874 overview, one-line proof via Algebraic.countable, degree stratification + alternative proof, bounded vs exact degree filtration structure, cardinal paradox (algebraic ≅ ℚ ≅ ℕ despite proper containment) - Expanded historicalContext: Cantor's 'height' function approach, Liouville 1844 vs Cantor cardinality argument, pre-1874 lack of known transcendentals - Added 5th keyInsight: degree 1 = ℚ via isAlgebraic_algebraMap connecting stratification to denumerability Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Enrich angle-trisection-oq-04: 5 annotations, 6 sections, expand history - 6 sections covering all 599 lines (header, core definitions + cos20, strict hierarchy proof, tool degrees + Mohr-Mascheroni, 2-3 number theory + Pierpont, Poncelet-Steiner + polygon classification) - 5 annotations: five-level tool hierarchy overview, three_not_dvd_power_of_two arithmetic core, Mohr-Mascheroni/Poncelet-Steiner by rfl, 2-3 number closure + exclusion pattern, Pierpont primes as Fermat prime generalization - Expanded historicalContext: ancient neusis (Archimedes, Nicomedes), Mohr-Mascheroni 1672/1797, Poncelet-Steiner 1833, Gleason 1988 algebraic characterization, Huzita-Justin 1989/1991 - Added 5th keyInsight: eleven_not_pierpont/eleven_not_two_three via prime divisibility pattern Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Enriches 5 gallery proof entries with annotations, sections, and expanded metadata:
Labels
enrichment
🤖 Generated with Claude Code