AGLib: bootstrap governance + Lake package on empty palimpsest/aglib

[AxelDlv00]

Goal

palimpsest/aglib is an empty orphan integration branch. Repository governance files and the AGLib Lake package do not exist yet. This issue is the first PR that must create them so ordinary extraction work can follow.

Build only through a reviewed PR into palimpsest/aglib. Do not push to main.

Required deliverables (one PR)

1. Governance (required to unlock later issues)

   • AGLib/ROADMAP.md — short mathlib-style plan for the library (scope, layers, extraction policy)
   • AGLib/docs/references.bib — bibliography stub (can be nearly empty; real cites added later)

2. Lake package bootstrap

   • AGLib/lean-toolchain, AGLib/lakefile.toml, AGLib/lake-manifest.json (mathlib pin)
   • AGLib/AGLib.lean, minimal AGLib/AGLib/Basic.lean (light import; lake build green)
   • AGLib/README.md

3. CI

   • .github/workflows/lean-ci.yml for pushes/PRs to palimpsest/aglib (lake-build on AGLib/)

Constraints

• Base branch: palimpsest/aglib (empty tree today)
• One focused PR; no monorepo content, no challenge cones, no probe files
• No automatic merge to main (manual backport later)

Out of scope

Blueprint edits, porting FormalizedSources wholesale, second extractions beyond bootstrap.

[AxelDlv00]

Palimpsest automation ⚙️ 📣

Engine: codex
Model: gpt-5.6-sol
Effort: ultra

Queued by Palimpsest for contributor contributor. Review profiles: mathematical-correctness, maths-lean-correspondence, lean-quality, architecture. Claims expire automatically if the contributor session does not complete.