How does an electric eel see in muddy water?

module eod_dipole;

// Electric organ discharge — modelled as a point dipole at the
// origin with moment p along the eel's body axis. Field at a
// receptor at distance r and angle theta from the dipole axis:
//   E_r     = (1 / 4πε) · 2p cos θ / r³        (radial)
//   E_θ     = (1 / 4πε) · p sin θ / r³         (transverse)
// |E| has a 1/r³ dependence — the same near-field falloff the
// shark sees on prey.
const FOUR_PI_EPS_WATER: Real = 1.39e-9   // F/m for fresh water (eps_r ~80)

@verify(lean, theorem = "eod_field_magnitude_nonneg")
fn dipole_field_magnitude(p: Real, r_m: Real, theta_rad: Real) -> Real
    requires (p >= 0.0 and r_m > 0.0)
    ensures  (result >= 0.0)
{
    p * sqrt(1.0 + 3.0 * cos(theta_rad) * cos(theta_rad))
      / (FOUR_PI_EPS_WATER * r_m * r_m * r_m)
}

module object_perturbation;

// Object perturbation — a conductive sphere of radius a at
// distance r from the dipole, with conductivity contrast
// σ_obj vs background σ_water, distorts the field. The
// fractional perturbation of |E| at a nearby receptor
// scales as:
//   ΔE / E ≈ Γ · (a / r)³
// where Γ is the contrast factor; Γ → +1 for a perfect
// conductor, Γ → −1/2 for a perfect insulator. The eel
// classifies prey vs rock by the SIGN of ΔE / E.
@verify(lean, theorem = "contrast_factor_in_signed_unit_interval")
fn contrast_factor(sigma_obj: Real, sigma_water: Real) -> Real
    requires (sigma_obj >= 0.0 and sigma_water > 0.0)
    ensures  (-1.0 <= result and result <= 1.0)
{
    clamp((sigma_obj - sigma_water) /
          (sigma_obj + 2.0 * sigma_water),
          -1.0, 1.0)
}

@verify(lean, theorem = "perturbation_decays_as_inverse_cube")
fn perturbation_fraction(gamma: Real, a_m: Real, r_m: Real) -> Real
    requires (a_m >= 0.0 and r_m > 0.0)
    ensures  (-1.0 <= result and result <= 1.0)
{
    clamp(gamma * (a_m * a_m * a_m) / (r_m * r_m * r_m),
          -1.0, 1.0)
}

module skin_electrode_array;

// The eel reads the perturbation pattern across its row of
// skin electrodes. We model one electrode at angle phi around
// the body and compute the local |E| modulation that a target
// at (r_m, theta_target_rad) imprints on it. This is the
// "image" the eel inverts to localise the object.
const FOUR_PI_EPS_WATER: Real = 1.39e-9

@verify(lean, theorem = "electrode_signal_nonneg")
fn electrode_signal(p: Real, phi_rad: Real, r_m: Real,
                    theta_target_rad: Real, gamma: Real,
                    a_m: Real) -> Real
    requires (p >= 0.0 and r_m > 0.0 and a_m >= 0.0 and
              -1.0 <= gamma and gamma <= 1.0)
    ensures  (result >= 0.0)
{
    // Base EOD intensity at this electrode.
    let base = p * sqrt(1.0 + 3.0 * cos(phi_rad) * cos(phi_rad))
               / (FOUR_PI_EPS_WATER * r_m * r_m * r_m)
    // Object perturbation, geometric coupling via cos of angle
    // between electrode and target.
    let coupling = clamp(cos(phi_rad - theta_target_rad), 0.0, 1.0)
    let perturb = gamma * (a_m * a_m * a_m) / (r_m * r_m * r_m)
    base * (1.0 + coupling * perturb)
}

module prey_vs_rock;

// The classifier: prey are conductive (live tissue σ ≈ 1 S/m
// vs water σ ≈ 0.05 S/m); rocks are insulating (σ ~10⁻⁸ S/m).
// Sign of contrast_factor flips between them. So a SINGLE
// readout — the polarity of ΔE / E — separates prey from
// rocks regardless of distance, as long as the magnitude is
// above the eel's noise floor.
const PREY_CONTRAST: Real = 0.95     // approx for fish flesh in fresh water
const ROCK_CONTRAST: Real = -0.50    // approx for high-resistance gravel

@verify(lean, theorem = "prey_and_rock_have_opposite_signs")
fn prey_minus_rock_polarity_gap() -> Real
    ensures (result > 1.0)
{
    PREY_CONTRAST - ROCK_CONTRAST
}