Add executable finite rational probability laws

[lyw-ops]

Summary

Add exact finite probability laws to the stable library. FiniteLaw α stores nonnegative rational weights on a finite list, so map, bind, and expectation execute without requiring the outcome carrier to be finite or decidably equal. Zero-mass conditioning returns none; a valid posterior with zero expected payoff remains a successful result.

The foundation includes independent products, partial conditioning, relational couplings, and equivalence of pre-sampling and on-demand fresh queries. Scoped variables and explicit hypotheses precede private helper lemmas and main results. Coupling composition reuses its two marginal arguments; independent-coordinate conditioning separates the probability and product identities; deferred sampling concludes with a short structural induction.

Scope

• Six Math/Probability/FiniteLaw modules, registered in EconCSLib.lean.
• A design note covering reading order, assumptions, proof organization, sparse versus semantic equality, and the finite rational execution boundary.
• Runtime regressions and a module-owner-based computability, axiom, and kernel-replay audit, both added to CI.

This is the independent probability foundation extracted from EFG development. It introduces no EFG strategy, history, or compiler changes and constructs no general measure-theoretic kernels or infinite path measures.

Verification

• lake build — 8,601 jobs. The finite-law modules emit no warnings; existing main modules still emit warnings.
• lake build EconCSLib.Examples — 1,608 jobs.
• lake env lean tests/FiniteLawSmoke.lean — 22 executable guards and four theorem instances covering infinite function carriers, repeated atoms, impossible conditioning, products, composed couplings, and fresh queries.
• lake env lean tests/FiniteLawAudit.lean — 380 declarations, zero noncomputable declarations, only standard logical axiom dependencies; 376 safe declarations replayed in the kernel. Four compiler recursion helpers are counted separately and excluded from replay.
• Temporary negative fixtures confirmed the audit rejects noncomputable definitions, additional axioms, unsafe definitions, and partial def.
• python3 scripts/check_lean_placeholders.py EconCSLib.
• git diff --cached --check.
• Blueprint checks are not applicable locally: docs/knowledge/ is unchanged.

The style-refactoring comparison preserves all 112 handwritten public declarations, including their elaborated parameter order, universe generality, and axiom dependencies. All 97 canonical definition bodies match; an additional Lean definitional-equality check passes for all 93 safe definitions. The refactor adds ten private proof lemmas, removes one compiler-generated _simp_1 proof helper, and changes the types of two compiler-generated _proof_ helpers; these implementation details are not counted as handwritten API.

Notes

Products enumerate finite combinations; this is an exact execution API, with no claim of efficient enumeration for large products. Fresh-query applications must supply the indexed tree and its freshness evidence. The original EFG worktree was checked against its content hashes and left unchanged.