Prove Shelah-Spencer sparse zero-one law for irrational α

PR #1168 formalizes the statements of Shelah-Spencer’s sparse zero-one law theorems, intending to close issue #1167. The theorems state that, for irrational α between 0 and 1, the Shelah-Spencer sparse graph with edge probability $n^{-\alpha}$ satisfies the zero-one law, namely for every first-order sentence, its satisfaction probability in $G(n, n^{-\alpha})$ tends to 0 or 1 as n grows; the theorems further state that for rational α in (0,1), such a zero-one law fails.

Main reference: [Shelah and Spencer, Zero-one laws for sparse random graphs](https://doi.org/10.1090/S0894-0347-1988-0924703-8), Journal of the American Mathematical Society, 1(1), 97-115 (1988).

- Issue #1167: to be closed with PR #1168;
- PR #1168: awaiting review;
- An independent effort to formalize the proof of the irrational zero-one law is in progress at https://github.com/LibertasSpZ/shelah-spencer-proof; currently with initial definitions and a small helper lemma;
- This tracking issue is intended to track later milestones and possible Mathlib PRs related to issue #1167, PR#1168 and the independent proof formalization effort. Next concrete milestone: define finite rooted extensions and connect their new-vertex and new-edge counts to `extensionCountExponent α v e`.

Start by reviewing PR #1168, issue #1167, and the Shelah–Spencer reference, then inspect the independent proof effort’s initial definitions and helper lemma. The next milestone is to define finite rooted extensions and connect their new-vertex and new-edge counts to extensionCountExponent α v e; completion should support later formalization of the irrational zero-one law.

Written by the indexing model from the issue text.