refactor: unbundle splitting unit u from BinaryConvexOp

Remove the splitting unit `u : R` with `[Invertible u]` and
`[Invertible (1 - u)]` from the `BinaryConvexOp` structure, making
it a parameter of `affineOfBinary` and the proof machinery instead.

The key insight is that `u` is an implementation detail of the balanced
tree recursion, not a fundamental property of the convex operation.
The `binCombo_swap_inner` axiom is now universally quantified over `u`.

Main changes:
- `BinaryConvexOp` no longer bundles `u`, `u_inv`, `one_sub_u_inv`
- `affineOfBinary`, `leftWeightedSeq`, `rightWeightedSeq` take `u` as
  an explicit parameter (via section variable)
- `ConvexSpace.ofBinary` takes `u` as an explicit parameter
- New `ConvexSpace.ofBinaryCharNeTwo`: over an ordered field where
  `2 ≠ 0`, any `BinaryConvexOp` gives a `ConvexSpace` using `⅟2`
  as the splitting unit

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em