Reference · Logic

rainbow.math.logic.half-monotone

Logicsrc/rainbow/math/logic/half_monotone.clj0 definitions, 1 theorems

The general halving-monotonicity lemma for the convergence capstone: (1/2) * d <= d for every nonnegative rational d. Worked instances live in geometric-convergence; this is the abstract-d step the general `forall epsilon` convergence theorem needs. The proof is by transport, not reflexivity, because `nnrat/multiply` stores the numerator as a nat product and the denominator via `combine-denominator-predecessors`, and because `algebra/nat-add` recurses on its LEFT argument -- so `x + 0` does NOT reduce to `x` definitionally (`algebra/nat-add-zero-right` is a theorem, not a reduction). Concretely, for half = 1/1 the projections reduce to numerator ((1/2)*d) == (num d) + 0 denominator ((1/2)*d) == (den d) + ((den d) + 0) so `nnrat/base-at-most ((1/2)*d) d` normalizes to (num d)*(den d) <= (num d)*((den d)+(den d)) once the two `+ 0` remainders are rewritten away. That inequality is `nat/multiply-left-monotone` applied to `nat/le-add-self (den d)` (den d <= den d + den d); the two `algebra/nat-add-zero-right` rewrites are transported through the cross terms with `equality/substitution` and `equality/congruent-function`, and `nnrat/at-most-from-cross` lifts the cross bound to the native `nnrat/at-most`. Requires nnrat/multiply, nnrat/half, nnrat/at-most-from-cross, nat/multiply-left-monotone, nat/le-add-self, algebra/nat-add-zero-right, equality/substitution, and equality/congruent-function.

nnrat/half-le-self :
  (d : ℚ≥0)
  → nnrat/half · d ≤ d