gate-3: three canonical examples - tropical, epistemic, linear

Three worked Agda examples, each on a different bridge axis,
each satisfying the forced + bridge-axis-active +
distinctness-from-neighbours bar.

  TropicalArgmin: tie-multiplicity at the optimum.
  EpistemicUpdate: agent-knowledge under refinement.
  LinearErasure: mode erasure with retained type structure.

All three examples carry echo-not-prop: a constructive proof
that the relevant Echo type is not a mere proposition. This is
the cleanest cross-axis distinctness signal and the
load-bearing certificate for the truncation argument
post-EI-2 - one of the two surviving distinctness arguments.

Author: hyperpolymath