/-
Per-run certificates: each published run satisfies the whole specification, hence every claim is reached from
its tree's origin along the drawn branches. The instance checks evaluate the decidable specification with Lean's
compiled evaluator (`native_decide`); the theorems in `Growth.Theorems` are kernel-checked.
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-/
import Growth.Theorems
import Growth.RunA
import Growth.RunB
import Growth.RunC
import Growth.RunD
import Growth.RunE
import Growth.RunF
import Growth.RunG
import Growth.RunH
import Growth.RunI
import Growth.RunJ
import Growth.RunK
import Growth.RunL
import Growth.RunM
import Growth.RunN
import Growth.RunO
import Growth.RunP
import Growth.RunQ
import Growth.RunR
import Growth.RunS
import Growth.RunT
import Growth.RunU
import Growth.RunV
import Growth.RunW
import Growth.RunX
import Growth.RunY

set_option maxRecDepth 100000
set_option maxHeartbeats 0

namespace Growth
open Run

theorem runA_valid : runA.Valid := by native_decide
theorem runA_reached : ∀ i, i < runA.claims.length → runA.start (runA.own i) ≤ runA.d i ∧
    runA.Walk (runA.pt (runA.origin (runA.own i))) (runA.pt i) (runA.d i - runA.start (runA.own i)) :=
  reached runA_valid.1 runA_valid.2.1

theorem runB_valid : runB.Valid := by native_decide
theorem runB_reached : ∀ i, i < runB.claims.length → runB.start (runB.own i) ≤ runB.d i ∧
    runB.Walk (runB.pt (runB.origin (runB.own i))) (runB.pt i) (runB.d i - runB.start (runB.own i)) :=
  reached runB_valid.1 runB_valid.2.1

theorem runC_valid : runC.Valid := by native_decide
theorem runC_reached : ∀ i, i < runC.claims.length → runC.start (runC.own i) ≤ runC.d i ∧
    runC.Walk (runC.pt (runC.origin (runC.own i))) (runC.pt i) (runC.d i - runC.start (runC.own i)) :=
  reached runC_valid.1 runC_valid.2.1

theorem runD_valid : runD.Valid := by native_decide
theorem runD_reached : ∀ i, i < runD.claims.length → runD.start (runD.own i) ≤ runD.d i ∧
    runD.Walk (runD.pt (runD.origin (runD.own i))) (runD.pt i) (runD.d i - runD.start (runD.own i)) :=
  reached runD_valid.1 runD_valid.2.1

theorem runE_valid : runE.Valid := by native_decide
theorem runE_reached : ∀ i, i < runE.claims.length → runE.start (runE.own i) ≤ runE.d i ∧
    runE.Walk (runE.pt (runE.origin (runE.own i))) (runE.pt i) (runE.d i - runE.start (runE.own i)) :=
  reached runE_valid.1 runE_valid.2.1

theorem runF_valid : runF.Valid := by native_decide
theorem runF_reached : ∀ i, i < runF.claims.length → runF.start (runF.own i) ≤ runF.d i ∧
    runF.Walk (runF.pt (runF.origin (runF.own i))) (runF.pt i) (runF.d i - runF.start (runF.own i)) :=
  reached runF_valid.1 runF_valid.2.1

theorem runG_valid : runG.Valid := by native_decide
theorem runG_reached : ∀ i, i < runG.claims.length → runG.start (runG.own i) ≤ runG.d i ∧
    runG.Walk (runG.pt (runG.origin (runG.own i))) (runG.pt i) (runG.d i - runG.start (runG.own i)) :=
  reached runG_valid.1 runG_valid.2.1

theorem runH_valid : runH.Valid := by native_decide
theorem runH_reached : ∀ i, i < runH.claims.length → runH.start (runH.own i) ≤ runH.d i ∧
    runH.Walk (runH.pt (runH.origin (runH.own i))) (runH.pt i) (runH.d i - runH.start (runH.own i)) :=
  reached runH_valid.1 runH_valid.2.1

theorem runI_valid : runI.Valid := by native_decide
theorem runI_reached : ∀ i, i < runI.claims.length → runI.start (runI.own i) ≤ runI.d i ∧
    runI.Walk (runI.pt (runI.origin (runI.own i))) (runI.pt i) (runI.d i - runI.start (runI.own i)) :=
  reached runI_valid.1 runI_valid.2.1

theorem runJ_valid : runJ.Valid := by native_decide
theorem runJ_reached : ∀ i, i < runJ.claims.length → runJ.start (runJ.own i) ≤ runJ.d i ∧
    runJ.Walk (runJ.pt (runJ.origin (runJ.own i))) (runJ.pt i) (runJ.d i - runJ.start (runJ.own i)) :=
  reached runJ_valid.1 runJ_valid.2.1

theorem runK_valid : runK.Valid := by native_decide
theorem runK_reached : ∀ i, i < runK.claims.length → runK.start (runK.own i) ≤ runK.d i ∧
    runK.Walk (runK.pt (runK.origin (runK.own i))) (runK.pt i) (runK.d i - runK.start (runK.own i)) :=
  reached runK_valid.1 runK_valid.2.1

theorem runL_valid : runL.Valid := by native_decide
theorem runL_reached : ∀ i, i < runL.claims.length → runL.start (runL.own i) ≤ runL.d i ∧
    runL.Walk (runL.pt (runL.origin (runL.own i))) (runL.pt i) (runL.d i - runL.start (runL.own i)) :=
  reached runL_valid.1 runL_valid.2.1

theorem runM_valid : runM.Valid := by native_decide
theorem runM_reached : ∀ i, i < runM.claims.length → runM.start (runM.own i) ≤ runM.d i ∧
    runM.Walk (runM.pt (runM.origin (runM.own i))) (runM.pt i) (runM.d i - runM.start (runM.own i)) :=
  reached runM_valid.1 runM_valid.2.1

theorem runN_valid : runN.Valid := by native_decide
theorem runN_reached : ∀ i, i < runN.claims.length → runN.start (runN.own i) ≤ runN.d i ∧
    runN.Walk (runN.pt (runN.origin (runN.own i))) (runN.pt i) (runN.d i - runN.start (runN.own i)) :=
  reached runN_valid.1 runN_valid.2.1

theorem runO_valid : runO.Valid := by native_decide
theorem runO_reached : ∀ i, i < runO.claims.length → runO.start (runO.own i) ≤ runO.d i ∧
    runO.Walk (runO.pt (runO.origin (runO.own i))) (runO.pt i) (runO.d i - runO.start (runO.own i)) :=
  reached runO_valid.1 runO_valid.2.1

theorem runP_valid : runP.Valid := by native_decide
theorem runP_reached : ∀ i, i < runP.claims.length → runP.start (runP.own i) ≤ runP.d i ∧
    runP.Walk (runP.pt (runP.origin (runP.own i))) (runP.pt i) (runP.d i - runP.start (runP.own i)) :=
  reached runP_valid.1 runP_valid.2.1

theorem runQ_valid : runQ.Valid := by native_decide
theorem runQ_reached : ∀ i, i < runQ.claims.length → runQ.start (runQ.own i) ≤ runQ.d i ∧
    runQ.Walk (runQ.pt (runQ.origin (runQ.own i))) (runQ.pt i) (runQ.d i - runQ.start (runQ.own i)) :=
  reached runQ_valid.1 runQ_valid.2.1

theorem runR_valid : runR.Valid := by native_decide
theorem runR_reached : ∀ i, i < runR.claims.length → runR.start (runR.own i) ≤ runR.d i ∧
    runR.Walk (runR.pt (runR.origin (runR.own i))) (runR.pt i) (runR.d i - runR.start (runR.own i)) :=
  reached runR_valid.1 runR_valid.2.1

theorem runS_valid : runS.Valid := by native_decide
theorem runS_reached : ∀ i, i < runS.claims.length → runS.start (runS.own i) ≤ runS.d i ∧
    runS.Walk (runS.pt (runS.origin (runS.own i))) (runS.pt i) (runS.d i - runS.start (runS.own i)) :=
  reached runS_valid.1 runS_valid.2.1

theorem runT_valid : runT.Valid := by native_decide
theorem runT_reached : ∀ i, i < runT.claims.length → runT.start (runT.own i) ≤ runT.d i ∧
    runT.Walk (runT.pt (runT.origin (runT.own i))) (runT.pt i) (runT.d i - runT.start (runT.own i)) :=
  reached runT_valid.1 runT_valid.2.1

theorem runU_valid : runU.Valid := by native_decide
theorem runU_reached : ∀ i, i < runU.claims.length → runU.start (runU.own i) ≤ runU.d i ∧
    runU.Walk (runU.pt (runU.origin (runU.own i))) (runU.pt i) (runU.d i - runU.start (runU.own i)) :=
  reached runU_valid.1 runU_valid.2.1

theorem runV_valid : runV.Valid := by native_decide
theorem runV_reached : ∀ i, i < runV.claims.length → runV.start (runV.own i) ≤ runV.d i ∧
    runV.Walk (runV.pt (runV.origin (runV.own i))) (runV.pt i) (runV.d i - runV.start (runV.own i)) :=
  reached runV_valid.1 runV_valid.2.1

theorem runW_valid : runW.Valid := by native_decide
theorem runW_reached : ∀ i, i < runW.claims.length → runW.start (runW.own i) ≤ runW.d i ∧
    runW.Walk (runW.pt (runW.origin (runW.own i))) (runW.pt i) (runW.d i - runW.start (runW.own i)) :=
  reached runW_valid.1 runW_valid.2.1

theorem runX_valid : runX.Valid := by native_decide
theorem runX_reached : ∀ i, i < runX.claims.length → runX.start (runX.own i) ≤ runX.d i ∧
    runX.Walk (runX.pt (runX.origin (runX.own i))) (runX.pt i) (runX.d i - runX.start (runX.own i)) :=
  reached runX_valid.1 runX_valid.2.1

theorem runY_valid : runY.Valid := by native_decide
theorem runY_reached : ∀ i, i < runY.claims.length → runY.start (runY.own i) ≤ runY.d i ∧
    runY.Walk (runY.pt (runY.origin (runY.own i))) (runY.pt i) (runY.d i - runY.start (runY.own i)) :=
  reached runY_valid.1 runY_valid.2.1

end Growth