Add exact finite absorbing Markov-chain foundation

[lyw-ops]

Adds exact finite absorbing Markov-chain execution and solving on top of FiniteLaw. For example, a fair repeat-or-stop chain with terminal reward six computes expected reward six and duration two, while retaining unfinished probability 1/4 in a two-step finite run.

Dependency: this draft depends on #37, which is still open. The Markov-only change is commit 3726be0; the inherited finite-law commits belong to #37. Merge #37 first, then rebase this branch onto main before marking this PR ready.

Scope

• Two library modules: executable finite rows, censored first-hit execution, exact absorption checks and Cramer solving; a separately imported analytic leaf proving normalization, integrability, Bellman uniqueness, and equality with the actual output.
• Formech-style sections with scoped variables and checked-absorption hypotheses, helper lemmas, and main specification/correctness theorems. The 59 authored public declarations retain their interfaces; an elaborated comparison also preserves all 133 public declaration types, including generated entries, and all 53 public definition bodies. Five private proof lemmas were extracted.
• Worked examples consume the library directly. They cover geometric and cyclic absorption, multiple terminal outcomes, a partially closed domain, and an empty transient domain. The geometric example proves its concrete reward and duration integrals with ordinary Lean proofs.
• The root aggregate imports only the executable module. Examples import the semantic leaf explicitly. Add reading/scope documentation and CI checks for execution, import separation, computability, axiom dependencies, and kernel replay.

The automatic checker covers every supplied transient state. Rejection can coexist with successful absorption from another start. The finite chain is a supplied Markov specification, not a quotient of arbitrary EFG histories. Dense rational determinants and Cramer's rule make no scalability claim.

Validation

• lake build: passed, 8602 jobs.
• lake build EconCSLib.Examples: passed, 2543 jobs.
• lake env lean tests/FiniteMarkovChainSmoke.lean: 31 runtime guards passed.
• lake env lean tests/FiniteMarkovChainAudit.lean: 194 library/example declarations, zero noncomputable declarations, standard logical axioms only; 193 safe declarations replayed in the kernel. One compiler recursion helper was separately validated and excluded from replay.
• Existing FiniteLawSmoke and FiniteLawAudit: passed.
• Placeholder and diff-whitespace checks: passed.

The new library and example modules build without warnings. Existing warnings in unrelated modules remain outside this change.