Proof-ready number-system refactor

[wsollers]

Purpose

Normalize the Lean number-system development against the streamlined Markdown source package.

Invariants

• definitions are mathematically complete;
• theorem statements are final;
• sorry appears only in proof bodies;
• Markdown order controls the proof queue;
• Blueprint TeX is generated from the same Markdown;
• p-adic material remains a sequel and does not block the active build.

Current slice

• proof-readiness postmortem and source manifest;
• proof-readiness linter;
• Markdown-to-Blueprint assembler;
• initial proof-ready Cauchy-real definitions and quotient obligations.

This PR remains draft while the remaining constructions are normalized and CI is made green.

[wsollers]

Progress update:

• Fixed the first PrimitiveIntervals compile errors by deriving non-strict-order reflexivity from the existing order law and stating injectivity explicitly.
• Added LRA/VolumeII/Rationals/Canonical.lean with a genuine positive-denominator context, cross-multiplication equivalence, quotient carrier, raw addition/multiplication/negation/order, representative-independence obligations, induced quotient operations, zero/one, integer embedding, and final ordered-ring law statements.
• Wired the canonical rational module into LRA.VolumeII.NumberSystems.

The latest Lean and Pages workflows are running on commit 0834bad87a77316a44f87778d798fe3597bb26df. Reciprocal and reduced-fraction normalization remain intentionally separate because they require an explicit normalization map from nonzero integer numerators to positive natural denominators.