Data/poincare astrolabe tex

[LehengChen]

Summary

This PR rebuilds projects/poincare-conjecture/.astrolabe from the Morgan-Tian arXiv TeX source (math/0607607).

Scope is data-side only; there are no web/ changes.

Changes

• Add tools/poincare_tex_extract.py, a reproducible TeX-to-Astrolabe extractor for the Poincare project.
• Generate structured Astrolabe entries:
  • 707 atoms
  • 1902 edges
  • 21 docs-src MDX files
  • 21 rendered docs MDX files
• Replace the previous coarse 15-doc split with chapter-based docs from the TeX source.
• Add edge evidence metadata, including ref spans, proof spans, prose triggers, containment spans, and definition-term candidate spans.

Validation

• validate_store passes.
• generated edge metadata validation passes.
• generated text quality validation passes.
• unresolved_refs: {}
• all edge classes graph has 1 connected component and 0 isolated nodes.

Notes

The semantic-only graph still has isolated nodes because many source statements do not explicitly cite other statements. Including prose and structural layers connects the full graph.

Definition-use edges are intentionally marked as weak/candidate evidence and should not be treated as strong proof dependencies.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
open-ga	Ready	Preview, Comment	Jun 28, 2026 11:23am