pith. machine review for the scientific record. sign in
theorem proved term proof

trajectory_defect_monotone

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 403theorem trajectory_defect_monotone {N : ℕ}
 404    (traj : Trajectory N)
 405    (h : IsVariationalTrajectory traj) :
 406    ∀ t, total_defect (traj (t + 1)) ≤ total_defect (traj t) :=

proof body

Term-mode proof.

 407  fun t => variational_step_reduces_defect (traj t) (traj (t + 1)) (h t)
 408
 409/-! ## Global Consistency: Non-Locality of the Update -/
 410
 411/-- **Structure (Localized Update)**: An update that modifies only one entry,
 412    holding all others fixed. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.