Unfolding of the state law: for a single state it is the exit law rescaled by `1 / (1 - returnWeight c)`, and for a crossing state it is the exit law itself.

import Definitions.Def_TypeDensity_Basic
import Definitions.Def_TypeDensity_Formula_LawAlgebra
import Definitions.Def_TypeDensity_Formula_StateCombinatorics
import Theorems.Thm_TypeDensity_children_valid
import Theorems.Thm_TypeDensity_nonself_child_rank_lt
import Theorems.Thm_TypeDensity_state_fuel_stable
import Mathlib.FieldTheory.RatFunc.Basic
import Mathlib.MeasureTheory.Measure.Haar.Unique
import Mathlib.NumberTheory.ArithmeticFunction.Moebius
import Mathlib.NumberTheory.Padics.PadicIntegers
import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
import Mathlib.RingTheory.MvPowerSeries.Basic
import Mathlib.RingTheory.RamificationInertia.Basic
import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
import Mathlib.FieldTheory.Finite.GaloisField
import Mathlib.RingTheory.AdicCompletion.Algebra
import Mathlib.RingTheory.RegularLocalRing.Defs
set_option autoImplicit false

open TypeDensity
open scoped BigOperators ENNReal

theorem TypeDensity.state_law_unfold (s : State) (hs : s.Valid) (hnt : s.terminal = false) :
    (∀ a c : ℕ, s = State.single a c → stateLaw s =
      lawScale (.inv (.sub (.const 1) (returnWeight c))) (exitLaw s)) ∧
      (∀ a b c h : ℕ, s = State.crossing a b c h → stateLaw s = exitLaw s) := by sorry