Equation (1): optimal second-stage production

Proved

CarbonPolicy.TaxVsCap.optimal_quantity

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

cap-and-tradecarbon-taxcorrelated-uncertaintyp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1technology-investment

For a positive demand sensitivity $b$ , fixed emission intensity $\gamma$ , realized market potential $a$ , permit price $k$ , and quota $w$ , the firm's operating profit is maximized over all real production quantities by

q^*(\gamma,a,k)=\frac{a-\gamma k}{2b}.

This identifies the second-stage response used in both first-stage policy objectives.

Formalization Note The maximization is over all real $q$ , as in the paper's unconstrained $\max_q$ .

Preamble

import Mathlib
import Definitions.Def_CarbonPolicy_TaxVsCap_Setting

open ProbabilityTheory MeasureTheory

Formal statement

namespace CarbonPolicy.TaxVsCap

theorem optimal_quantity (b w γ a k : ℝ) (hb : 0 < b) :
    ∀ q : ℝ, profit b w γ a k q ≤ profit b w γ a k (qStar b γ a k) := by sorry

end CarbonPolicy.TaxVsCap

Source

Fan, Chen, Chen, Is Price Commitment a Better Solution to Control Carbon Emissions and Promote Technology Investment?, SSRN 3817235 (version of November 15, 2021), p. 12, equation (1)

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph