Skip to content

cleanup: golf padicLog_mul_of_norm_lt_one #1

New issue
New issue
Closed
Closed
cleanup: golf padicLog_mul_of_norm_lt_one#1
Assignees
CBirkbeck
Labels
lane:cleanupWorker lane: /cleanup (golf/style; auto-merge)

Description

@CBirkbeck
CBirkbeck
opened on Jun 17, 2026

Target: padicLog_mul_of_norm_lt_one — projects/PadicLFunctions/PadicLFunctions/ValuesAtOne.lean:551 (~43-line proof, on main).

Action: Run /cleanup on this declaration (single-declaration mode): golf the proof, apply mathlib style, search mathlib for anything that shortens it. Do not change the statement.

Acceptance (the green bar): lake build PadicLFunctions green · zero new sorry · #print axioms padicLog_mul_of_norm_lt_one shows only propext/Classical.choice/Quot.sound · statement byte-for-byte unchanged.

(First smoke-test ticket for the worker pipeline.)

Activity

  1. CBirkbeck
    added
    lane:cleanupWorker lane: /cleanup (golf/style; auto-merge)
    state:todoTicket open, unclaimed
    state:in-progressTicket claimed + being worked
    and removed
    state:todoTicket open, unclaimed
    on Jun 17, 2026
  2. CBirkbeck
    self-assigned this
    on Jun 17, 2026

  3. CBirkbeck commented on Jun 17, 2026

    @CBirkbeck
    CBirkbeck
    on Jun 17, 2026
    OwnerAuthor

    claimed

  4. CBirkbeck
    added a commit that references this issue on Jun 17, 2026

    cleanup: golf padicLog_mul_of_norm_lt_one (#1) (#4)

    172515c

  5. CBirkbeck commented on Jun 17, 2026

    @CBirkbeck
    CBirkbeck
    on Jun 17, 2026
    OwnerAuthor

    Done — golfed via #4 (squash-merged to main as 172515c).

    Acceptance bar (all green):

    • lake build PadicLFunctions ✓ (3923 jobs, no new warnings)
    • zero new sorry in ValuesAtOne.lean ✓
    • #print axioms PadicLFunctions.MeasureR.padicLog_mul_of_norm_lt_one → [propext, Classical.choice, Quot.sound] ✓
    • statement byte-for-byte unchanged ✓

    Golf: removed dead exp-ball witness (hbxy/jxy were defined but never used — hkey only needs hbx,hby via padicLog_mul), collapsing N := max (max jx jy) jxy → max jx jy; golfed the ‖x*y-1‖<1 ultrametric bound; inlined hpN; stripped narrative comments. Proof body 37 → 27 lines.

  6. CBirkbeck
    removed
    state:in-progressTicket claimed + being worked
    on Jun 17, 2026
  7. CBirkbeck
    closed this as completedon Jun 17, 2026
  8. CBirkbeck
    added 2 commits that reference this issue on Jun 17, 2026

    cleanup: golf padicLog_mul_of_norm_lt_one (#1) (#4)

    f24e2f6

    dev/hasse-weil: DUAL-DESCENT arc landed end-to-end — isogeny symmetry…

    a4170e7
  9. CBirkbeck
    added 7 commits that reference this issue on Jul 8, 2026

    feat(ModularCurves): T-END0 END0a foundation — endMonHom PROVEN (poin…

    37ba287

    docs(ModularCurves): T-UPSTREAM-TRIAGE — upstream-ledger.md (ranked, …

    464046f

    board(T-UPSTREAM-TRIAGE): stage PR-draft .lean files for READY candid…

    98c3999

    board: beastmode-A session close (PHASE-8) — charter arc -> CHARTER-A…

    17ebdff

    board(KM-INTEGRAL): [KM-W2-core] adversarial /develop --decompose — A…

    426f95d

    feat(ModularCurves): [HG-C1d] M6 — IsHopfGalois chartCoaction assembl…

    c0b9ebb

    board(ModularCurves): v10.319 — COORDINATOR HANDOVER rewritten (owner…

    bd4b2b2
  10. CBirkbeck
    added 2 commits that reference this issue on Aug 3, 2026

    goal: fU_uniformContinuous 169 -> 84 (two more lifts, "spell the term…

    312f0b4

    goal: exists_lift_norm_le_of_closed_range 318 -> 298; gate cost map c…

    44e724d
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

lane:cleanupWorker lane: /cleanup (golf/style; auto-merge)

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions