feat(ModularCurves): Y(N) frontier — [YF-ETALE]★ (Γ(N)-presentation is étale) + T-D8-bridge + T-E9 MASTER wired - #5790
Open
CBirkbeck wants to merge 61 commits into
Open
feat(ModularCurves): Y(N) frontier — [YF-ETALE]★ (Γ(N)-presentation is étale) + T-D8-bridge + T-E9 MASTER wired#5790CBirkbeck wants to merge 61 commits into
CBirkbeck wants to merge 61 commits into
Conversation
…gree_eq — a subdivisor of equal degree is the whole divisor (axiom-clean): the subscheme inclusion is a closed immersion of finite-loc-free equal-rank S-schemes ⟹ iso (general scheme wrapper) ⟹ equal kernels ⟹ equal ideals. The ⊇ divisor-equality tool; rooted (NEW-Y1)
…penness + full ⊇ machinery: comm-algebra + comaximal + general scheme wrapper + [YF-SUBDIV-EQ]); remaining = [YF-⊇]/[YF-⊆] wiring to the taut/sectionsDivisor construction (NEW-Y1)
…ionIdeal (∏ker=⋂ker⊇torsionIdeal via [YF-COMAX]+torsionIdeal_le_ker, IsSubdivisor+degree N²→[YF-SUBDIV-EQ]); public torsionDivisor + torsionDivisor_degree (torsion_rank transported across torsionIdeal_subscheme iso); torsionIdeal_le_ker axiom-CLEAN; divisor chain inherits ONLY boarded Tier-B boxes (torsionπ finite/flat, torsion_rank), zero new sorry; fixed zero_comp_mulByHom collision w/ sibling GammaH (renamed mine→zeroPoint_comp_mulByHom) (NEW-Y1)
…q_top_of_sections_pointwise_ne: two pointwise-distinct sections of a separated ρ have comaximal kernels (sections are closed immersions via of_comp; retraction forces disjoint images; support_ker+disjoint→sup_eq_top). Refactored sectionsDivisor_ideal_eq_torsionIdeal to consume pointwise-ne directly via prod_eq_biInf_of_pairwise_sup_eq_top (cleaner than support-disjoint). Engine clean; chain inherits only boarded Tier-B boxes (NEW-Y1)
…entι_comp_eq (agreementι ≫ a = agreementι ≫ b, via lift_fst/snd + diagonal_fst/snd) + range_agreementι_subset (range ⊆ topological agreement locus). Reusable keystone for the disjointness bridge: for SECTIONS the residue map is forced = retraction-inverse, so topological agreement = morphism agreement = equalizer range, making empty-agreement-scheme ⟹ comaximal (NEW-Y1)
…CLEAN, term-mode) — base-changed sections agreeing at u ⟹ underlying E-points agree (via asSection_val_fst first-projection); sidesteps semireducible-baseChange kabstract friction. Reduces base-changed-combo pointwise-ne to E-point pointwise-ne, the sectionsDivisor_ideal_eq_torsionIdeal input (NEW-Y1)
…_killed (difference of N-killed is N-killed, CLEAN) + base_ne_of_notMem_pointVanishSet consumer (CLEAN, contrapositive giving pointwise-ne from vanish-locus avoidance). Single deep frontier: mem_pointVanishSet_of_base_eq (fibrewise group law: topological point agreement ⟹ difference vanishes) — WIP sorry, fully documented proof strategy (pointToTorsion additivity + E[N] translation automorphism + zero-section residue triviality). All else in [YF-⊇] chain axiom-clean/boarded (NEW-Y1)
…Divisor_ideal_eq_torsionIdeal + comaximality engine + agreement equalizer + scaffolding, all clean/boarded); single frontier localized = mem_pointVanishSet_of_base_eq (fibrewise group law, WIP sorry) w/ 3 documented sub-tickets (E[N] group structure→pointToTorsion additivity, translation automorphism, zero-section residue triviality) (NEW-Y1)
…f_base_eq (topological agreement ⟹ vanish) was FALSE: Galois-conjugate torsion points share a topological image but their nonzero difference vanishes nowhere. Replaced with mem_pointVanishSet_of_residue_eq (residue-field morphism agreement ⟹ vanish, TRUE) + sections_residue_eq_of_base_eq (forced-residue-for-sections: section residue map = retraction-inverse, the section-specific upgrade). Both WIP sorry but CORRECT; the base-changed combos ARE sections so the section route applies (NEW-Y1)
…oncrete proof paths (forced-residue-for-sections via residueFieldMap two-sided-inverse; residue-agreement vanishing via Spec κ(u)→agreement locus) (NEW-Y1)
…velSupset 0-sorry) sections_residue_eq_of_base_eq (forced residue for sections: retraction of a field extension is iso — mono field-hom + split-epi via residueFieldMap_comp, then epi-cancel + residueFieldCongr proof-irrelevance) + mem_pointVanishSet_of_residue_eq (residue agreement ⟹ x−y agrees with 0 over κ(u) via Point.restrict additivity ⟹ E[N]-classifiers agree ⟹ Spec κ(u) factors through the agreement locus = pointVanishSet). New reusable engine leaf base_mem_range_agreementι (AgreementLocusClopen): a map equalizing a,b factors through agreementι (no unramified hyp). [YF-⊇] divisor chain now needs only its boarded Tier-B torsion boxes. (STREAM-YN) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… Sub-lemma A - base_mem_pointVanishSet_of_comp_eq (FullLevelSupset): generalize the residue bridge to an arbitrary morphism m (residue special case now derives from it) — the tool the distinctness argument composes with U.ι. - Moduli/FullLevelClopen.lean (new): restrict_zsmul, Point.asSection_add (term-mode, via the point_add_val_congr_base base-independence + baseChangeEquiv AddEquiv), combo_eq_asSection_restrict (Sub-lemma A: [a]P+[b]Q of taut sections = section of combPoint a b). Foundation for [YF-⊇] over fullLevelOpens. (STREAM-YN) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Over fullLevelOpens, two taut combinations differing mod N are pointwise distinct: agreement at w ⟹ base-changed sections agree over κ(w) (sections_residue_eq_of_base_eq) ⟹ (composed with U.ι, via base_mem_pointVanishSet_of_comp_eq) the nonzero difference combPoint vanishes at v=U.ι(w) ⟹ contradicts v∈fullLevelOpens (combPoint_emod N-periodicity + Fin N×N index match). Plus helpers: asSection_zero, combPoint_sub, zsmul_emod_eq, combPoint_emod, killing, pointVanishSet_congr. (STREAM-YN) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…orry) Over fullLevelOpens the tautological pair is a full-level structure: N² combinations N-killed (smul_N_taut sections) + pairwise pointwise-distinct (combSec_ne_of_diff + Fin(N²)≃Fin N×Fin N via div/mod, divisor-of-small-difference nlinarith) ⟹ sectionsDivisor = torsionIdeal (sectionsDivisor_ideal_eq_torsionIdeal). Plugs directly into isOpenImmersion_levelSpaceΓι_of_taut. Remaining for [YF-ETALE]: [YF-⊆] range levelSpaceΓι ⊆ fullLevelOpens. (STREAM-YN) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… gate isOpenImmersion_levelSpaceΓι_full = isOpenImmersion_levelSpaceΓι_of_taut ∘ [YF-⊆] ∘ [YF-⊇]. YFullRoute.isOpenImmersion_levelSpaceΓι now PROVEN (consumes it); YFullRoute sorries 6→5. [YF-ETALE] etale_fullLevelSpaceStruct now depends ONLY on range_levelSpaceΓι_subset ([YF-⊆], a documented reduced-fibre gate: full-level pt ⟹ N² combos fibrewise distinct via E[N] étale-reduced, the T-D8-bridge register) + the boarded torsionπ_etale' box. All of [YF-⊇] is sorry-free. (STREAM-YN) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…LE] reduced to [YF-⊆] gate (STREAM-YN)
…transport mirror) (STREAM-YN)
…rtPoint fibre-additivity infra (STREAM-YN)
…ED (NaiveProblems:211) New Moduli/TransportPoint.lean: transportPoint (fibre-point transport along curveIsoPullback) + transportPoint_add (mirrors transportSection_add_of_isMonHom at arbitrary base t via the same isMonHom_of_pointedIso_records) + transportPointEquiv (AddEquiv) + transportPoint_pull_pullSection (dictionary → transportSection_pullSection) + AddEquiv.mem_closure_image (closure transport). NaiveProblems: isNaiveFullLevel_asSection_pull (baseChange←Y via baseChangeEquiv closure-transport) + isNaiveFullLevel_pullSection (X←baseChange via transportPointEquiv) → map-field discharged. The full-level closure clause (arbitrary fibre points) needed the fibre AddEquiv the Γ₁ kernel-route avoided — the v10.176 scope correction, now built. Unblocks the Y(N) representability half → MASTER. (STREAM-YN) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…blem total functor) (STREAM-YN)
…ted to YFullTE9) Per v10.111/117 relocation doctrine: the T-E9 master (zero code-consumers) relocates from NaiveProblems (the held by-sorry, now retired with a pointer) to new ModularCurve/YFullTE9.lean downstream of YFullRoute, closed by . The Y(N) representability theorem is now connected end-to-end through the YFULL route — consuming this session's [YF-⊇]/[YF-CLOPEN] + the now-total gammaFullNaiveProblem functor (map-field) — and reduced to EXACTLY the two boarded cross-charter gates: gammaFullNaive_rigid ([YF-NOETH]/CHARTER-P3B3) and exists_representing_smooth_affine ([YF-GEOM]/CHARTER-FP4). Full build green (3949 jobs). (STREAM-YN) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…frontier COMPLETE (rest cross-charter-gated) (STREAM-YN)
comboFamily_injective_iff_closure_top + range_comboFamily_eq_closure: over a finite group G of order N^2 (T-B6, E[N]_k̄ ≅ (ℤ/N)²), the N² combinations [a]P+[b]Q are pairwise distinct iff P,Q generate G — the fibrewise heart of KM 1.4.4. Axiom-clean (propext/choice/Quot.sound). Serves coordinator order 2 (T-D8-bridge fullLevel_divisor_iff_naive_gen) step D; steps A/B (scheme↔affine full-set bridge, KM 1.9-1.10) next. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The naive full-level generation condition over a geometric fibre is reshaped, sorry-free, into group-theoretic distinctness of the N² combinations: naiveClosure_iff_torsion_filled : condition ⟺ closure fills E[N]_t closure_pair_eq_iff_closure_top : ambient closure = H ⟺ closure_H = ⊤ (axiom-clean) naiveClosure_iff_subgroup_closure_top : composed, route-agnostic finite_fibreTorsion / natCard_fibreTorsion : #E[N]_t = N² (T-B6) naive_iff_comboFamily_injective : naive gen ⟺ N² combos distinct Composes step D + T-B6. Own proofs sorry-free; inherits only T-B6's registered black-box sorryAx. Fibre half of KM 1.4.4; scheme half (sectionsDivisor.ideal = torsionIdeal ⟺ fibrewise distinct, KM 1.9-1.10) remains — no repo infrastructure yet, boarded for coordinator. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…me-side ⟹ re-scoped to elementary support-counting (not multi-week) Documents the precise, de-risked route for the last gate (fullLevel_divisor_iff_naive_gen ⟹ / [YF-⊆]): support tool CartierDivisor:1052 + T-B6 count + pigeonhole. Corrects the prior multi-week-crux framing with concrete evidence. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ivisor_baseChange) for the T-D8-⟹/[YF-⊆] gate Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…mbing The section divisor commutes with base change: (sectionsDivisor π P).ideal.comap (pullback.fst π t) = sectionsDivisor of the base-changed sections of pullback.snd π t. Assembled from baseChange_ideal + ker_sectionBaseChange + comap_prod. The general (non-elliptic-curve-specific, curveIsoPullback-free) fibre-reduction step for the [YF-⊆] / fullLevel_divisor_iff_naive_gen ⟹ argument. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…support — T-D8-⟹ fibre support-covering - sectionsDivisor_support (CartierDivisor, public wrapper of the private support-prod): (sectionsDivisor π P).ideal.support = ⋃ᵢ range(Pᵢ.base). - sectionsDivisor_comap_support (SectionsDivisorBaseChange): the base-changed section divisor's support = ⋃ᵢ range(base-changed section) — combines sectionsDivisor_baseChange with the support wrapper. Axiom-clean. The topological core of the [YF-⊆]/fullLevel_divisor_iff_naive_gen ⟹ argument: with a divisor equality, the union of fibre section images = fst⁻¹(J.support). Full build green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…identification pinned as remaining gate Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…hole for T-D8-⟹ If a finite family f : ι → X has range exactly T with #T = #ι, then f is injective. The counting core of the [YF-⊆] distinctness argument: N² combinations covering the N² fibre torsion points must be pairwise distinct. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…e of the T-D8-⟹ count For an essentially-finite-type formally-étale algebra A over a separably closed field K, #PrimeSpectrum A = finrank K A, via mathlib's equivPiOfIsSepClosed (A ≃ₐ (PrimeSpectrum A → K)). The algebraic core of the reduced-fibre point count (KM 3.7.1) for [YF-⊆]. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…eme<->algebra glue remains (9 lemmas this session) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…oint count For A an ess-finite-type formally-étale algebra over a sep-closed field k, Spec A has finrank k A topological points (↥(Spec A) defeq PrimeSpectrum A + the algebra count core). The scheme-level reduced-fibre point count (KM 3.7.1) for [YF-⊆]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…torsion-fibre connection is the sole remaining glue Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… the fibre count Source of a finite morphism to an affine scheme is affine (via HasAffineProperty @IsAffineHom). The clean affineness step for the torsion-fibre point count; the algebra-instance derivation + .finrank connection (needs CartierDivisor import + ΓSpecIso threading) is the remaining fiddly glue. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… glue concretely bounded (11 lemmas) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ation (KM 3.7.1) A finite étale scheme over a separably closed field has finrank-many topological points (= as many points as sections). Mirrors natCard_sections_eq_finrank, reusing its full affine↔algebra translation (isoSpec ψ, Algebra.Etale instance, finrank_SpecMap) and algHomEquivPrimeSpectrum for the points↔algHoms↔PrimeSpectrum bridge. This cracks the sole remaining hard piece of the T-D8-⟹ / [YF-⊆] argument. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… = N² (T-B6 point form) Applies natCard_carrier_eq_finrank to (E.baseChange t).torsionπ N (finite étale over k̄) + torsion_rank. The reduced-fibre point count for [YF-⊆], own-proof sorry-free (inherits only the registered torsion black boxes via torsion_rank, as T-B6 does). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…rd_carrier_eq_finrank + natCard_torsion_fibre); only plumbing remains Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…range helper for [YF-⊆] Over a single-point domain (a geometric point Spec k), ⋃ᵢ range(fᵢ) = range(i ↦ fᵢ default) — turns the support-covering into a Set.range fit for the pigeonhole. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… (T-D8-⟹ piece a1) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…l.support)=N² (T-D8-⟹ piece a) Via torsionIdeal_support (support=range torsionι) + pullback.range_snd + closed-immersion injectivity + the pasting iso (pullbackRightPullbackFstIso + torsion_baseChange_isPullback) to natCard_torsion_fibre=N². Completes piece (a) of the [YF-⊆] count chain. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…lemmas, only wiring + (d) curveIsoPullback remain Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…⟹ distinct base-points (T-D8-⟹ b+c) Assembles sectionsDivisor_comap_support + iUnion_range_eq_range_eval + pigeonhole + natCard_fibre_torsion_locus: the N² base-changed sections have pairwise-distinct base-points. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…8-⟹ piece d) Distinct base-points force the pulled points distinct (via the sectionBaseChange lift structure). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…n COMPLETE (KM 3.7.1) The Drinfeld full-level divisor equality implies naive fibrewise generation. Assembles the whole ⟹ chain: count-identification → piece (a) #fst⁻¹=N² → (b+c) distinct base-points → (d) distinct pulls → (e) comboFamily injective via naive_iff. The decisive direction for [YF-⊆]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…(18 lemmas; count cracked + ⟹ proven) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The tautological pair is full-level over levelSpaceΓ (via levelSpaceΓ_spec with h=𝟙), mirroring exists_tautSection. The starting point for range_levelSpaceΓι_subset ([YF-⊆]): full-level at a levelSpaceΓ point → (naive_gen_of_divisor_eq ⟹) generation → no combo vanishes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The taut pair generates E[N] at every geometric point of levelSpaceΓ — direct application of the T-D8-bridge ⟹ (naive_gen_of_divisor_eq) to taut_isFullLevel_over_levelSpaceΓ. Clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…remaining wiring scoped Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…e A (fibre) If P,Q generate G (order N²), every nonzero-indexed combo [a]P+[b]Q ≠ 0 (step D corollary). The no-vanishing input for range_levelSpaceΓι_subset. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…)=κ(y), geom pt factors); tools mapped Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…-⊆] piece B enabler For a closed immersion, the residue-field map is an iso (κ(f x)≅κ(x)): injective (field hom) + surjective (SurjectiveOnStalks + residue_surjective, via the residue_residueFieldMap naturality). Unlocks factoring fromSpecResidueField through closed immersions for piece B. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…e B factoring A geom point at w factors through a closed immersion given w ∈ range (via residueFieldMap iso + SpecMap_residueFieldMap naturality). The key enabler for piece B: the geom pt at w factors through BOTH levelSpaceΓ and the agreement locus, giving combPoint≠0 and combPoint=0 at the same point. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…eFieldMap iso + factoring); 24 lemmas Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… + contradiction structure The fullLevelOpenSet membership reduces to: hw (w∈range levelSpaceΓι) + hmem (w∈pointVanishSet combPoint) + hcd (cd≠0) ⊢ False. The contradiction (geom pt factors through both closed immersions via exists_fromSpecResidueField_factor: levelSpaceΓι→combPoint≠0, agreement locus→combPoint=0) is the remaining ~60-80 line integration of built tools. sorry marks the fibre-connector integration. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…CLOPEN]/[YF-ETALE]★ discharged The reduced-fibre distinctness leaf of Y(N) (KM 3.7.1): the full-level closed immersion levelSpaceΓι lands in the open fullLevelOpens, so it is an open immersion (isOpenImmersion_levelSpaceΓι_full), and the Γ(N)-presentation is étale (etale_fullLevelSpaceStruct in YFullRoute is now genuinely discharged). New: - comb_ne_zero_of_generates (FullLevelFibre): group core — over a geometric point where N is invertible, if two N-torsion points generate the fibre's N-torsion, no nonzero [c]A+[d]B (c,d ∈ [0,N), not both 0) vanishes. Pigeonhole via comboFamily_ne_zero_of_closure_top + natCard_fibreTorsion (T-B6). - taut_generates_restrict (FullLevelClopen): pushes taut_generates_over_levelSpaceΓ through Point.baseChangeEquiv + Point.castBase (assoc) into restrict form. - range_levelSpaceΓι_subset Part 2: at the alg-closed geometric point over w (factored through levelSpaceΓι), the taut pair generates ⟹ combPoint(cd)≠0, contradicting Part 1's agreement-locus vanishing (hzero). Root ModularCurves.lean now imports FullLevelClopen + FullLevelDivisorBridge. Full build green (4212 jobs); sorry-free; axioms = the pre-existing T-B6 registered KM black-boxes (sorryAx via BB-DIFF/BB-QF/BB-FLAT/BB-DEG), no new sorry. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…es_divisor_eq (full iff now sorry-free downstream)
The reverse of the T-D8-bridge (KM 3.7.1 / 1.4.4): fibrewise generation ⟹ the
Drinfeld full-level divisor equality. The board had flagged this as needing the
full-set-of-sections / T-D2 globalization ("missing infra"); it does NOT.
Route (cheaper than T-D2): if two combination sections [a]P+[b]Q collide
topologically at u ∈ S, their difference hits the RATIONAL identity section at u,
so sections_residue_eq_of_base_eq (separatedness ⟹ forced residue-field agreement,
no Galois ambiguity since the collision point is rational) upgrades the collision to
residue-field agreement; pulling to the geometric point over u makes the difference
vanish, but generation makes the N² combinations injective there
(naive_iff_comboFamily_injective) — forcing the two indices equal. Pairwise
topological distinctness then feeds the [YF-⊇] divisor chain
(sectionsDivisor_ideal_eq_torsionIdeal).
New in FullLevelClopen:
- naive_gen_implies_divisor_eq — the ⟸ content (~50 lines).
- fullLevel_divisor_iff_naive_gen_downstream — the full iff (⟹ = naive_gen_of_divisor_eq,
⟸ = naive_gen_implies_divisor_eq), the sorry-free downstream discharge of the
register box Basic.fullLevel_divisor_iff_naive_gen.
Builds; axioms = the pre-existing T-B6 registered KM black-boxes (no new sorry).
NOTE for coordinator: Basic.fullLevel_divisor_iff_naive_gen (:115) + isFullLevel_iff_naive
(:130) are now dischargeable by relocation (byte-identical statements move downstream to
FullLevelClopen; consumers YFullRoute:552 + GammaHRepresentability:641 re-point). Cross-cutting.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…MPLETE + T-D8-bridge ⟸ PROVEN (full iff sorry-free downstream); relocation boarded for coordinator Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
CBirkbeck
pushed a commit
that referenced
this pull request
Jul 13, 2026
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.
STREAM-YN's completed Y(N) frontier, per the v10.172 cadence. Clean-room verification pinned at d9f2fbb.
Headline
etale_fullLevelSpaceStruct— the Γ(N)-presentation is étale over the base (KM 3.7.1 / Loeffler 3.8.2 for Γ(N)): open immersion ([YF-CLOPEN]) ≫ pullback of finite étale ≫ finite étale. Depends only on the inherited T-B6/BB-DIFF torsion black-box.isOpenImmersion_levelSpaceΓι_full+ the full ⊇-over-fullLevelOpens leaf (Moduli/FullLevelClopen.lean:combSec_ne_of_diff,isFullLevel_taut_over_fullLevelOpens), axiom-clean.fullLevel_divisor_iff_naive_gen— proven BOTH directions sorry-free downstream (viasections_residue_eq_of_base_eq; no T-D2 globalization needed).gammaFullNaive_representablewired end-to-end (ModularCurve/YFullTE9.lean).WIP markers (main tolerates per CLAUDE.md)
The MASTER's
Representable+ recollement conjuncts bottom out at the sharedrepresentable_iffengine (KM 4.7.0) — the same gate KM's Γ₁ and GH's Γ_H hit — currently gated on T-E-OMEGA (coordinator-tracked, un-demote surfaced to owner). Plus the inherited T-B6 torsion black-box and one redundantLevelStructure/Basic.leanregister-box (proof exists sorry-free downstream inFullLevelClopen; relocation is a boarded coordinator TODO). The cleanup fleet only touches sorry-free declarations.Verification
No PR CI on this repo — coordinator clean-room
lake build ModularCurvesin a detached worktree at d9f2fbb:Build completed successfully (4212 jobs), real logged exit 0, zero errors.Held for owner merge-go (coordinator opens + verifies; owner merges — the #5256/#5680 precedent).
🤖 Generated with Claude Code