The Flappy Condor

§1. The Flappy Condor

An iron condor holds credit spreads on both sides of the current price: a bull put spread below spot and a bear call spread above spot. The position earns theta (time decay) as long as spot stays within the short strikes.

The Flappy Condor adds dynamic management. It opens and closes spreads to maintain portfolio theta in a target band, adjusts aggression based on the implied vol regime, and closes positions when spot approaches the short strike. The "flapping" is the continuous adjustment. Without it, you get blown up.

The system is a Phase Lock Loop (PLL):

§2. The State Machine — Control Law v3

The original control law (v1) had only the theta band: Open below floor, Close above ceiling, Hold in band. This is vulnerable to the Woodchipper.

Control law v3 adds a Cooldown state. When a spread is closed, its short strike is banned from the Kelly open selector for 60 minutes. This breaks the degenerate cycle.

inductive Action | Open | Close | Hold | Cooldown

def controlLaw3
    (θ θ_L θ_H : ℚ)
    (is_banned : Bool)     -- true if strike was recently closed
    (yoga_close : Bool)    -- true if |S - K_short| < δ_min
    : Action :=
  if is_banned then .Cooldown          -- layer 1: hysteresis
  else if yoga_close then .Close       -- layer 2: yoga override
  else if θ < θ_L then .Open          -- layer 3: theta band
  else if θ > θ_H then .Close
  else .Hold

Implementation: CooldownCache in pll.rs — HashMap<String, Instant> with 60-minute TTL. Key format: "{strike}{C|P}". Ban on close submission (pre-ban) and reinforced on fill.

§3. The Anti-Woodchipper Theorem

Statement: If a strike is banned, the control law cannot output Open.

-- Banned strikes NEVER produce Open
theorem anti_woodchipper
    (θ θ_L θ_H : ℚ) (yoga_close : Bool) :
    controlLaw3 θ θ_L θ_H true yoga_close ≠ .Open := by
  simp [controlLaw3]  ✓

-- Stronger: banned strikes ALWAYS produce Cooldown
theorem banned_implies_cooldown
    (θ θ_L θ_H : ℚ) (yoga_close : Bool) :
    controlLaw3 θ θ_L θ_H true yoga_close = .Cooldown := by
  simp [controlLaw3]  ✓

The proof is trivial by definition — which is the point. The safety property is baked into the type system. You cannot construct a code path where a banned strike opens a new position.

The hysteresis is purely additive — it doesn't change normal theta-band operation.

§4. Theta Band Convergence

The control law drives theta toward the target band from any starting position. Below floor, each fill adds $\delta\theta > 0$. By the Archimedean property of $\mathbb{Q}$, there exists $n \in \mathbb{N}$ such that $\theta + n \cdot \delta\theta \geq \theta_L$. Above ceiling: symmetric.

lemma convergence_from_below (θ θ_L δθ : ℚ) (hδ : δθ > 0) :
    ∃ n : ℕ, θ_L ≤ θ + ↑n * δθ := by
  obtain ⟨n, hn⟩ := Archimedean.arch (θ_L - θ) hδ
  exact ⟨n, by rw [nsmul_eq_mul] at hn; linarith⟩  ✓

lemma convergence_from_above (θ θ_H δθ : ℚ) (hδ : δθ > 0) :
    ∃ n : ℕ, θ - ↑n * δθ ≤ θ_H := by
  obtain ⟨n, hn⟩ := Archimedean.arch (θ - θ_H) hδ
  exact ⟨n, by rw [nsmul_eq_mul] at hn; linarith⟩  ✓

The band is quasi-invariant: exogenous shocks can eject theta from the band, but the controller restores it in finite steps. This is PLL lock recovery.

§5. Risk-Budget Partitioning — The Crown Jewel

This is the substantive theorem. It strictly separates financial modeling (axioms the operator must enforce) from execution logic (verified by the type system).

Statement. Given:

• $\Theta_{daily} > 0$ (portfolio theta, positive by band construction)
• $0 < \lambda < 1$ (budget split ratio)
• $L_\Gamma \leq \lambda \cdot \Theta_{daily}$ (gamma drag bounded by gamma budget)
• $C_{tx} \leq (1 - \lambda) \cdot \Theta_{daily}$ (costs bounded by cost budget)

Then: $\Theta_{daily} - L_\Gamma - C_{tx} \geq 0$

Proof: $\lambda\Theta + (1-\lambda)\Theta = \Theta$ (partition of unity). The sum of budgets equals total theta. The sum of actuals is bounded by the sum of budgets. QED.

theorem one_step_pnl_nonneg
    (Θ_daily L_Γ C_tx λ : ℚ)
    (hΘ : Θ_daily > 0)
    (hλ_pos : 0 < λ) (hλ_lt : λ < 1)
    (h_gamma_budget : L_Γ ≤ λ * Θ_daily)
    (h_cost_budget : C_tx ≤ (1 - λ) * Θ_daily) :
    Θ_daily - L_Γ - C_tx ≥ 0 := by
  have h_partition : λ * Θ_daily + (1 - λ) * Θ_daily = Θ_daily := by ring
  have h_sum := add_le_add h_gamma_budget h_cost_budget
  linarith  ✓

-- With vol edge: strictly better
theorem one_step_pnl_with_vol_edge
    (Θ_daily L_Γ C_tx V_edge λ : ℚ)
    -- ... same hypotheses ...
    (h_vol : V_edge ≥ 0) :
    Θ_daily - L_Γ - C_tx + V_edge ≥ 0  ✓

What this does NOT claim: it does not claim that any particular market regime will satisfy the budget constraints. The constraints are the operator's responsibility. The theorem verifies that the math connecting constraints to the guarantee is correct.

§6. Regime Filter

In SELL regime ($\sigma_{fc} < \sigma_{live}$), the market prices options above forecast realized vol. Debit spreads have negative edge by construction.

-- In SELL regime, model price < market price
theorem sell_regime_debit_edge_negative
    (σ_fc σ_live vega : ℚ)
    (h_sell : σ_fc < σ_live) (h_vega : vega > 0) :
    vega * σ_fc < vega * σ_live :=
  mul_lt_mul_of_pos_left h_sell h_vega  ✓

-- Negative-edge bets reduce wealth
theorem negative_edge_reduces_wealth
    (f edge : ℚ) (hf : 0 < f) (he : edge < 0) :
    1 + f * edge < 1 := by nlinarith  ✓

v1 had a logically explosive axiom (sell_regime_no_debit_edge) that was universally quantified over all $\mathbb{Q}$ and could prove $1 \leq 0$. In v3, everything is proved. No axioms. No sorry.

§7. Honest Failure Modes

The system CAN lose money. These theorems prove it. Intellectual honesty is a feature, not a bug.

• Regime inversion overwhelms theta. If vol moves against the position, theta cannot compensate. Machine-checked: $\Delta_\theta = 1450, \Delta_{vol} = -2000 \Rightarrow \Delta_\theta + \Delta_{vol} < 0$.
  Mitigation: close-only when τ < 0.001yr or when vol signal is stale.
• Gap risk exceeds theta. A 2σ+ move produces gamma drag exceeding theta. The yoga condition only helps for continuous moves — gaps bypass it entirely.
  Mitigation: position-level max loss cap (Kelly fraction below theoretical max).
• Yoga failure. Spot moves faster than system can close. PLL loses lock.
  Mitigation: δ_min triggers market-order close, not adaptive pricing.
• Vol forecast overfitting. σ_fc has no true predictive skill. Vol edge channel contributes noise.
  System still works (theta channel is model-free) but at reduced Sharpe.
• Liquidity withdrawal. Bid-ask widens 5-10× during flash crashes. Adaptive pricer can't fill when closing is most needed.
  Mitigation: market-order escalation when |S − K_short| < δ_min/2.

-- Regime inversion overwhelms theta
theorem regime_failure_can_overwhelm_theta
    (Δ_θ Δ_vol : ℚ) (hθ : Δ_θ = 1450) (hv : Δ_vol = -2000) :
    Δ_θ + Δ_vol < 0 := by subst hθ; subst hv; norm_num  ✓

-- Gap risk: 2σ gamma exceeds theta
theorem two_sigma_exceeds_theta (theta gamma_1σ : ℚ)
    (h_theta : theta > 0) (h_ratio : gamma_1σ > theta / 4) :
    4 * gamma_1σ > theta := by linarith  ✓

-- "Gains on all sides" is conditional, not absolute
theorem gains_conditional
    (Δ_θ Δ_vol Δ_roll Δ_adj : ℚ)
    (hθ : Δ_θ > 0) (hv : Δ_vol ≥ 0) (hr : Δ_roll ≥ 0) (ha : Δ_adj ≥ 0) :
    Δ_θ + Δ_vol + Δ_roll + Δ_adj > 0 := by linarith  ✓

§8. What Was Falsified

This section documents what we got wrong and how we found out. Worn as a badge of honor.

v1 → v2: Codex adversarial review

Three rounds with gpt-5.3-codex at xhigh reasoning effort. Pass 1 (35 critiques): logically explosive axiom, 16% localization without derivation. Pass 2: corrected to 46%, $6,850 gamma spike, 1.85× buffer. Pass 3: grade B-. Risk-budget theorem proposed and proved.

v2 → v3: Gemini 3 Deep Think

Gemini Deep Think falsified the continuous-time mathematics entirely:

What survived

The Flappy Condor is a theta harvester with a vol overlay, run by a formally verified state machine. It is not a proof that markets are profitable. It is a proof that the execution logic cannot destroy capital through its own control decisions.

What Lean 4 proves: The state machine cannot enter the Woodchipper. Risk budgets imply non-negative one-step P&L. The theta band restores in finite steps. The regime filter eliminates negative-edge bets. The system can lose money (and we prove how).

What Lean 4 does NOT prove: That any specific market condition will produce profit. That Black-Scholes dynamics favor short premium. Any specific numerical P&L. That the operator will successfully enforce budget constraints.

The name is accurate. It flaps. If it stops flapping, it falls.