proposition. A compute bound from financed expenditure [ftip-00O9]
✍️source

    If Definition [ftip-00O8] holds and \(p(t)\geq p_*>0\), then

    \[\int _0^T u(t)\,dt\leq \frac {b_0+F}{p_*}.\]

    Proof. 

      Integration of the balance sheet gives

      \[\int _0^T p(t)u(t)\,dt =b_0-b(T)+\int _0^T f(t)\,dt-\int _0^T o(t)\,dt \leq b_0+F.\]

      Apply the price lower bound. If the premises hold uniformly almost surely, the same bound holds for the hard envelope over all executions.

      This establishes the financing term in proposition [ftip-00O2] from an explicit account. It does not derive \(F\) from aggregate output or welfare. A concrete model must establish the inflow bound while admitting its actual investment, borrowing and redistribution mechanisms.