Fill in `LipschitzSmoothWith.hasLineDerivAt`: a `K`-smooth function is
line-differentiable everywhere, and the `lineDeriv` value at every
direction is the actual line derivative. The predicate bound

  |f(x + t·v) - f x - t · lineDeriv f x v| ≤ K/2 · t² · ‖v‖²

(obtained by applying the abs-bound at `(x, x + t • v)` and factoring
`t` via `lineDeriv_smul`) is `o(t)`, which is the `IsLittleO` form of
`HasDerivAt` at `0` for the 1D restriction.

The `continuous` field remains `sorry` pending a separate argument.

Basic.lean (K = 0 cases, no extra hypotheses):
- `lipschitzSmoothWith_const`: constants are 0-smooth
- `lipschitzSmoothWith_affine`: affine functions `y ↦ ℓ y + c` are 0-smooth

Algebra.lean (new, imports `ContinuousAffineMap`):
- `LipschitzSmoothWith.add`: closed under `+` with `K₁ + K₂`
- `LipschitzSmoothWith.const_smul`: closed under nonneg `c •` with `c · K`
- `LipschitzSmoothWith.comp_continuousAffineMap`: composition with continuous affine
  map `A` gives `‖A.contLinear‖² · K`-smooth (currently `sorry`)

The `add` and `const_smul` lemmas require `Differentiable ℝ f` hypotheses because
mathlib's `lineDeriv` doesn't have an unconditional additivity/scaling lemma (junk
values when a summand is non-differentiable); the proofs route through the
`fderiv`-form characterisation to sidestep this.

…ffineMap companion

- `lipschitzSmoothWith_const` now derived as a one-liner from
  `lipschitzSmoothWith_affine` with `ℓ = 0` (was duplicated proof).
- Add `lipschitzSmoothWith_continuousAffineMap` in `Algebra.lean` as the
  bundled `ContinuousAffineMap` companion to the linear+const form in
  `Basic.lean`. Mathematically cleanest statement, but stays in
  `Algebra.lean` since it pulls in `ContinuousAffineMap`.

…predicate

The two-sided abs form of `LipschitzSmoothWith` (predicated on the
weakest form `lineDeriv`) implies line-differentiability everywhere via
`LipschitzSmoothWith.hasLineDerivAt`, so the algebraic preservation
lemmas no longer require any `Differentiable ℝ f` hypothesis:

- `add` works in pure `lineDeriv` form by computing
  `HasLineDerivAt (f₁ + f₂)` from the two pointwise `hasLineDerivAt`
  witnesses (via `HasDerivAt.add`), then chaining the triangle
  inequality with the two abs bounds.
- `const_smul` analogously via `HasDerivAt.const_smul` and `abs_mul`
  plus `abs_of_nonneg` (since `c : NNReal ≥ 0`).
- `neg` becomes trivial under the abs predicate (it was not provable
  under the old one-sided descent form), with the *same* constant `K`.

Also fix the `lipschitzSmoothWith_affine` proof in `Basic.lean` (the
post-`map_sub` goal is now `|0| ≤ 0` rather than the old descent
`linarith`-trivial goal, so the closing tactic switches to `simp`).

The module docstring is updated to drop the (now-false) "not closed
under negation" caveat — that was a consequence of the one-sided form
and disappears in the two-sided form. The deferred-follow-up sorry on
`comp_continuousAffineMap` is unchanged.