Documentation

Lean 4 Proof

theorem boundary_indifference {J : ℕ} :
    specializationRatio J 1 = 1 := by
  simp [specializationRatio, sub_self, rpow_zero]

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:231

Module Section

Substitute Regime: The ρ > 1 Theory (Anti-Complementarity)

In the same file