v0.2.0

Three new modules, all proved from Mathlib alone: no axiom, no sorry, and #print axioms on every declaration reduces to propext, Classical.choice and Quot.sound.

The causal admissible cone as a shared type (CausalCone, CausalData)

• ScaleSpace.CausalAdmissible: a drift b₀ ≥ 0 and a nonincreasing delay profile k ≥ 0 on (0,∞), with ∫₀¹ k < ∞ and ∫₁^∞ k(u)/u du < ∞. The exponents are exponentL (ℝ≥0∞) and exponent (ℝ).
• Two field forms. Some consumers state admissibility as the finiteness of the exponent, ∀ σ ≥ 0, exponentL σ ≠ ⊤. ofNeTop builds the structure from that form, and ne_top_iff_windows proves the two forms equivalent.
• Combinators: add, smul, dilate, with their exponent identities.
• Generator data: drift, Gamma profile γe^{−u}, and stable profile αu^{−α}/Γ(1−α) with exponent σ^α.

Karlin's class E₂* and the symmetry reduction (PolyaFrequencyClass, PowerSumSymmetry)

• Transforms: bilateralLaplace μ s = ∫ e^{−sx} dμ, in Karlin's sign, bridged to complexMGF, charFun and the real integral. polyaE2 γ δ a s = e^{−γs² + δs} ∏ (1 + a_j s) e^{−a_j s} is the class E₂* of Total Positivity I, Ch. 7 (2.2).
• Properties of polyaE2: multipliability under ∑ a² < ∞, the log form on the real axis, the modulus on the imaginary axis, and the value on ±-paired parameters.
• Symmetry reduction:
  • evenness near 0 forces δ = 0 and all odd power sums to vanish (polyaE2_even_imp_oddPowerSums);
  • vanishing odd power sums make ∑ a_j² δ_{a_j} reflection-invariant, whence ∑ g(a_j) = 2 ∑ g(a_j⁺) for even, quadratically bounded g (tsum_eq_two_mul_tsum_posPart).

These discharge the parameter matching between Karlin's representation of Pólya frequency densities and a symmetric exponent. The queued "two-sided Laplace transform as an entire function with an identity theorem" was not built. It is unnecessary at Karlin's letter, and Mathlib's complexMGF already carries holomorphy on the strip and the identity theorem (see the README, "Growing it").

Consumers pinning v0.1.x are unaffected: nothing existing changed.