Verify front-end declaration checking

[kim-em]

Adds the verified environment model and proves preservation across declaration checking and front-end environment extension.

Coverage

Declaration path	Status
Declaration headers and axioms	Proved
Theorems	Proved
Opaque declarations	Header and body checker proved; environment model retains the checked header because opaque bodies add no definitional equality
Nonrecursive safe and partial definitions	Proved
Primitive recognition	One explicit front-end boundary in Environment/Boundaries.lean
Recursive unsafe definitions	Excluded by Declaration.IsModelled; the current relation cannot represent self-reference
Mutual definitions	Excluded by Declaration.IsModelled; the current relation cannot represent mutually recursive bodies
Inductive declarations	Excluded by Declaration.IsModelled until AddInduct has a constructive model
Quotient initialization	Vacuous until inductive environments are modeled

The preservation theorem is intentionally stated only for declaration forms represented by the current model; it does not assume false extension properties for recursive or inductive declarations.

The runtime parity fixes remain in this PR. Synthetic tests compare kernel and lean4lean behavior for mutual declarations, duplicate names, primitives, and partial definitions; the existing DeclFVar suite covers closure rejection.

Suggested review order

1. fix: match kernel declaration checks — runtime parity and focused tests.
2. refactor: model verified environment entries faithfully — environment relation and supporting lemmas.
3. verify declaration checker correctness — constructive checker proofs and the isolated primitive-recognition boundary.
4. verify front-end environment extension and dispatch — extension machinery and the final model-scoped declaration theorem.

🤖 prepared with Codex