PhysicalSelectionProgram.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Finite online and whole-cell candidate programs

Physical selections use the representative and guarded band lists. Each band has its own finite optimizer stream; every whole cell has shared per-scale child streams. These streams define coherent finite tables.

def OAI.EditApproximation.physicalProgramBandG line 30
def OAI.EditApproximation.physicalProgramBandK line 36
theorem OAI.EditApproximation.physicalProgramBandG_spec line 40
theorem OAI.EditApproximation.physicalProgramBandG_ge_two line 52
theorem OAI.EditApproximation.physicalProgramBandK_positive line 58
def OAI.EditApproximation.physicalProgramCells line 65
def OAI.EditApproximation.physicalBandOnlineCandidate line 69
def OAI.EditApproximation.physicalProgramOnlineCandidate line 91
abbrev OAI.EditApproximation.PhysicalOnlineStreams line 102
abbrev OAI.EditApproximation.PhysicalGroupStreams line 107
def OAI.EditApproximation.physicalProgramOnlineGuard line 117
Source documentation
The literal online query uses its one rounded center at each allowed scale, with the scale window tested against the literal initial table.
```
def physicalProgramOnlineGuard (node : PhysicalNode M J) (q : TargetInterval target.length)
    (br : ℕ × TargetInterval target.length) : Prop :=
…
```
Mentions: OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval
instance OAI.EditApproximation.physicalProgramOnlineGuard_decidable line 123

theorem OAI.EditApproximation.physicalProgramOnlineGuard_comparison line 131

Source documentation

The actual dyadic comparison center passes the query filter on every good initial seed; no local scale premise is assumed.

theorem physicalProgramOnlineGuard_comparison
    (hsize : source.length + target.length ≤ N) (hP : 66 ≤ P) (hF : 1 ≤ F) (hA : 1 ≤ A)
    (hseed : ∀ state, stateEditCost (physicalSource source state.1) target state.2 ≤ U state ∧
      (U state : ℚ) ≤ A * stateEditCost (physicalSource source state.1) target state.2)
    (node : PhysicalNode M J) (q : TargetInterval target.length)
    (hc : 0 < stateEditCost (physicalSource source node) target q) :
    let b := 2 ^ Nat.log 2 (stateEditCost (physicalSource source node) target q)
…

Mentions: OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval

def OAI.EditApproximation.physicalProgramOnline line 167
def OAI.EditApproximation.physicalProgramGroups line 179

theorem OAI.EditApproximation.physicalProgramOnlineCandidate_wide line 199

Source documentation

Every produced online candidate is literally one of the parent wide actions.

theorem physicalProgramOnlineCandidate_wide (node : PhysicalInternalNode M J)
    (representative : Fin (representatives node.1).length) (children : PhysicalChildTables M target.length)
    (t : ℕ)
    (integer : Fin (optimizerTriangularMass
      (physicalProgramBandK source target U N P F A T thetaExponent H tau node representative)))
    (action : PhysicalRationalAction M target.length)
    (hselected : physicalProgramOnlineCandidate source target U N P F A T thetaExponent H tau η κ
      node representative children t integer = some action) :
    action ∈ rationalActualWideActions (physicalSourceInterval source.length node.1)
      (representatives node.1) P := by
…

Mentions: OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.physicalProgramBandK, OAI.EditApproximation.PhysicalRationalAction, OAI.EditApproximation.physicalProgramOnlineCandidate, OAI.EditApproximation.rationalActualWideActions, OAI.EditApproximation.physicalSourceInterval

theorem OAI.EditApproximation.physicalProgramOnline_wide line 222
theorem OAI.EditApproximation.physicalProgramGroups_wide line 237
def OAI.EditApproximation.physicalProgramSelections line 259
Source documentation
The actual complete selection interface contains exactly the finite online and shared whole-cell candidates produced by the streams.
```
def physicalProgramSelections {R : ℕ} [NeZero R]
    (online : PhysicalOnlineStreams source target U N P F A T thetaExponent H tau R)
    (groups : PhysicalGroupStreams source target U N P F A thetaExponent Q R) :
    PhysicalSelections M J source.length target.length P representatives where
…
```
Mentions: OAI.EditApproximation.PhysicalOnlineStreams, OAI.EditApproximation.PhysicalGroupStreams, OAI.EditApproximation.PhysicalSelections

theorem OAI.EditApproximation.physicalProgramOnlineCandidate_accepted line 269

Source documentation

An accepted literal band is retained in its online representative slot.

theorem physicalProgramOnlineCandidate_accepted (node : PhysicalInternalNode M J)
    (representative : Fin (representatives node.1).length) (b : ℕ)
    (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 : (representatives node.1).get representative = (b, member.center))
    (children : PhysicalChildTables M target.length) (t : ℕ)
    (integer : Fin (optimizerTriangularMass
      (physicalProgramBandK source target U N P F A T thetaExponent H tau node representative))) :
    physicalProgramOnlineCandidate source target U N P F A T thetaExponent H tau η κ
      node representative children t integer = some (sharedBandRationalAction member.center
…

Mentions: OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.physicalSourceInterval, OAI.EditApproximation.physicalBandChildMassTable, OAI.EditApproximation.physicalBandChildInitial, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.physicalProgramBandK, OAI.EditApproximation.physicalProgramOnlineCandidate, OAI.EditApproximation.sharedBandRationalAction

theorem OAI.EditApproximation.physicalProgramCells_complete line 294
Source documentation
Every eligible center contributes its whole cell to the actual cell loop.
```
theorem physicalProgramCells_complete (node : PhysicalNode M J) (b : ℕ)
    (r : TargetInterval target.length) (hrep : (b, r) ∈ representatives node) :
    targetCell (theta * b) r ∈ physicalProgramCells source target U N P F A thetaExponent node b := by
…
```
Mentions: OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.targetCell, OAI.EditApproximation.physicalProgramCells

theorem OAI.EditApproximation.physicalProgramOnline_contains_accepted line 304

Source documentation

The candidate list contains the sampled shared action at every accepted representative slot, with the supplied child history and current integer.

theorem physicalProgramOnline_contains_accepted {R : ℕ} [NeZero R]
    (stream : PhysicalOnlineStreams source target U N P F A T thetaExponent H tau R)
    (node : PhysicalInternalNode M J)
    (representative : Fin (representatives node.1).length) (b : ℕ)
    (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 : (representatives node.1).get representative = (b, member.center))
    (children : PhysicalChildTables M target.length) (t : ℕ) (q : TargetInterval target.length)
    (hquery : physicalProgramOnlineGuard source target U N P F A node.1 q (b, member.center)) :
    sharedBandRationalAction member.center
…

Mentions: OAI.EditApproximation.PhysicalOnlineStreams, OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.physicalSourceInterval, OAI.EditApproximation.physicalBandChildMassTable, OAI.EditApproximation.physicalBandChildInitial, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.physicalProgramOnlineGuard, OAI.EditApproximation.sharedBandRationalAction

theorem OAI.EditApproximation.physicalProgramGroups_contains_selected line 335

Source documentation

Whole-cell sampling uses the same per-scale arrays for all its members; the literal selected member is included in the parent candidate list.

theorem physicalProgramGroups_contains_selected {R : ℕ} [NeZero R]
    (stream : PhysicalGroupStreams source target U N P F A thetaExponent Q R)
    (node : PhysicalInternalNode M J) (scale : Fin (dyadicScales N).length)
    (cell : Fin (physicalProgramCells source target U N P F A thetaExponent node.1
      ((dyadicScales N).get scale)).length)
    (hnonempty : physicalNodeCellBands source target U N P F A T node.1 node.2
      ((dyadicScales N).get scale) thetaExponent tau
      ((physicalProgramCells source target U N P F A thetaExponent node.1
        ((dyadicScales N).get scale)).get cell) ≠ [])
    (children : PhysicalChildTables M target.length) (t : ℕ) :
    (chooseUnskippedGroup Q (fun i q => children i (t + 1) q)
      (physicalNodeCellBands source target U N P F A T node.1 node.2
…

Mentions: OAI.EditApproximation.PhysicalGroupStreams, OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.dyadicScales, OAI.EditApproximation.physicalProgramCells, OAI.EditApproximation.physicalNodeCellBands, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.chooseUnskippedGroup