Real-valued Shannon entropy H(P) = −Σ pᵢ·log pᵢ (reals + probability layer) #264

Status

The parametric non-distinguishing half is DONE — proofs/agda/EchoEntropy.agda ships entropy-blind-parametric (any H : (Fin 2 → W) → X factoring through the fibre distribution agrees on echo-true vs echo-false) and entropy-witness-distinguishes (the Σ-witness distinguishes), landed in #261. The discrete fibre-count shadow (entropy-shadow / shannon-shadow via ⌊log₂⌋) was already present.

Open

Lift the shadow to real-valued H(P) = −Σ pᵢ log pᵢ over a parametric distribution. This needs a rationals/reals layer + a probability interface — out of reach under --safe --without-K without significant extra infrastructure. Lower priority: the discrete + parametric forms are the load-bearing artifacts for the abstraction-barrier line.

In-repo sketch / proof-debt (already recorded)

• proofs/agda/EchoEntropy.agda companion-remark: the open real-valued / mutual-information forms.
• EchoThermodynamics.agda and EchoStabilityTests.agda point at EchoEntropy.agda.

Acceptance

• A --safe-compatible reals / probability interface (or an explicitly isolated + justified analytic interface).
• H defined; the non-distinguishing theorem restated over H.
• No postulates in the load-bearing path.