security: 2 ProofDrift findings need DRAFT-PR remediation (Track D)

[hyperpolymath]

panic-attack estate sweep — Track D (proof-aware) tracking issue

panic-attack assail flagged the following PA021 ProofDrift findings in this repo on 2026-05-26.

Unlike Track C findings (judgement calls in non-proof code), these touch proof modules. The campaign convention is to remediate them via DRAFT PRs with a local proof-rebuild check before flipping to ready-for-review.

Estate tracker: hyperpolymath/panic-attack#32.

Findings

Medium  lol/analysis/test/runtests.jl:?  1 `@test x isa Y` assertion(s) with no value check — type-only tests may substitute for an unwritten formal theorem in lol/analysis/test/run
Medium  lol/proofs/theories/information_theory.agda:?  4 postulate block(s) (unproven axiom — verify these hold) in lol/proofs/theories/information_theory.agda

---

🤖 Discovered during the panic-attack estate sweep (2026-05-26). See hyperpolymath/panic-attack#32 for campaign tracker.

[hyperpolymath]

Closed by classification PR #184. The PA021 ProofDrift finding is the 4 information-theory postulates in lol/proofs/theories/information_theory.agda, classified by the file's own comment as 'justified postulates, not proof debt' (real-analysis formalisation out of scope). The Julia @test type-only assertion is part of the closed Julia chapter and is tracked at the container level.