PhysicalRefinementLocality.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Locality of the complete physical refinement

Changing selection streams above a fixed level cannot alter histories at that level or below. This proves the fixed-child environment under parent-only resampling directly from the executable recurrence.

theorem OAI.EditApproximation.physicalRefinement_congr_from_level line 17

Source documentation

The complete history depends only on selection functions at its own physical level and deeper levels.

theorem physicalRefinement_congr_from_level {α : Type*} [DecidableEq α] {M J : ℕ}
    (source target : List α) (U : PhysicalEntry M J target.length → ℕ)
    (N P F : ℕ) (A : ℚ) (T : ℕ) (delta : ℚ)
    (first second : PhysicalSelections M J source.length target.length P
      (stageRepresentatives source target U N P F A))
    (d : ℕ) (hgroups : ∀ node, d ≤ node.1.val → first.groups node = second.groups node)
    (honline : ∀ node, d ≤ node.1.val → first.online node = second.online node)
    (node : PhysicalNode M J) (hnode : d ≤ node.1.val) (t : ℕ) (q : TargetInterval target.length) :
    physicalRefinement source target U N P F A T delta first node t q =
      physicalRefinement source target U N P F A T delta second node t q := by
…

Mentions: OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.PhysicalSelections, OAI.EditApproximation.stageRepresentatives, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.physicalRefinement

theorem OAI.EditApproximation.physicalRefinement_children_fixed line 57

Source documentation

Parent-only resampling fixes every child table, at every refinement index and target state, without independence assumptions about children.

theorem physicalRefinement_children_fixed {α : Type*} [DecidableEq α] {M J : ℕ}
    (source target : List α) (U : PhysicalEntry M J target.length → ℕ)
    (N P F : ℕ) (A : ℚ) (T : ℕ) (delta : ℚ)
    (first second : PhysicalSelections M J source.length target.length P
      (stageRepresentatives source target U N P F A))
    (node : PhysicalNode M J) (hbelow : node.1.val < J)
    (hgroups : ∀ label, node.1.val < label.1.val → first.groups label = second.groups label)
    (honline : ∀ label, node.1.val < label.1.val → first.online label = second.online label) :
    (fun i : Fin M => physicalRefinement source target U N P F A T delta first (physicalChild node hbelow i)) =
      fun i : Fin M => physicalRefinement source target U N P F A T delta second (physicalChild node hbelow i) := by
…

Mentions: OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.PhysicalSelections, OAI.EditApproximation.stageRepresentatives, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.physicalRefinement, OAI.EditApproximation.physicalChild