Documentation

Lean 4 Proof

theorem anti_network_reversal (ρ : ℝ) (hρ : ρ < 0) :
    -- Cross-externalities saturate as participation grows;
    -- beyond a threshold, the platform should tax rather than subsidize.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:799

Module Section

## Network Scaling Results

In the same file