OAI/Combinatorics/EditApproximation/Refinement/PhysicalProgramRefreshWiring.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact candidate wiring and complete-child locality under actual two-key refresh.

  1. theorem OAI.EditApproximation.physicalProgramRefresh_history line 35

    Source documentation

    Complete child histories remain fixed under replacement of the two actual random arrays at this parent.

    theorem physicalProgramRefresh_history (draw : Draw) (fresh : Fresh) :
    physicalBandHistory source target U N P F A T delta (choices (refresh draw onlineKey groupKey fresh)) node.1 node.2 =
      physicalBandHistory source target U N P F A T delta (choices draw) node.1 node.2 := by
…

    Mentions: OAI.EditApproximation.physicalBandHistory

  2. theorem OAI.EditApproximation.physicalProgramRefresh_clipped line 47
  3. theorem OAI.EditApproximation.physicalProgramRefresh_online_mem line 59

    Source documentation

    The literal online slot supplies the reference-environment sampler at the refreshed integer; no candidate-list premise remains.

    theorem physicalProgramRefresh_online_mem (draw : Draw) (fresh : Fresh)
    (member : UnskippedBand source target (physicalSourceInterval source.length node.1)
      b P thetaExponent tau F
      (physicalBandChildMassTable source target U N P F A T node.1 node.2)
      (physicalBandChildInitial source target U N P F A node.1 node.2))
    (hget : (stageRepresentatives source target U N P F A node.1).get representative = (b, member.center))
    (t : ℕ) (q : TargetInterval target.length)
    (hquery : physicalProgramOnlineGuard source target U N P F A node.1 q (b, member.center)) :
    sharedBandRationalAction member.center
      (physicalBandOnlineDraw source target U N P F A T delta (choices draw) node.1 node.2
        b thetaExponent tau member.center member.nonempty η κ G K t (parentOnlineDraw fresh t)) ∈
      physicalNodeOnline source target U N P F A T delta
…

    Mentions: OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.physicalSourceInterval, OAI.EditApproximation.physicalBandChildMassTable, OAI.EditApproximation.physicalBandChildInitial, OAI.EditApproximation.stageRepresentatives, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.physicalProgramOnlineGuard, OAI.EditApproximation.sharedBandRationalAction, OAI.EditApproximation.physicalBandOnlineDraw, OAI.EditApproximation.parentOnlineDraw, OAI.EditApproximation.physicalNodeOnline

  4. theorem OAI.EditApproximation.physicalProgramRefresh_group_mem line 91

    Source documentation

    The literal whole-cell slot supplies the selected group computed from the unchanged complete child environment and refreshed shared arrays.

    theorem physicalProgramRefresh_group_mem (draw : Draw) (fresh : Fresh)
    (hnonempty : physicalNodeCellBands source target U N P F A T node.1 node.2 b thetaExponent tau groupCell ≠ [])
    (t : ℕ) :
    (physicalNodeSelectedGroup source target U N P F A T delta (choices draw) node.1 node.2
      b thetaExponent Q tau groupCell hnonempty t (parentGroupDraw fresh t)).rationalAction ∈
      physicalNodeGroups source target U N P F A T delta
        (choices (refresh draw onlineKey groupKey fresh)) node.1 node.2 t := by
…

    Mentions: OAI.EditApproximation.physicalNodeCellBands, OAI.EditApproximation.physicalNodeSelectedGroup, OAI.EditApproximation.parentGroupDraw, OAI.EditApproximation.physicalNodeGroups