feat(HasseWeil): isogeny symmetry over ℚ — universalDualWitness_of_charZero axiom-clean (dual isogeny over the base field, Silverman III.6.1) - #416
Open
CBirkbeck wants to merge 80 commits into
Open
Conversation
…lueprint/scripts (from origin)
… standalone repo Brings the project's dev ticket system up to date in the monorepo (the .lean tree was already byte-identical from the initial import; only process docs needed porting). Additive — preserves all import-only context (cleanup-state/, overview/, renames.jsonl, expert-review/2026-06-04): - plan-iv1.md + tickets-iv1.md — the IV.1 formal-group program board (BRIDGE-003/Wall A/P all DONE axiom-clean; remaining: III.1.5 pair + the off-path leaves) - plan-silverman.md + tickets-silverman.md — the Silverman continuation plan - triage/ — the sorry triage (remaining-sorries.md, openlemma-trio.md) - develop/ — the /develop decompositions (isogeny-foundation, tate-module, formal-group-bridge, dual-completion) - expert-review/2026-06-10/ — round-24 reviewer brief/reply/integration - b2_log.jsonl (superset) + learnings.jsonl (UNION with the import's 7 unique entries — both preserved) No .lean changes (code already present and identical on dev/hasse-weil). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…tative table NEW HasseWeil/EC/IsogenyAG/IsogenyClassLabel.lean (0 sorries, builds green in the HasseWeil target). Reduces "assign a curve its LMFDB isogeny-class letter" to an isogeny-membership check against a GIVEN representative table — no enumeration / Shafarevich needed (the table + ordering are taken as input, exactly as the conductor is): - IsogenyClassTable F: the given LMFDB table for a fixed conductor (card, reps : Fin card → EllipticCurveOver F, letter : Fin card → String, pairwise_not_isogenous). - index / classLetter / lmfdbLabel: E's label = the letter of the unique rep E is isogenous to. - index_unique + classLetter_eq_of_isogenous: well-definedness = the class letter is an isogeny INVARIANT — gated on UniversalDualWitness F (isogeny symmetry / the dual, Silverman III.6.1), reusing the existing IsogenyClass gate. NEXT: discharge that gate properly (the dual isogeny). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…the base field (isogeny symmetry) /develop output for discharging UniversalDualWitness over a char-0 field (= symmetry of IsIsogenous = the LMFDB-label gate). Source-faithful to Silverman III.6.1 + III.4.10-4.12 (read this session) + the project dual-machinery audit + a mathlib descent search. Plan (plan-dual-descent.md) + ticket board (tickets-dual-descent.md, 4 phases): - DUAL-Q1: Galois action on K̄(E_K̄)=K̄⊗_F F(E), fixed field = F(E) (finite-Galois level). - DUAL-Q2 (CRUX, API gap): descent of a curve morphism along finite Galois L/F — new AG infra, only partially in mathlib (FaithfullyFlat/Descent + finite-Galois fixedField exist; CurveMap descent does not). May warrant /expert-review. - DUAL-Q3: φ̂_K̄ Galois-equivariant from uniqueness (compose_right_cancel / II.2.3). - DUAL-Q4: assemble → universalDualWitness_of_charZero → IsIsogenous.symm → discharge the IsogenyClassLabel gate. Route is Silverman's own (build φ̂ over K̄ via existing machinery — char 0 ⟹ separable — then descend to F by uniqueness + Galois-invariance, at a FINITE Galois level to dodge the infinite Gal(K̄/F)). HAVE: K̄ dual (exists_dual_of_pullbackEvaluation_general), base-change (baseChangeIsogeny+CoordHom), factorThrough, hbase/reflects_ordAtInfty, the tensor identification functionField_baseChange_tensorEquiv. NEW: the descent (Q2). NEW HasseWeil/EC/IsogenyAG/DualDescent.lean scaffold: headline universalDualWitness_of_charZero (sorry, elaborates) + isIsogenous_symm_charZero (derives symmetry from it — gate-discharge interface confirmed sound). Root build GREEN (8822 jobs); the one sorry is the headline (allowed on dev). Q1-Q3 internals fill across tickets; Q2's deep sub-leaves may stay sorry/REVIEW-PENDING. HONEST: this is the largest remaining piece, with Q2 a genuine partially-mathlib-lacking descent development — the proper path to unconditional isogeny symmetry (hence unconditional LMFDB isogeny-class labels), not a quick win. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… down to 2 documented sorries The whole base-change-to-K̄ + Galois-descend route (Silverman III.6.1) built in HasseWeil/EC/IsogenyAG/DualDescent.lean (+471 lines). All of DUAL-Q1..Q4's structure is proven and axiom-clean; the deep inputs are isolated to EXACTLY 2 named sorries: - DUAL-Q1: galActFunctionField (Gal(L/F) action on F(C_L) via σ⊗id through functionField_baseChange_tensorEquiv) + _id/_trans + galActFunctionField_fixes_baseChange — all axiom-clean. mem_range_functionField_baseChange_iff_fixed: easy direction proved, the → (Galois descent of Frac(L⊗_F F[C])) is sorry #1. - DUAL-Q2 (the predicted crux — came in CLEAN modulo Q1): descendPullback / descendIsogeny (CoordHom-free), round-trip functionFieldMap_comp_descendPullback, basepoint descend_basepoint — the CurveMap-from-restricted-pullback is COMPLETE modulo Q1. - DUAL-Q3: galEquivariant_of_compose (equivariance from φ*∘φ̂*=[m]* + injectivity) — axiom-clean. - DUAL-Q4: hasDualWitness_of_compose (axiom-clean); universalDualWitness_of_charZero + isIsogenous_symm_charZero reduce to the assembled chain rationalDualCompose_of_charZero = sorry #2. IsogenyClassLabel.lean: the LMFDB gate DISCHARGED UNGATED over char 0 — index_unique_charZero / index_eq_charZero / classLetter_eq_of_isogenous_charZero (drop the UniversalDualWitness hypothesis), 0 sorries in that file. Verified (worker + this commit): lake build HasseWeil GREEN (8822 jobs); sacred hasse_bound_unconditional still [propext, Classical.choice, Quot.sound]; all Q1-Q4 structural decls axiom-clean, the 2 residuals carry sorryAx as expected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…-clean mem_range_functionField_baseChange_iff_fixed (both directions now) — a Gal(L/F)-invariant element of F(C_L) descends to F(C). [propext, Classical.choice, Quot.sound], no sorryAx. The → direction (the deep Q1 leaf) proved by a SELF-CONTAINED tensor-level Galois descent — mathlib v4.31 has NO base-change-of-IsGalois lemma, so it was built directly: - ring/free-module descent: Module.Basis.baseChange + baseChange_repr_tmul + IsGalois.mem_range_algebraMap_iff_fixed (a coefficient is Gal(L/F)-fixed iff in range(algebraMap F L)); F[C] is F-free so the L-basis 1⊗bᵢ + coordinatewise σ-action apply. - fraction-field lift: write y = n/den, make den Gal-fixed via the norm ∏_σ (σ⊗id)den (Equiv.prod_comp (mulLeft τ)), then both n and den fixed ⟹ descend through functionField_baseChange_tensorEquiv. New private helpers: ringAct, repr_congr_apply, tensor_fixed_mem_range, congr_alg_eq_lin, tensor_ringAct_fixed_mem_range, galActFrac_algebraMap, norm_fixed, the_lift (~140 LOC). These descent lemmas (free-module Galois descent + the norm-fix trick) are reusable for the remaining DUAL-Q4 chain. Build GREEN (8822 jobs). DualDescent.lean now down to 1 sorry (rationalDualCompose_of_charZero, DUAL-Q4). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…l reduces to Im([m]*) ⊆ Im(φ*) rationalDualCompose_of_charZero + universalDualWitness_of_charZero now assemble over a single named residual rationalRangeIncl_of_separable (Im([deg φ]*) ⊆ Im(φ*) over F for separable φ — the genuine Silverman III.6.1 range-inclusion core). Everything else PROVEN axiom-clean: - isSeparable_of_charZero (char 0 ⟹ φ separable, via isSeparable_iff_algebra_isSeparable + isAlgebraic_toAlgebra + Algebra.IsSeparable.of_integral) - rationalDualCompose_of_hasMulByIntDualWitness (the formal payoff: F-rational [n]-witness ⟹ (mulByIntDual w).compose φ = [n], via mulByIntDual_comp_pullback + ext_toCurveMap) - hasMulByIntDualWitness_of_rangeIncl (basepoint leaf from the range inclusion alone, via hbase_of_reflects + mulByIntBasepoint_holds + reflects_ordAtInfty) The residual's honest sub-gaps (worker-identified): (1) general TWO-CURVE base-change of an isogeny — baseChangeIsogeny is endomorphism-only, the ticket's "HAVE" was wrong for φ:E₁→E₂; (2) field of definition over AlgebraicClosure F → finite Galois L/F (deep); (3) full base-changed-pullback equivariance on all of F(C_L). NEXT (cleaner route, sidesteps (2)): descend the PREIMAGE ELEMENT via the now-proven DUAL-Q1 (mem_range_functionField_baseChange_iff_fixed) — the K̄ range inclusion + Q1 elementwise descent needs only (1), not the isogeny field-of-definition. Build GREEN (8822 jobs); sacred hasse_bound_unconditional axiom-clean; universalDualWitness_of_charZero carries sorryAx via the one residual (expected). Imports += TwistedFactorization (EC↔Algebra separability bridge; no cycle). New helpers: isSeparable_of_charZero, rationalDualCompose_of_hasMulByIntDualWitness, + 3 private. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ata_of_separable The whole isogeny-symmetry / dual-over-base-field program now rests on a single named residual. Elementwise Galois descent glue PROVEN axiom-clean (exploiting the now-proven DUAL-Q1): - DescentData / SomeDescentData (the finite-Galois descent interface). - rangeIncl_of_descentData: from descent data over finite Galois L/F, derive Im([m]*) ⊆ Im(φ*) over F by descending the PREIMAGE ELEMENT (ĝ ∈ K̄(E₂), Gal-fixed by uniqueness ⟹ ĝ ∈ F(E₂) via DUAL-Q1 mem_range_functionField_baseChange_iff_fixed) + functionFieldMap naturality & injectivity. Axiom-clean. - rationalRangeIncl_of_separable now a thin proof = exists_descentData_of_separable + rangeIncl_of_descentData. THE ONE RESIDUAL (REVIEW-PENDING): exists_descentData_of_separable — for separable φ over F, ∃ finite Galois L/F with the full descent data (two-curve base-change ψ_L + descended K̄-dual range inclusion + equivariance + naturality). = the union of the two genuine missing-infra gaps: (1) two-curve base-change of an isogeny (baseChangeIsogeny is endomorphism-only; function-field base-change goes through FractionRing(L⊗CR)); (2) field of definition (morphism over AlgebraicClosure F defined over a finite Galois L — no bridge from scheme-theoretic SpreadingOut to the elementary function-field framework). Build GREEN (8822 jobs); sacred hasse_bound_unconditional axiom-clean; universalDualWitness_of_charZero carries sorryAx via this one residual only. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… on ONE leaf (two-curve base-change) MOVE 1 (the feared field-of-definition gap) PROVEN axiom-clean and reusable: - instIsGalois_algebraicClosure: char 0 ⟹ K̄/F Galois (IsAlgClosure.normal + .separable). - galFixed_of_galFixed_top: Gal(K̄/F)-fixed ⟹ Gal(L/F)-fixed (AlgEquiv.restrictNormalHom_surjective + restrictNormal_commutes). - exists_finiteGalois_fieldOfDefinition: a finite set of K̄-elements lies in a finite Galois L ⊆ K̄ (FiniteGaloisIntermediateField.adjoin) — the single-element field-of-definition, sidestepping the hard isogeny field-of-definition. MOVE 2 packaging: DescentDataOverKbar + someDescentData_of_overKbar (universe-correct) — proven; exists_descentData_of_separable is now a PROVEN thin assembly over the one leaf. THE SINGLE REMAINING LEAF (REVIEW-PENDING): descentData_over_kbar_intermediate — the two-curve base-change of a separable isogeny (the L-linear ψ_L over a finite Galois L ⊆ K̄). Obstacle: a general EC.Isogeny carries no CoordHom (separate data; baseChangeIsogeny is endo-only), so the base-change of φ* must construct/use a CoordHom for the separable φ. Standard project-area base-change infra — the most tractable of the program's three deep pieces; the other two (function-field Galois descent = DUAL-Q1, and field-of-definition = MOVE 1) are now BOTH proven. So: universalDualWitness_of_charZero (⟹ isogeny symmetry ⟹ the ungated LMFDB label gate) is proven modulo exactly one base-change leaf. Build GREEN (8822 jobs); sacred hasse_bound_unconditional axiom-clean; all MOVE 1/2 decls axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…sts on the two-curve K̄-dual alone The whole dual-over-ℚ / isogeny-symmetry program now reduces to ONE leaf: twoCurveKbarRangeIncl_descended (the two-curve K̄-dual range inclusion Im([deg φ]_L*) ⊆ Im(ψ_L)). The three feared deep pieces are ALL now proven (DUAL-Q1 function-field Galois descent, field-of-definition MOVE 1, and now two-curve base-change + equivariance): TwoCurveBaseChange namespace (CoordHom-FREE, all axiom-clean): - bcIsog: two-curve base-change φ_L : E₁_L → E₂_L over a general finite L via EC.Isogeny.ofEquation on bcXgen/bcYgen (= functionFieldMap of φ's generator pullbacks) — no CoordHom, no IsAlgClosed. Inputs bc_equation (Affine.Equation.map ∘ generic_equation), bc_ord (exists_pos_ramificationIdx_at_infinity transported), bcXgen_transcendental. - NEW ordAtInfty_eq_zero_of_isAlgebraic_constants (removes IsAlgClosed from transcendence — minpoly/ultrametric: algebraic over the constant field ⟹ ord 0). - psiL := bcIsog.pullback; psiL_nat / mPbL_nat (naturality, algHom_ext_x_y_gen2), psiL_injective. - psiL_galEquivariant (DUAL-Q3, fully proven): equivariance on ALL of F(E₂_L), via galActFunctionField_algebraMap_L (σ-semilinearity) + ringHom_ext_baseL reducing to L-constants + x_gen/y_gen Galois-fixed images. THE SINGLE REMAINING LEAF (REVIEW-PENDING): twoCurveKbarRangeIncl_descended — needs the TWO-CURVE K̄-dual (DualGaloisData/the III.4.10c fixed-field equality Im(φ*)=Fix(ker φ) for φ_K̄ : E₁_K̄ → E₂_K̄). The project's K̄-dual machinery (exists_dual_of_pullbackEvaluation_general, KernelCountGeneral/GenericCovarianceGeneral/WallCascade) is ENDOMORPHISM-ONLY; generalizing it to two curves is the irreducible remaining infrastructure (a major on-track sub-development). The factorization downstream (CurveMap.factorThroughPullback) is already axiom-clean. universalDualWitness_of_charZero (⟹ isogeny symmetry ⟹ ungated LMFDB label gate) proven modulo this one leaf. Build GREEN (8822 jobs); sacred hasse_bound_unconditional axiom-clean. +558 LOC. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…10/4.11) — dual rests on the two-curve generic-point covariance alone
Generalizes the project's endomorphism-only Galois fixed-field machinery to a
genuine TWO-curve isogeny φ : E₁ → E₂, the shape Silverman III.4.10/4.11 actually
uses. This disproves the codebase's standing "endo-only" framing: every step of
the fixed-field argument is about the SOURCE curve (ker φ ⊆ E₁.Point acting on
K(E₁) by translation; the only cross-curve object is φ.pullback : K(E₂) → K(E₁)).
New files, both axiom-clean, 0 sorry:
- TwoCurveFixedField.lean (~290 LOC): the full fixed-field equality
Im(φ*) = Fix(ker φ) two-curve — algHom_ext_x_y_gen_twoCurve,
translate_pullback_invariance_of_xy_twoCurve, isAlgebraic/finiteDimensional/
degree_pos_twoCurve, kernelMulSemiringAction_twoCurve (scoped),
finite_kernel_of_hcov_twoCurve, pullback_fieldRange_{le,eq}_fixedField_twoCurve,
finrank_pullback_fieldRange_eq_degree_twoCurve, fixedField_hfix_twoCurve.
- TwoCurveDualRange.lean (~120 LOC): the K̄-dual range inclusion
Im([deg φ]*) ⊆ Im(φ*) two-curve — rangeIncl_mulByInt_le_fixed_twoCurve
(easy inclusion via Lagrange ker φ ⊆ E₁[deg φ]) + mulByInt_deg_rangeIncl_twoCurve.
DualDescent.lean: wires the two-curve range inclusion into the descent chain.
THE SINGLE REMAINING SORRY: twoCurveGeometricDualData (DualDescent.lean:1590) —
the genuinely cross-curve generic-point covariance (mapTranslateGenericPoint_of_
pullbackEvaluation + the kernel torsor, ~500 LOC) generalized to two curves, plus
the h_deg / h_mPbL base-change plumbing. This is Silverman III.4.10b (τ_T* fixes
φ*K̄(E₂) since φ∘τ_T = φ for T ∈ ker φ) — geometrically TRIVIAL (φ is a group hom)
but the project's standing hgcomm/PullbackEvaluation formalization-deep piece, in
two-curve form. Everything else in the DUAL-DESCENT program (DUAL-Q1 function-field
Galois descent, the field-of-definition MOVE 1, the two-curve base-change via
ofEquation + equivariance) is PROVEN axiom-clean; universalDualWitness_of_charZero
now carries sorryAx solely via this one leaf.
Build GREEN (8760 jobs). Sacred bound hasse_bound_unconditional untouched
(EC/IsogenyAG/ is downstream of the Hasse bound).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…lverman III.4.10b) New leaf file TwoCurveGenericCovariance.lean (193 LOC, 0 sorry, axiom-clean [propext, Classical.choice, Quot.sound]). Generalizes the project's single-curve covariance to a TWO-CURVE isogeny φ : E₁ → E₂, for the kernel-point case — which is exactly what the dual-descent residual h_xy_family needs. - PE-0 PullbackEvaluation_twoCurve : the two-curve cofinite pullback-evaluation predicate (β.pullback (x_gen W₂) ∈ K(E₁) evaluates at P ∈ E₁ to the x-coord of β.toAddMonoidHom P ∈ E₂; bad = finite excluded set). - PE-2 xy_family_of_pullbackEvaluation_twoCurve : Silverman III.4.10b verbatim — for k ∈ ker β, τ_k* fixes β.pullback (x_gen W₂) and (y_gen W₂). Proved DIRECTLY via the single-curve separation eq_of_evaluatesTo_cofinite on K(E₁) (both sides live in K(E₁)): at a good P, β(P+k) = βP + βk = βP since βk = 0, so both evaluate to the same x'(βP). This is the kernel-case of the covariance — the ~600-LOC full generic engine is NOT needed (no image-density / two-curve separation), because both functions live on the SOURCE curve. This is the reusable engine for the DualDescent residual twoCurveGeometricDualData's h_xy_family field. Remaining residual = the βL realization (CoordHom-free geometric point map of a general affine-kernel isogeny + #ker=deg) — recorded in .mathlib-quality/decompose-twoCurveGeometricDualData.md. Full HasseWeil build green (8824 jobs); sacred bound hasse_bound_unconditional untouched (leaf file, no downstream of the Hasse bound). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…wo-curve isogeny (Silverman III.4.8 substrate) New leaf file TwoCurvePointImage.lean (542 LOC, 19 decls, 0 sorry, axiom-clean [propext, Classical.choice, Quot.sound]; build green 8747 jobs). Builds the CoordHom-FREE geometric realization of a separable two-curve isogeny's point map, the substrate for the dual-descent residual twoCurveGeometricDualData. The affine-kernel bcIsog (ofEquation) has NO CoordHom, so the project's shipped III.4.8 / norm / Pic⁰ pushforward machinery (all CoordHom-gated) does not apply. This file recovers the realization CoordHom-free via place restriction, in two complementary axiom-clean routes: - Route I (place-equality): twoCurve_evaluatesTo_of_comap_eq — if P's place restricts along φ.pullback to Q's place, then φ.pullback f evaluates at P to f's value at Q (an EXACT valuation identity — Silverman's "free" functoriality step τ_T*φ* = (φ∘τ_T)* recovered at the place level). Assembled via TwoCurvePlaceData + pullbackEvaluation_twoCurve_of_placeData. - Route II (constructive, place-equality-FREE — bypasses the deep place→point dictionary / e=1 wall): residue values exist over F̄ (exists_evaluatesTo_of_pointValuation_le_one), satisfy E₂'s Weierstrass equation (twoCurve_equation_of_evaluatesTo), hence form a nonsingular E₂ point (nonsingular_of_evaluatesTo_generators), reducing the whole PullbackEvaluation_twoCurve coherence to a single tie (stored map = residue point) via pullbackEvaluation_twoCurve_of_residue_agreement, with bad = the finite pole locus twoCurvePoleLocus (twoCurvePoleLocus_finite, Silverman II.1.2). - placeRestrictionIsogeny: packages a point map into the Basic-world HasseWeil.Isogeny, carrying the group-hom property as a NAMED HYPOTHESIS hgrouphom (NOT a sorry). NET: PE-1a (the point-image realization + PullbackEvaluation coherence) is now constructively discharged. The SOLE remaining geometric input is PE-1b — the group-homomorphism property (Silverman III.4.8, CoordHom-free) — the project's standing geometric-realization wall (done elsewhere only for [n]/1−π via explicit formulas). Decomposition + verbatim Silverman anchors in .mathlib-quality/decompose-twoCurveGeometricDualData.md. Sacred bound hasse_bound_unconditional untouched (leaf file). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… divisor pushforward (PE-1 reduced to exactly III.4.8 group-hom) TwoCurvePointImage.lean (+206 LOC, 0 sorry, build green 8747): TASK A complete — the concrete CoordHom-free total point map and the βL realization: - placeRestrictionPointMap φ : W₁.Point → W₂.Point (O ↦ O; affine P off the pole locus ↦ its residue-value point ⟨cx,cy⟩ from exists_evaluatesTo_…; pole-locus/ kernel ↦ O), with placeRestrictionResidueX/Y + evaluatesTo_… support. - placeRestrictionPointMap_residue_agreement : the stored map IS the residue construction (so the PullbackEvaluation residue-agreement is rfl). - placeRestrictionRealization φ (hgrouphom) : HasseWeil.Isogeny W₁ W₂ — the βL realization, carrying ONLY the group-hom property hgrouphom as a hypothesis. - pullbackEvaluation_twoCurve_placeRestrictionRealization : its PullbackEvaluation witness, FREE (bad = twoCurvePoleLocus). NET: the dual-descent point-map realization is reduced to EXACTLY the one classical input — Silverman III.4.8 (group-hom) for placeRestrictionPointMap, CoordHom-free. TwoCurveGroupHom.lean (NEW, 118 LOC, 0 sorry, build green 8748): PE-1b foundation — the CoordHom-FREE Pic⁰ diagram-chase spine, started: - placeRestrictionPlaceImage / placeRestrictionPushforward : the divisor pushforward Div(E₁) →+ Div(E₂) via the CoordHom-free place-image map (Finsupp.mapDomain), the two-curve CoordHom-free analogue of PushforwardDivisor's pushforwardProjectiveDivisor. - degree_placeRestrictionPushforward + placeRestrictionPushforwardDegZero : degree preservation + restriction to Div⁰. Remaining for PE-1b (hgrouphom): norm–conorm principal-preservation (CoordHom-free) + the AddHomProperty_of_AFInputs Pic⁰ diagram chase with this pushforward. Both axiom-clean (0 sorry over axiom-clean imports). Sacred bound untouched. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ymmetry reduced to ONE Prop (Silverman II.3.6 norm–conorm)
TwoCurveGroupHom.lean (now 0 sorry, axiom-clean, build green 8748): the CoordHom-FREE
Silverman III.4.8 group-hom for placeRestrictionPointMap, faithfully mirroring
AddHomProperty_of_picZero_witnesses (HomProperty.lean:165) with the CoordHom-free
place-image map / pushforward replacing toPointMap cd / pushforwardProjectiveDivisor:
- placeRestrictionPushforward_kappaDivisor : the divisor square φ_∗((P)−(O)) = (φP)−(O).
- PlaceRestrictionPreservesPrincipal φ : Prop — the SINGLE deep input, isolated.
- placeRestrictionPushforwardPicZero + picZeroOfPoint_… : descent to Pic⁰ + the Pic⁰ square.
- placeRestrictionPointMap_add_of_picZero_witnesses : the full diagram chase (parametric).
- placeRestrictionPointMap_add_of_preservesPrincipal : curve-side witnesses (h_van, h_inj)
discharged via Curves.afInputs_allChar, leaving ONLY PlaceRestrictionPreservesPrincipal.
- placeRestrictionRealizationOfPreservesPrincipal : the realized geometric HasseWeil.Isogeny
directly from the one Prop (PullbackEvaluation coherence from the TASK-A theorem).
NET: the ENTIRE char-0 isogeny-symmetry goal (UniversalDualWitness → IsIsogenous.symm) is
now reduced to the single classical statement
PlaceRestrictionPreservesPrincipal φ :
∀ D principal on E₁, placeRestrictionPushforward φ D is principal on E₂
= Silverman II.3.6/II.3.7 (the place-restriction pushforward preserves principal divisors,
norm–conorm), CoordHom-free. Honest assessment (recorded in the decompose doc): this is the
project's standing geometric-realization wall — the CoordHom-gated relNorm route
(PushforwardDivisor:1096) needs an affine coordinate-ring extension that a genuine isogeny
lacks; a CoordHom-free norm–conorm is multi-day new infrastructure.
Sacred bound untouched.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…pal reduced to ONE per-place leaf
CoordHom-free norm-conorm (Silverman II.3.6/II.3.7) for the place-restriction
pushforward. Structural chain sorry-free:
- conorm N_φ = field norm Algebra.norm_{K(E₁)/φ*K(E₂)} : K(E₁) →* K(E₂)
- f = u/v reduction (placeRestrictionPushforward_projectiveDivisorOf_of_algebraMap)
- algebraMap-case assembly (affine via the leaf, infinity via degree)
- div(N_φ f) = placeRestrictionPushforward φ (div f) (placeRestrictionPushforward_projectiveDivisorOf)
- placeRestrictionPreservesPrincipal_of_finite_separable (THE WALL, mod hfin/hsep)
- RHS fibre-sum reduction (placeRestrictionPushforward_apply_affine)
Single remaining sorry: twoCurve_ord_conorm_eq_sum_fiber — the per-affine-place
identity ord_Q(N_φ(algebraMap w)) = Σ_{φP=Q} ord_P(algebraMap w) (e=1 by III.4.10c),
the integral-closure-over-B re-derivation of count_relNorm_eq_sum_fiber.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…one + leaf route map - isogeny_finiteDimensional_twoCurve: K(E₁)/φ*K(E₂) finite-dimensional for ANY two-curve isogeny (trdeg additivity, both legs trdeg 1), axiom-clean. - placeRestrictionPreservesPrincipal_of_separable: the wall keyed on hsep ALONE (hfin auto-derived) — the form to wire at the twoCurveGeometricDualData call site. - placeRestrictionPushforward_apply_affine: RHS fibre-sum reduction (structural). - Detailed route map on the single deep leaf (localized-D template in KernelCountGeneral, the weighted-count gap, the bad-Q gap). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Port `card_kernel_eq_degree_of_separable` (KernelCountGeneral) to a two-curve `β : Isogeny W₁ W₂` over an algebraically closed field, carrying only the cofinite two-curve pullback-evaluation coherence `PullbackEvaluation_twoCurve`. New file `HasseWeil/EC/IsogenyKernelTwoCurve.lean`, all axiom-clean ([propext, Classical.choice, Quot.sound], no sorryAx): - `card_kernel_eq_degree_twoCurve` — the headline. - `hcov_of_pullbackEvaluation_twoCurve` — full kernel-translation covariance from the committed PE-2 `xy_family_of_pullbackEvaluation_twoCurve` + generator extensionality. - `kernelTranslateForwardAut_twoCurve(_injective)` — kernel ↪ Aut(K(E₁)/β*K(E₂)). - `finite_fiber_twoCurve` — two-curve port of `PullbackEvaluation.finite_fiber`. ≤ via kernel ↪ Aut + `AlgEquiv.card_le` (finite-dim from `isogeny_finiteDimensional_twoCurve`); ≥ via the already-two-curve `LocalizedDictionary.exists_good_fiber_points`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…(P)=m_Q (Silverman II.3.6, mathlib relNorm_eq_pow_of_isMaximal)
NormConormIntegralClosure.lean (NEW, 168 LOC, builds green, 2 named sorries):
the integral-closure substrate for the CoordHom-free norm–conorm (Silverman II.3.6).
- B := integralClosure(C₂.CoordinateRing, K(C₁)) with instDedekindB / instModuleFiniteB /
instFractionRingB / instTorsionFreeB (T-A1, DONE).
- inertiaDeg_eq_one : over alg-closed F, inertia degree = 1 (via LocalizedDictionary
inertiaDeg_eq_one_of_under_eq, no e=1 needed).
- relNorm_eq_of_under : relNorm_{C₂.CoordinateRing}(P) = m_Q for P over m_Q — the crux
application of mathlib Ideal.relNorm_eq_pow_of_isMaximal (RelNorm.lean:436) + inertiaDeg=1.
(char-0 ⟹ the PerfectField hypothesis is derivable; the decompose pass confirmed this
mathlib lemma EXISTS — no missing API.)
REMAINING (2 named sorries + downstream): coordXFun_mem_B / coordYFun_mem_B (the coordinate
functions of C₁ are integral over C₂.CoordinateRing = land in B; their only poles are at ∞ of
C₁ and the affine kernel, all over ∞ of C₂); then the global-B place dictionary + the
norm-divisor count Σ-over-fiber, then filling twoCurve_ord_conorm_eq_sum_fiber (TwoCurveNormConorm:273).
Salvaged from a worker that died on a transient API error one `.symm` from compiling.
Sacred bound untouched (nothing imports this file yet).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…om-clean)
count_relNorm_eq_sum_fiber_B: for w ∈ B nonzero and a smooth point Q of C₂,
count_{m_Q}(relNorm(span{w})) = Σ_{P over m_Q} count_P(span{w}). Ports
PushforwardDivisor.count_relNorm_eq_sum_fiber over the integral closure B,
using the committed s=1 core relNorm_eq_of_under (wrapped as relNorm_eq_under,
smooth-point-free). All inertia degrees 1; #print axioms = [propext,
Classical.choice, Quot.sound]. Integrality sorries (coordXFun/coordYFun_mem_B)
unchanged.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…f chain (Task 1)
The bare-`HasseWeil.Isogeny` statement of `coordXFun_mem_B`/`coordYFun_mem_B` is
false without a basepoint-regularity hypothesis: x₁,y₁'s only pole (∞ of C₁) must
lie over ∞ of C₂, which is exactly what `EC.Isogeny.pullback_ordAtInfty_nonneg`
controls. Added
hreg : ∀ f, 0 ≤ C₂.ordAtInfty f → 0 ≤ C₁.ordAtInfty (φ.pullback f)
(spelled `OrdAtInftyReg` in NormConormIntegralClosure; inline in TwoCurveNormConorm
where `φ.pullback` is the `HasseWeil.Isogeny` pullback) to:
- `coordXFun_mem_B`, `coordYFun_mem_B`, `coordRing_mem_B`;
- `twoCurve_ord_conorm_eq_sum_fiber` (the deep leaf, :273) and its callers
`placeRestrictionPushforward_projectiveDivisorOf{,_algebraMap}`,
`placeRestrictionPreservesPrincipal_of_{finite_,}separable`.
No external consumer calls the leaf yet (`twoCurveGeometricDualData` is itself an
open `sorry` and routes #ker=deg through `LocalizedDictionary`), so nothing breaks.
Both files build GREEN (sorries-only).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…*_mem_B (Task 2/3) Eliminate the two opaque sorries (`coordXFun_mem_B`, `coordYFun_mem_B`) by reducing integrality of the C₁ coordinate generators to a single PRECISELY-NAMED geometric residual, via the NON-CIRCULAR valuative criterion (mathlib's `IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one` on the Dedekind domain B with fraction field K(C₁)). NEW (axiom-clean): - `mem_B_of_forall_valuation_le_one` : z ∈ B ⟸ v.valuation K(C₁) z ≤ 1 for every height-one prime v of B. Structural, `#print axioms = [propext,Classical.choice, Quot.sound]` (no sorryAx). This is the non-circular core (it does NOT presuppose `coordRingToClosure` = the very integralities — contrast `LocalizedDictionary.pointAt`). - `BPrimeValuationCoordGenLeOne` : the genuine geometric residual = every B-prime valuation is ≤ 1 on x₁,y₁ (i.e. the B-prime's place lies over an affine place of C₂, away from ∞ of C₁ where x₁,y₁ pole). This packages the global-B place dictionary (B-prime ↔ affine point of C₁ over affine C₂) — the project's STANDING WALL. `coordXFun_mem_B`/`coordYFun_mem_B`/`coordRing_mem_B` now take this residual (+ hreg, threaded per Task 1) and are one-liners off `mem_B_of_forall_valuation_le_one`. The file is now SORRY-FREE; the open content is isolated in the named `BPrimeValuationCoordGenLeOne`. No external callers (the leaf `twoCurve_ord_conorm_eq_sum_fiber` is still a sorry and routes #ker=deg through LocalizedDictionary). Builds GREEN. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…er on C₂, DVR, valuation≤1 on base) The structural half of the global-B place dictionary, axiom-clean and non-circular (available before BPrimeValuationCoordGenLeOne): - valuation_algebraMap_coordinateRing_le_one: v ≤ 1 on the C₂.CoordinateRing image - under_ne_bot: a B-prime contracts to a nonzero prime of C₂.CoordinateRing (via Ideal.eq_bot_of_comap_eq_bot, integral extension) - exists_smoothPoint_under: every B-prime lies over the maximal ideal of a smooth point Q of C₂ (the affine-place restriction excluding ∞ of C₂) - valuationSubring_isDVR: the v-adic valuation subring is a DVR (rank-one), the input to rankOne_valuationSubring_le_eq_of_ne_top These sharpen the standing place-classification wall to the single irreducible classification 'an F-trivial DVR of K(C₁) that is not the ∞-place is a point'. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… classification Introduces BPrimePlaceClassification (every B-prime valuation on K(C₁) is a point valuation or the ∞-place — the curve-completeness statement) and the axiom-clean reduction bPrimeValuationCoordGenLeOne_of_classification: the place-dictionary residual follows from the classification + the ∞-exclusion hinf (no B-prime is the ∞-place of C₁). Point case via pointValuation_algebraMap_le_one; ∞ case excluded by hinf. Isolates the genuine wall into two clean hypotheses (curve-completeness + geometric ∞-exclusion, the latter dischargeable at the concrete isogeny level by the ramification-at-∞ pullback formula). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…tion-at-∞) bPrime_valuation_ne_ordAtInfty (axiom-clean): no B-prime valuation equals the ∞-place of C₁, PROVEN from OrdAtInftyReg (hreg). The coordX C₂ image is a base-ring element of B (valuation ≤ 1); were v the ∞-place, ord_∞(φ* coordX₂) ≥ 0 would contradict the ramification-at-∞ formula ord_∞(φ* coordX₂) = e·(-2) < 0 (e ≥ 1 via exists_pos_ramificationIdx_ordAtInfty_ringHom_of_isAlgebraic, algebraicity from finiteness). Plus bPrimeValuationCoordGenLeOne_of_classification_of_reg: the residual follows from BPrimePlaceClassification + hreg alone. NET: the standing place-classification wall is now reduced to the SINGLE genuine content — the curve-completeness classification BPrimePlaceClassification (every F-trivial DVR of K(C₁) is a point or ∞); the geometric ∞-exclusion is discharged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… sharp reduction Records that the residual is now derived from BPrimePlaceClassification + OrdAtInftyReg (bPrimeValuationCoordGenLeOne_of_classification_of_reg), with the ∞-exclusion half discharged — leaving BPrimePlaceClassification (curve completeness) as the only input. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…o lightweight Curves/RankOneDomination The DVR-domination engine (rank-one valuation subring `A ≤ B`, `B ≠ ⊤` ⟹ `A = B`) moves from the heavy char-p `Hasse/L6Witnesses` into a new `Curves/RankOneDomination.lean` depending only on the mathlib ValuationSubring/DiscreteValuationRing/DedekindDomain.Basic API. L6Witnesses re-exports it under the historical name (all V.1.3 domination consumers unchanged), so the curve-completeness place classification in `Curves/NormConormIntegralClosure.lean` can use it without importing the char-p machinery. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…o RankOneDomination Move `Valuation.isEquiv_iff_eq_of_surjective_withZeroInt` (two surjective ℤᵐ⁰ valuations that are IsEquiv are equal) and `Valuation.isEquiv_of_valuationSubring_le` (subring domination ⟹ IsEquiv via LocalSubring maximality) from `Hasse/L6Witnesses` into the lightweight `Curves/RankOneDomination.lean`. L6Witnesses re-exports both under their historical names (all V.1.3 consumers unchanged). These are the value-precise equality engine the curve-completeness place classification needs. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ators Adds the affine-center input `valuation_algebraMap_coordinateRing_C₁_le_one`: a B-prime v with v(x₁) ≤ 1, v(y₁) ≤ 1 is ≤ 1 on the image of every element of C₁.CoordinateRing (mirrors coordRing_mem_integralClosure with O_v in place of the integral closure; F-constants routed through C₂.CoordinateRing where valuation_algebraMap_coordinateRing_le_one applies). Also adds the general `valuationSubring_isDVR_of_surjective_withZeroInt` to RankOneDomination and simplifies valuationSubring_isDVR to use it. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
bPrime_valuation_eq_pointValuation_of_coordGen_le_one: a height-one prime v of B with v ≤ 1 on both
coordinate generators of C₁ IS the point valuation at a smooth point P. Constructs the center ideal
c_v = {a | v(a)<1} (centerIdealOnC₁), proves it nonzero (v nontrivial) and prime (contraction of the
v-adic maximal ideal), hence maximal in the Dedekind domain F[C₁], hence maximalIdealAt P. The local
ring O_P sits inside O_v (a/s with s∉m_P=c_v has v(s)=1), so the rank-one DVR domination engine
rankOne_valuationSubring_le_eq_of_ne_top forces O_{pointValuation P} = O_v, and the two surjective
ℤᵐ⁰-valued valuations are equal. #print axioms: [propext, Classical.choice, Quot.sound], no sorryAx.
Requires [IsIntegrallyClosed C₁.CoordinateRing] (automatic for elliptic curves off char 2,3).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…coeff)
hcountMatch: count_{vP}(span{wB}) = D(affine P) via vP.intValuation wB = exp(-count) +
pointValuation_algebraMap_eq_exp_count, equated through vP.valuation = pointValuation P.
Final bijection still sorry.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…rse-dictionary regularity) For P with φ^*(x_gen₂),φ^*(y_gen₂) ≤ 1 at P, every φ^*(algebraMap c) (c ∈ F[E₂]) is ≤ 1 at P (generator induction; F-constant legs are regular). The E₁-point analogue of valuation_algebraMap_coordinateRing_C₁_le_one, transported through φ^*. Step 1 of the reverse place dictionary (surjectivity). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…P ∉ poleLocus) Reverse-dictionary step 2: every b ∈ B has pointValuation P ≤ 1, since b is integral over F[E₂] whose image lands in the valuation integers pv.integer (generators regular at P), hence b integral over pv.integer ⟹ pv P b ≤ 1 (Valuation.Integers.isIntegral_iff_v_le_one). Prime construction + domination still sorry. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…tionary PROVEN (surjectivity)
For P ∉ poleLocus with a nonzero B-function z vanishing at P, there is a B-prime v with
v.valuation = pointValuation P. Center q = {b : pv P (algMap_B b) < 1} is prime (pv multiplicative),
nonzero (z ∈ q, z ≠ 0), proper; O_v ⊆ O_P via exists_primeCompl_mul_eq_of_integer (d ∉ q ⟹
pv (algMap_B d) = 1), then rank-one DVR domination gives O_v = O_P, i.e. v.valuation = pointValuation P.
The surjectivity wall of the conorm fibre bijection is now CLOSED.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…PROVEN (0 sorries) Final fibre bijection assembled: B-primes over m_Q ↔ support points P with placeRestrictionPlaceImage φ (affine P) = affine Q. - count_relNorm_eq_sum_fiber_B reduces LHS to Σ over B-primes over m_Q; - forward (hpoint) + count match (hcountMatch) + injectivity (valuation determines prime/point) give Σ over primes = Σ over fibre image; - backward surjectivity (exists_bPrime_eq_pointValuation, sum_subset) matches the fibre image to the support-filter sum (support points map back to B-primes over m_Q via Q'=Q from the forward direction). TwoCurveNormConorm.lean is now SORRY-FREE: placeRestrictionPreservesPrincipal_of_separable PROVEN (mod hreg). Silverman II.3.6 CoordHom-free norm-conorm DONE. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…p 1, axiom-clean) For a two-curve EC.Isogeny φ : E₁ → E₂ over [IsAlgClosed F] [CharZero F], prove Im([deg φ]*) ⊆ Im(φ*) (Silverman III.6.1) by assembling the DONE pieces: the place-restriction geometric realization β of φ* (from the norm–conorm preserves-principal wall, discharged via separability alone in char 0), its kernel-translation covariance xy_family (PE-2) and #ker β = deg β (T-B1), fed to the two-curve fixed-field range inclusion mulByInt_deg_rangeIncl_twoCurve. Also: Isogeny.isSeparable_of_charZero_twoCurve (char 0 ⟹ separable for a Basic two-curve HasseWeil.Isogeny). Both axiom-clean. This is the K̄-level input that the dual descent must push down to a finite Galois L. New file HasseWeil/EC/IsogenyAG/TwoCurveKbarRangeIncl.lean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Route A step 1 (tower fact) scaffolding: the F-algebra inclusion towerTensorIncl from a finite intermediate level M ⊆ K̄ to the algebraic-closure tensor level, with its tmul computation rule. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Injectivity via TensorProduct.map_injective_of_flat_flat (val M injective + flatness over the field F), and equivariance: for σ ⊇ τ, the inclusion intertwines σ⊗id with τ⊗id (tensor induction). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…te Galois M exists_finiteGalois_towerTensorIncl_range: any z ∈ K̄ ⊗_F R is the towerTensorIncl image of an element of M ⊗_F R for a finite Galois M ⊆ K̄ (finite-sum decomposition + exists_finiteGalois_fieldOfDefinition on the finitely many scalars). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Move towerTensorIncl + injectivity + Galois-equivariance + the tensor tower fact (exists_finiteGalois_towerTensorIncl_range) into DualDescent so they sit alongside the private finite tensor-descent helpers and exists_finiteGalois_fieldOfDefinition. Remove the standalone TowerDescent.lean (import direction made it unusable for the rewiring). This is MOVE 2: the K̄-direct infinite-Galois descent scaffold. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ebraMap/injective Frac(M ⊗ F[C]) → Frac(K̄ ⊗ F[C]) via IsFractionRing.map of the injective towerTensorIncl; with the algebraMap compatibility (IsLocalization.map_eq) and injectivity (ring hom out of a field). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
fracTowerIncl intertwines galActFrac C M τ with galActFrac C K̄ σ when σ restricts to τ; reduced via div_surjective + galActFrac_algebraMap to the ring-level towerTensorIncl_congr. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
exists_finiteGalois_towerTensorIncl_range₂: a pair z₁,z₂ ∈ K̄⊗R live over a common finite Galois M (scalars of both finite-sum reps in one M). Factor out towerTensorIncl_finset_sum_mem_range. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ation (axiom-clean) mem_range_functionField_baseChange_iff_fixed_kbar: the L=K̄ analogue of the finite mem_range_functionField_baseChange_iff_fixed. A Gal(K̄/F)-fixed element of (C.baseChange K̄).FunctionField descends to F(C). The genuine tower descent: scalars of the tensor-fraction numerator/denominator lie in a finite Galois M (pair tower fact); the fraction y_M is Gal(M/F)-fixed (fracTowerIncl equivariance + injectivity + restrictNormalHom_surjective); the proven finite descent (the_lift + tensor_ringAct_fixed_mem_range) at M writes y_M as 1⊗-/1⊗-, carried upstairs by towerTensorIncl. #print axioms = [propext, Classical.choice, Quot.sound] (NO sorryAx). This is Route A step 1 (the tower fact), the genuinely new lemma. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…e descent The one-step analogue of rangeIncl_of_descentData: from psiK=φ*_K̄, mPbK=[m]*_K̄ (naturalities, psiK Gal(K̄/F)-equivariant + injective) and the K̄-level inclusion Im(mPbK) ⊆ Im(psiK), derive the F-level Im(mPb) ⊆ Im(φ*). Uses the tower fixed-field characterization, bypassing the finite-L geometric realization. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…cent Move ecIsog_mulByInt_deg_rangeIncl_of_charZero (+ ecShell, isSeparable_of_charZero_twoCurve) from the unimported leaf TwoCurveKbarRangeIncl.lean into DualDescent (adding the 5 two-curve imports, no cycle). This makes the fully-proven K̄ inclusion available to the rewiring (rangeIncl_of_descentData_kbar). Axiom-clean ([propext, Classical.choice, Quot.sound]). Delete the now-redundant TwoCurveKbarRangeIncl.lean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…n-poly base-change mPbL_eq_mulByInt_baseChange_kbar: the structural mulByInt base-change identification — mPbL W₁ K̄ = (mulByInt_pullbackAlgHom (W₁_K̄)).restrictScalars. Both K-algebra homs send x_gen ↦ mulByInt_x (W₁_K̄), y_gen ↦ mulByInt_y (W₁_K̄) and fix K̄-constants (ringHom_ext_baseL). Includes char-independent local division-poly base-change lemmas (coordRingMap_algebraMap_Φ/ΨSq_kbar, coordRingMap_mk_ω/ψ_kbar, functionFieldMap_mulByInt_x/y_kbar) — the PencilComapWitnesses versions are finite-field-gated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…om-clean via K̄-direct route Rewire rationalReverseCompose_of_separable through the MOVE 2 K̄-direct route: rationalRangeIncl_kbar produces Im([m]*_F) ⊆ Im(φ*_F) for m = deg of the K̄-base-change, via ecIsog_mulByInt_deg_rangeIncl_of_charZero (hreg = bcIsog.pullback_ordAtInfty_nonneg) + mPbL_eq_mulByInt_baseChange_kbar + rangeIncl_of_descentData_kbar (tower fixed-field char). The general basepoint builder hasMulByIntDualWitness_of_rangeIncl_general handles n = deg(bcIsog) (n is existential downstream). #print axioms universalDualWitness_of_charZero = [propext, Classical.choice, Quot.sound] -- NO sorryAx. THE GOAL. The old finite-L geometric chain (twoCurveGeometricDualData sorry) is now dead code, to be removed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…lines) Delete the superseded finite-L route: TwoCurveKbarRangeInclData, TwoCurveGeometricDualData (the last sorry), twoCurveKbarRangeIncl_descended, descentData_over_kbar_intermediate, exists_descentData_of_separable, rationalRangeIncl_of_separable, hasMulByIntDualWitness_of_rangeIncl. All superseded by the MOVE 2 K̄-direct route. DualDescent.lean is now sorry-FREE; universalDualWitness_of_charZero and isIsogenous_symm_charZero remain axiom-clean ([propext, Classical.choice, Quot.sound]). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…pic #2546) Adds the dev-side ticket T-TATE-GENN (general-N torsion structure via CRT) — the one genuinely-new piece of the #2546 extraction; the rest is already proven on main + tracked as mathlib:pr GitHub tickets. Source files are protected from the fleet (protected-paths.txt). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…q_of_under via global-balance port (char-p separable leaf) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…r-p prep) Relax the infinite-Galois tower-descent / field-of-definition chain in DualDescent.lean from [CharZero F] to [PerfectField F]: instIsGalois_algebraicClosure, exists_finiteGalois_fieldOfDefinition, exists_finiteGalois_towerTensorIncl_range(₂), mem_range_functionField_baseChange_iff_fixed_kbar, rangeIncl_of_descentData_kbar. The only char-0-specific input was IsGalois F (AlgebraicClosure F), which holds for any perfect field (K̄/F separable + normal, both automatic instances). CharZero ⟹ PerfectField, so the char-0 headline still resolves and stays axiom-clean. Also drop the now-vestigial [PerfectField (FractionRing F[E₂])] binders from the five norm-conorm wrappers in TwoCurveNormConorm.lean (CP-1's NormConormIntegralClosure port already made the conorm PerfectField-free). lake build HasseWeil green (8831); universalDualWitness_of_charZero and hasse_bound_unconditional verified still [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…tField (char-p) Generalize the separable K̄-dual reverse-isogeny engine from [CharZero F] to [PerfectField F], threading separability explicitly: * ecIsog_mulByInt_deg_rangeIncl_of_separable — new separable-form of the K̄ range inclusion (drops CharZero, takes hsep : φ.IsSeparable, [IsAlgClosed F] only); the old _of_charZero is kept as a thin wrapper. Threads hsep through placeRestrictionPreservesPrincipal_of_separable (PerfectField-free since CP-1) and the card_kernel = degree leaf (via ecShell_isSeparable_of_isSeparable + Isogeny.isSeparable_of_pullback_eq). * rationalRangeIncl_kbar, rationalReverseCompose_of_separable: CharZero → PerfectField, take hsep; char-0 callers pass isSeparable_of_charZero. Key new math (the genuine sub-lemma): BASE-CHANGE SEPARABILITY of a two-curve isogeny, TwoCurveBaseChange.bcIsog_isSeparable — for any algebraic L/K, bcIsog φ over L is separable when φ is. Proved via the differential transport (OmegaBaseChange.omegaDiffMap): exists_separating_element gives g with D_K(φ*g) ≠ 0 (separable ⟹ Ω[K(E₁)/K(E₂)]=0 ⟹ mapBaseChange surjective ⟹ rank-1 forces a separating generator), and omegaDiffMap_ne_zero carries it to D_L(bcIsog^*(functionFieldMap g)) ≠ 0 (rank-1 nonvanishing: η = c•ω_K ↦ functionFieldMap(c)•ω_L, both nonzero). Imports OmegaBaseChange into DualDescent. lake build HasseWeil green (8831); universalDualWitness_of_charZero and hasse_bound_unconditional verified still [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…try over any perfect field, axiom-clean The perfect-field analogue of the char-0 headline universalDualWitness_of_charZero: every isogeny over a PERFECT field F has an F-rational dual (UniversalDualWitness F). Case on char F: * char 0: universalDualWitness_of_charZero (every isogeny separable). * char p: nonempty_hasDualWitness_of_twisted_separable_witnesses (twisted Frobenius factorization + relative Verschiebung, TwistedFactorization) reduces to dual witnesses for the SEPARABLE isogenies out of Frobenius twists of W₁, each supplied by rationalDualCompose_of_separable (the PerfectField-relaxed, hsep-threaded K̄ engine from CP-2a/CP-2b). Also: rationalDualCompose_of_separable (public separable form of rationalDualCompose_of_charZero) and isIsogenous_symm_perfectField. #print axioms (verified this session): universalDualWitness_of_charZero = [propext, Classical.choice, Quot.sound] universalDualWitness_of_perfectField = [propext, Classical.choice, Quot.sound] hasse_bound_unconditional = [propext, Classical.choice, Quot.sound] All axiom-clean (no sorryAx). lake build HasseWeil green (8831). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…(char-p, incl. finite 𝔽_q) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…int) Self-contained per-project blueprint for the multi-blueprint site, modelled on projects/PadicLFunctions/_blueprint: lakefile path-requires the AINTLIB workspace + patched VersoBlueprint v4.30 + mathlib (pinned, last); toolchain v4.31.0-rc2. Content (HasseWeilBlueprint/Blueprint.lean) nodes the headline Hasse bound with real (lean := …) refs that resolve against the project oleans: - HasseWeil.pointCount - HasseWeil.frobeniusIsog - HasseWeil.WeilPairing.hasse_bound (+ hasse_bound_unconditional) — sorry-free/unconditional Builds (9082 jobs, all refs resolve) + renders html-multi. The *Blueprint modules are siblings of the HasseWeil lib, so the root workspace glob never picks them up.
…ee QF, t²≤4q, √-reduction) + proof sketches
Co-Authored-By: Claude Opus 4.8 (1M context) <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
2 participants
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.
Isogeny symmetry over ℚ — the dual isogeny over the base field (Silverman III.6.1), axiom-clean
This branch discharges
HasseWeil.EC.universalDualWitness_of_charZero— every isogeny over a characteristic-0 field has anF-rational dual — i.e. symmetry ofIsIsogenousover ℚ. This was the project's single largest remaining piece (the dual isogeny over the base field), and it closes the LMFDB isogeny-class label gate over char-0:IsIsogenous/IsogenyClassis now an unconditional equivalence relation over ℚ.Verification (against this branch's base)
Every step was checked against Silverman, The Arithmetic of Elliptic Curves (II.2.6, II.3.6, III.4.8–4.12, III.6.1–6.2), read from source.
Proof arc (≈67 commits)
PlaceRestrictionPreservesPrincipal(Silverman II.3.6) over the integral closureB, on mathlib'sIdeal.relNorm_eq_pow_of_isMaximalx₁-pole is the place at infinity (explicit local coordinates + rank-one DVR domination)Im([deg φ]*) ⊆ Im(φ*)Algebra.TensorProduct.cancelBaseChange) descends the range inclusion K̄→F →HasDualWitness→ the goalNew / key files (under
projects/HasseWeil/)EC/IsogenyAG/DualDescent.lean(the K̄-direct route,section TowerDescent)Curves/NormConormIntegralClosure.lean(integral closureB+ norm–conorm + curve completeness)EC/IsogenyAG/TwoCurveGroupHom.lean(III.4.8),TwoCurveNormConorm.lean(conorm leaf),TwoCurvePointImage.lean(realization)EC/IsogenyKernelTwoCurve.lean(#ker = deg),WeilPairing/TwoCurveGenericCovariance.lean(covariance engine)EC/IsogenyAG/TwoCurveFixedField.lean,TwoCurveDualRange.lean(fixed-field route),Curves/RankOneDomination.lean(relocated DVR domination)Caveat
This is the char-0 headline (
[CharZero F]⟹ separable + perfect, the case that matters for ℚ / LMFDB). Positive characteristic would need thePerfectField-free variant of the conorm crux, which is not built (and not needed here).Integration note (for cleanup)
This branch is 69 ahead of / 161 behind
main—mainhas advanced via daily mathlib bumps + other projects since this branch's base. The proof is verified green + axiom-clean against the branch's base; merging will need a rebase onto currentmain+ repair of any daily-bump fallout (standard cleanup). Nosorry/axiomadded; the three#print axiomsabove are the acceptance gate.🤖 Generated with Claude Code