R4 revision: re-index tiers, add leadership hierarchy evidence, trim …

…discussion

Major changes:
- Re-index tiers bottom-up (Earth=0, Mars=3) so j≤i reads naturally
  as "at or below" — resolves persistent fatal finding
- Add flat construction formal definition (Q1^flat)
- Add Q1 quorum count table from TLA+ enumeration quantifying the
  leadership hierarchy gradient (992 Earth vs 217 Mars, 4.6×)
- Add WPaxos contrast: symmetric grids cannot express per-tier
  leadership cost because uniform Q1 size is required for intersection
- Trim Discussion from 733 to ~280 words; cut Conclusion speculation
- Calibrate abstract: label 0%/100% as structural consequence
- Prove safety-tier-membership claim (Q1∩T0≠∅, Q2⊆T0)
- Add simulator parameter table, commit hash placeholder
- Add pigeonhole derivation and relaxed Q1 formal definition
- Total word count reduced from 6259 to ~4500

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>