MarkerJointHistory.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.markerEmbedding line 14
lemma OAI.DilutedSpinGlass.PrescribedTree.markerEmbedding_injective line 18

theorem OAI.DilutedSpinGlass.PrescribedTree.marker_history_augment line 25

Source documentation

Exact enlargement of the signed marker history by all the protected old paths. The matrix constraints force the added tree to separate before the old tree branches; no old-position branch is silently retained or discarded.

theorem marker_history_augment
    (S T Q : PrescribedTree n) (a : S.Leaf) (q : Option C → T.Leaf)
    (qold : S.Leaf → Q.Leaf) (qfresh : C → Q.Leaf)
    (hold : ∀ d e, splitDepth S d e=splitDepth Q (qold d) (qold e))
    (hmarker : ∀ x y : Option C,
      splitDepth T (q x) (q y)=
        splitDepth Q (Option.elim' (qold a) qfresh x) (Option.elim' (qold a) qfresh y))
    (hsep : ∀ c d, splitDepth Q (qfresh c) (qold a)<splitDepth Q (qold a) (qold d))
    (K : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (cs : List C) (hcs : cs.Nodup)
    (F : (S.Leaf → FinitePath Ω n) → ℝ) (A : (Option C → FinitePath Ω n) → ℝ) :
    weightedMatrixHistory T q
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory