Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.clamped-surrogate

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/clamped_surrogate.clj1 definitions, 3 theorems

AHoF D52 Clamped Surrogate Objective (PPO): stabilize policy-gradient updates by clamping the probability ratio r into the trust region [lo, hi] = [1-eps, 1+eps] before forming the surrogate objective: clamp r lo hi = min (max r lo) hi. A ratio 3/4 already inside [1/2, 1] clamps to itself; a ratio 1/4 below the region clamps up to the lower edge 1/2; a ratio 2 above the region clamps down to the upper edge 1. Proved native and axiom-free: the clamp (nested min/max) and the three worked regimes (inside, below, above). Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.clamped-surrogate` prints this classification.

clip/clamp :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

clip/inside-region-unchanged :
  → clip/clamp 3/4 1/2 1 = 3/4

clip/below-region-clamped-up :
  → clip/clamp 1/4 1/2 1 = 1/2

clip/above-region-clamped-down :
  → clip/clamp 2 1/2 1 = 1