Real.pos

-- POSITIVITY THAT CARRIES ITS MODULUS.
--
-- `LtR realZero x` is `∥(k : ℕ) × (…)∥` — an Ω-squash, so the k is
-- gone for good: squash-elim reaches only propositions, and a
-- CONSTRUCTION needs the k. That single line (Real/lt.nova:35) is the
-- only place in the ℕ→ℝ tower where truncation hides something a
-- construction wants; everywhere else the payload is consumed by
-- propositions, or the relation must be Ω because a quotient's must.
--
-- So positivity is repackaged here, in the bracket instead of the
-- squash:
--
--   PosR x ≜ Br ((k : ℕ) × prfC (LeR (realOfQ (qInvNat k)) x))
--
-- `class` retains its representative, so brElim lands in arbitrary
-- types — the k comes back, at the price of proving the result
-- independent of it. That price is exactly the theorem one owes
-- anyway to call the result a function of x.
--
-- PosR x → (LtR realZero x) holds; the converse does not, and
-- cannot. That asymmetry is the constructive content: knowing
-- propositionally that x is positive genuinely does not hand you a
-- rate.
-- ℝ's quotient is EFFECTIVE: equal classes have related
-- representatives. Proved the usual way — transport reqRefl along the
-- class equation, through a motive built by quot-elim into Ω.

import Core.prop (⊤, propExt)
import Rat (Q, +, *, qNeg, qZero, qOne, qAddAssoc, qAddZeroL, qAddZeroR, qAddNegL, qAddNegR, qMulComm, qMulOneL, qNegNeg, qDistribR)
import Rat.order (≤, leQTrans, leQMulMono, leQPlusMono)
import Rat.bound (Bnd, bndEq, bndZero, bndOfBothLe, leQSelfAdd, leQNegFlip, qNegZeroQ)
import Rat.max (qMax, qMaxLub, leQMaxL, leQMaxR, bndMaxSub)
import Rat.arch (leQSubShift, leQAddShift, leQUnsquash)
import Rat.half (dbl, qInvHalf, leQZeroInvNat)
import Rat.nat (qOfNat, qOfNatOne, leQOfNat)
import Rat.sqrt (qMulInvNat, qInvNatMulIdx)
import Natural.order (≤, leZero, leSucMono)
import Real (Real, RSeq, REq, Regular, qInvNat, rBound, leQZeroBound, realOfQ, realZero, constReg)
import Real.neg (seqOf, regOf, regBnd, bndReg, reqOf, reqRefl, reqSym, realEqOfREq)
import Real.order (≤, leRCls)
import Real.eq (reqTrans)
import Real.lt (<, ltROf)
import Real.add (+, realAddZeroL)
import Real.mul (mulIdx)
import Core.bracket (Br, br, brElim, brIsProp, brToSquash)
import Core.propCode (prfC, prfIntro, prfElim)
import Core.id (Id, idToEq, eqToId)
import Core.equality (trans, sym, cong, transport, transportP)

reqCongR : (p y y' : RSeq) → REq y y' → REq p y ≡ REq p y'
reqCongR = λp y y' h. propExt (λa. reqTrans _ a h) (λa. reqTrans _ a (reqSym h))

reqAt : RSeq → Real → Ω
  using (Real.REq.unfold, Real.RSeq.unfold, Real.Real.unfold, Real.Regular.unfold, reqCongR)
reqAt = λp z. quot-elim (y. REq p y) z

reqOfClassEq : {p p' : RSeq} → (class p ≡ class p' ∈ Real) → REq p p'
  using (Real.RSeq.unfold, Real.Real.unfold, Real.Regular.unfold, Real.REq.unfold, reqAt.eq)
reqOfClassEq = λp p' e. transportP (λz. reqAt p z) e reqRefl

-- THE WITNESS. It carries a representative as well as the modulus.
-- Not decoration: without it the descent needs a quot-elim on x whose
-- motive mentions the payload type, and the resulting obligation is a
-- rewrite underneath prfC — a path the kernel refuses to replay (B-1).
-- With the representative inside, √ is ONE elimination.
PosPayload : Real → 𝕌 using (Real.RSeq.unfold, Real.Real.unfold, Real.Regular.unfold)
PosPayload = λx. (p : RSeq) (k : ℕ) × prfC (realOfQ (qInvNat k) ≤ x) × Id _ (class p) x

PosR : Real → 𝕌
PosR = λx. Br (PosPayload x)

posMk : (x : Real) (p : RSeq) (k : ℕ) → (class p ≡ x) → realOfQ (qInvNat k) ≤ x → PosR x
  using (PosPayload.unfold, PosR.eq, Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold)
posMk = λx p k e h. br (p, k, prfIntro h, eqToId _ _ e)

posRep : (x : Real) → PosPayload x → RSeq using (PosPayload.unfold)
posRep = λx d. d .π₁

posK : (x : Real) → PosPayload x → ℕ using (PosPayload.unfold)
posK = λx d. d .π₂ .π₁

posBound : {x : Real} {d : PosPayload x} → realOfQ (qInvNat (posK _ d)) ≤ x
  using (PosPayload.unfold, posK.eq)
posBound = λx d. prfElim (realOfQ (qInvNat (d .π₂ .π₁)) ≤ x) (d .π₂ .π₂ .π₁)

posRepEq : (x : Real) (d : PosPayload x) → class (posRep _ d) ≡ x
  using (PosPayload.unfold, posRep.eq, Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold)
posRepEq = λx d. idToEq _ (class (d .π₁)) _ (d .π₂ .π₂ .π₂)

-- the bound, read at the payload's own representative
posBoundRep : (x : Real) (d : PosPayload x) → realOfQ (qInvNat (posK _ d)) ≤ class (posRep _ d)
  using (Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold)
posBoundRep =
  λx d. transportP (λv. realOfQ (qInvNat (posK _ d)) ≤ v) (sym _ _ (posRepEq _ d)) posBound

-- the bracket implies the squash — one way only
posToLt : (x : Real) → PosR x → realZero < x using (PosPayload.unfold, PosR.eq, posK.eq)
posToLt =
  λx w. squash-elim
    brToSquash w
    d. ltROf
      _
      _
      _
      transportP (λv. v ≤ x) (sym _ _ (realAddZeroL (realOfQ (qInvNat (posK x d))))) posBound

-- ===== turning the modulus into a ℚ-level fact, as DATA =====
leQZeroOfSubLe : (a u : Q) → a + qNeg u ≤ a → qZero ≤ u
leQZeroOfSubLe =
  λa u h. transport
    λw. w ≤ u
    qAddNegR a
    leQSubShift
      _
      _
      transport
        λw. w ≤ a + u
        trans
          _
          _
          _
          qAddAssoc a (qNeg u) u
          trans _ _ _ (cong (λw. Q) (λw. a + w) (qAddNegL u)) (qAddZeroR a)
        leQPlusMono u h

leQOneInv : (i : ℕ) → qInvNat i ≤ qOne
leQOneInv =
  λi. transport
    λw. w ≤ qOne
    qMulOneL (qInvNat i)
    transport
      λw. qOne * qInvNat i ≤ w
      {qOfNat (S i) * qInvNat i}
      {qOne}
      qMulInvNat
      leQMulMono
        _
        _
        transport (λw. w ≤ qOfNat (S i)) qOfNatOne (leQOfNat (leSucMono (leZero i)))
        leQZeroInvNat i

-- at a sample of the form mulIdx (dbl k) i the harmonic bound is
-- 1/(k+1) times 1/(i+1) — exactly, so it sits under 1/(k+1)
rBoundDeepEq : (k i : ℕ) → rBound (mulIdx (dbl k) i) (mulIdx (dbl k) i) ≡ qInvNat k * qInvNat i
  using (Real.rBound.eq)
rBoundDeepEq =
  λk i. trans
    qInvNat (mulIdx (dbl k) i) + qInvNat (mulIdx (dbl k) i)
    _
    _
    cong
      λw. Q
      λw. w + w
      {qInvNat (mulIdx (dbl k) i)}
      {qInvNat (dbl k) * qInvNat i}
      qInvNatMulIdx
    trans
      _
      _
      _
      sym _ _ (qDistribR (qInvNat i) (qInvNat (dbl k)) (qInvNat (dbl k)))
      cong (λw. Q) (λw. w * qInvNat i) (qInvHalf k)

leQRBoundDeep : (k i : ℕ) → rBound (mulIdx (dbl k) i) (mulIdx (dbl k) i) ≤ qInvNat k
leQRBoundDeep =
  λk i. transport
    λw. w ≤ qInvNat k
    sym _ _ (rBoundDeepEq k i)
    transport
      λw. w ≤ qInvNat k
      qMulComm (qInvNat i) (qInvNat k)
      transport
        λw. qInvNat i * qInvNat k ≤ w
        qMulOneL (qInvNat k)
        leQMulMono _ _ (leQOneInv i) (leQZeroInvNat k)

-- THE extraction: at every sample of the form mulIdx (dbl k) i the
-- representative is nonnegative, and that fact is DATA — recovered
-- from the Ω-level bound because ≤ on ℚ is decidable (leQUnsquash).
posSampleNN : (p : RSeq)
  (k : ℕ)
  → realOfQ (qInvNat k) ≤ class p → (i : ℕ) → qZero ≤ seqOf p (mulIdx (dbl k) i)
  using (Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.realOfQ.eq,
    Real.constReg.eq,
    Real.order.≤.eq,
    Real.order.RLeP.eq,
    Real.neg.seqOf.eq)
posSampleNN =
  λp k h i. leQUnsquash
    _
    squash-elim
      h
      u. ⋆
        leQZeroOfSubLe
          _
          _
          leQTrans
            qInvNat k + qNeg (seqOf p (mulIdx (dbl k) i))
            _
            _
            u (mulIdx (dbl k) i)
            leQRBoundDeep k i

-- ===== NONNEGATIVITY, as a nonnegative PRESENTATION =====
--
-- √ does not need separation from zero; it needs its SAMPLES to be
-- nonnegative. Strict positivity is one way to arrange that (sample
-- deep enough and PosR's modulus makes p_j ≥ 1/(2(k+1))), but not the
-- only way, and not the best: it excludes 0, which is in √'s domain.
--
-- A real is nonnegative exactly when it has a representative that is
-- POINTWISE nonnegative, and that presentation is pure data — LeQ and
-- Id are codes. Bracketed, it is the witness √ actually wants.
--
-- The clamp lives here, in nonNegMk, and nowhere else: given x ≥ 0 and
-- any representative, max(·,0) is regular, pointwise nonnegative, and
-- REq to the original precisely because x ≥ 0 gives p_n ≥ −rBound n n.
NonNegPayload : Real → 𝕌 using (Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold)
NonNegPayload = λx. (p : RSeq) × ((n : ℕ) → qZero ≤ seqOf p n) × Id _ (class p) x

NonNegR : Real → 𝕌
NonNegR = λx. Br (NonNegPayload x)

nnRep : (x : Real) → NonNegPayload x → RSeq using (NonNegPayload.unfold)
nnRep = λx d. d .π₁

nnAt : (x : Real) (d : NonNegPayload x) (n : ℕ) → qZero ≤ seqOf (nnRep _ d) n
  using (NonNegPayload.unfold, nnRep.eq)
nnAt = λx d n. d .π₂ .π₁ n

nnRepEq : (x : Real) (d : NonNegPayload x) → class (nnRep _ d) ≡ x
  using (NonNegPayload.unfold, nnRep.eq, Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold)
nnRepEq = λx d. idToEq _ (class (d .π₁)) _ (d .π₂ .π₂)

-- ===== the clamp =====
bndClamp : (b u : Q) → qZero ≤ b → qNeg b ≤ u → Bnd b (qMax u qZero + qNeg u)
bndClamp =
  λb u hb hu. bndOfBothLe
    _
    _
    leQSubShift
      _
      _
      qMaxLub (leQSelfAdd u hb) (transport (λw. w ≤ u + b) (qAddNegL b) (leQPlusMono b hu))
    leQSubShift _ _ (leQTrans _ _ _ (leQMaxL u qZero) (leQSelfAdd (qMax u qZero) hb))

bndZeroSub : {b : Q} → qZero ≤ b → Bnd b (qZero + qNeg qZero)
bndZeroSub =
  λb hb. bndEq
    _
    _
    sym _ _ (trans _ _ _ (cong (λw. Q) (λw. qZero + w) qNegZeroQ) (qAddZeroR qZero))
    bndZero _ hb

clampSeq : RSeq → ℕ → Q
clampSeq = λp n. qMax (seqOf p n) qZero

clampReg : {p : RSeq} → Regular (clampSeq p) using (clampSeq.eq)
clampReg =
  λp. bndReg (λm n. bndMaxSub _ _ _ _ _ (regBnd _ (regOf p) m n) (bndZeroSub (leQZeroBound m n)))

clampRSeq : RSeq → RSeq using (Real.RSeq.unfold)
clampRSeq = λp. clampSeq p, clampReg

clampNN : (p : RSeq) (n : ℕ) → qZero ≤ seqOf (clampRSeq p) n
  using (Real.RSeq.unfold, clampRSeq.eq, clampSeq.eq, Real.neg.seqOf.eq)
clampNN = λp n. leQMaxR (seqOf p n) qZero

-- the clamp changes nothing, precisely because x ≥ 0
clampREq : {p : RSeq} → realZero ≤ class p → REq (clampRSeq p) p
  using (Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.REq.unfold,
    Real.realZero.eq,
    Real.realOfQ.eq,
    Real.constReg.eq,
    Real.order.≤.eq,
    Real.order.RLeP.eq,
    Real.neg.seqOf.eq,
    clampRSeq.eq,
    clampSeq.eq)
clampREq =
  λp h. squash-elim
    h
    u. reqOf
      _
      _
      λn. bndClamp
        _
        _
        leQZeroBound n n
        transport
          λw. qNeg (rBound n n) ≤ w
          qNegNeg (seqOf p n)
          leQNegFlip _ _ (transport (λw. w ≤ rBound n n) (qAddZeroL (qNeg (seqOf p n))) (u n))

nonNegMk : (x : Real) (p : RSeq) → (class p ≡ x) → realZero ≤ x → NonNegR x
  using (NonNegPayload.unfold, NonNegR.eq, Real.Real.unfold, Real.RSeq.unfold, Real.Regular.unfold)
nonNegMk =
  λx p e h. br
    (,)
      clampRSeq p
      clampNN p
      eqToId
        _
        _
        trans _ _ _ (realEqOfREq _ _ (clampREq (transportP (λv. realZero ≤ v) (sym _ _ e) h))) e