PhysicalOnlineLocality.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The literal query-filtered online loop has at most one candidate per scale.

theorem OAI.EditApproximation.makeTargetState_endpoints line 11
theorem OAI.EditApproximation.targetStates_nodup line 18
theorem OAI.EditApproximation.dyadicScales_nodup line 34
theorem OAI.EditApproximation.representativeList_nodup line 37
theorem OAI.EditApproximation.representativeList_scale_mem line 50
theorem OAI.EditApproximation.physicalProgramOnline_query_indices_length line 67
Source documentation
A fixed query retains at most one original representative index for each scale. This is a pathwise statement on every initial seed.
```
theorem physicalProgramOnline_query_indices_length (node : PhysicalNode M J)
    (q : TargetInterval target.length) :
    ((List.finRange (representatives node).length).filter fun representative => decide
      (physicalProgramOnlineGuard source target U N P F A node q
        ((representatives node).get representative))).length ≤ (dyadicScales N).length := by
…
```
Mentions: OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.physicalProgramOnlineGuard, OAI.EditApproximation.dyadicScales
theorem OAI.EditApproximation.physicalProgramOnline_length line 93
Source documentation
The actual online action loop produces at most one action per dyadic scale, including failed band tests and every initial seed.
```
theorem physicalProgramOnline_length {R : ℕ} [NeZero R]
    (stream : PhysicalOnlineStreams source target U N P F A T thetaExponent H tau R)
    (node : PhysicalNode M J) (children : PhysicalChildTables M target.length) (t : ℕ)
    (q : TargetInterval target.length) :
    (physicalProgramOnline source target U N P F A T thetaExponent H tau η κ stream node children t q).length ≤
      (dyadicScales N).length := by
…
```
Mentions: OAI.EditApproximation.PhysicalOnlineStreams, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.physicalProgramOnline, OAI.EditApproximation.dyadicScales