feat(model): synchronize persistent writes with finite account storage

[Th0rgal]

Canonical persistent writes updated flat storage while the finite account world could retain an old value. Add explicit physical-slot APIs that synchronize both representations, and use them in Denote, reference source semantics and differential initialization. Stateful replay now rejects any mismatch across touched/requested persistent slots after every transaction.

The finite account storage uses a lawful Std.TreeMap. Kernel proofs cover single/batch/transformed writes, duplicate targets, other-account frames and conditional runtime-code commits. Legacy storage APIs and their existing account-world frame regression remain unchanged. Code/balance views, transient storage and legacy shadow channels retain their separate semantics.

Validation on 8be556e947494e8c98fd38eef885672943ac8176:

• Build 9 captured sources match the committed sources, including unchanged DenoteAgreement, DenoteFunctionAgreement and DeploymentWorldChecks; new smoke checks and runners compiled.
• Three valid semantic mutations compile their implementations, then fail unchanged storage-coherence assertions. These are kernel conformance controls, not runtime A/B/C witnesses.
• 32 public theorem axiom audits use only standard Lean axioms; axiom generator and trust inventory checks pass.
• Packed/address storage: 96 real A/B/C transactions agree across three equivalent variants, including writes, deletion and rollback; executed source provenance verified.
• Scalar writes with void returns: another 96 real A/B/C transactions agree across three equivalent variants, with executed source provenance verified.
• Bytes32 and packed struct-member writes: 192 additional real A/B/C transactions agree across six variants (384 storage transactions verified in total).
• Dirty-mapping regressions and saved CREATE2-context replays are running. Full exact-head release gates remain pending; this PR stays draft.

Stacked on #2504. No golden model or pilot provenance changes. This does not admit Solidity CREATE2 or establish complete creation/memory/gas refinement; external-account nonce/code/balance harness integration remains required.