Note: optional ViaL2 simplification by canonicalizing the directing measure

[cameronfreer]

Tracking a design observation surfaced during the post-#50 review. Not a planned PR — recording for future reference because the alternative architecture is interesting and the math already supports it.

Observation

Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean:300 (directing_measure_satisfies_requirements) can be discharged directly using the existing ViaMartingale.directingMeasure / conditional_law_eq_directingMeasure, bypassing the local Stieltjes/CDF directing-measure chain entirely. Lean LSP confirms this body closes:

refine ⟨ViaMartingale.directingMeasure (μ := μ) X hX_meas, ?_, ?_, ?_⟩
· exact ViaMartingale.directingMeasure_isProb X hX_meas
· exact ViaMartingale.directingMeasure_measurable_eval X hX_meas
· intro m k hk B hB
  exact indicator_product_bridge X hX_contract hX_meas
    (ViaMartingale.directingMeasure (μ := μ) X hX_meas)
    (ViaMartingale.directingMeasure_isProb X hX_meas)
    (ViaMartingale.directingMeasure_measurable_eval X hX_meas)
    (fun n B hB => ViaMartingale.conditional_law_eq_directingMeasure X hX_contract hX_meas n B hB)
    k hk B hB

Potential deletion surface (rough estimate, ≈3,291 lines)

After re-running zero-caller checks, the following could plausibly become dead:

• MoreL2Helpers.lean (Stieltjes section)
• DirectingMeasureIntegral.lean, DirectingMeasureBridge.lean, DirectingMeasureIic.lean, DirectingMeasureCore.lean
• Possibly portions of the AlphaIic* / AlphaConvergence chain

Total ≈3,291 lines, but I would not assume all are reachable from this change until the packaging theorem is swapped and usage rerun.

Architectural tradeoff

Currently the L² path constructs a Kallenberg-style witness from L² Cesàro limits → alphaIic → Stieltjes → directing_measure, then separately proves that this measure agrees a.e. with the condExpKernel pushforward. The common ending only ever consumes a ν satisfying probability + measurability + the product bridge.

The shortcut chooses the already-existing condExpKernel-derived witness (from ViaMartingale) directly. Mathematically equivalent post-agreement-theorem; conceptually it stops formalizing the part of Kallenberg's L² proof where the directing measure is built from L² limits.

Three options

1. Take the shortcut. Mathematically clean, big deletion, but hX_L2 becomes essentially decorative in the packaging theorem and the L² route's witness comes from the martingale/condExpKernel infrastructure instead of an L²-native construction.

2. Preserve the current L² route. Keep the local Stieltjes/CDF directing-measure chain as its own Kallenberg-style witness. No deletion; status quo.

3. Middle path. Keep the theorem that identifies the L² Stieltjes directing measure with the condExpKernel pushforward as a documented bridge (preserving the mathematical audit trail), but make the main packaging theorem use the canonical witness directly. Deletes most downstream plumbing while keeping the construction visible as a lemma.

Recommendation in this repo

Preserve the L² route as a distinct Kallenberg proof (option 2). The architectural simplification is valid but trades the "three independent proofs" posture of the formalization for line savings, and the current setup already has full agreement-theorem coverage.

Filed for future reference, not as a planned PR.