OAI/Combinatorics/EditApproximation/Geometry/BandEarlierDependence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The band construction and its literal guards use only the child coordinates of the finite wide action list. The result types retain the full tables as indices, so acceptance and returned centers are compared after projecting away proof fields.

  1. theorem OAI.EditApproximation.rationalWidePrefixCost_congr_child line 15
  2. theorem OAI.EditApproximation.rationalWidePrefixMinimum_congr_child line 27
  3. theorem OAI.EditApproximation.rationalWideActionMinimum_congr_child line 41
  4. theorem OAI.EditApproximation.computedBandActions_congr_child line 59
  5. theorem OAI.EditApproximation.representativeBandActions_congr_child line 75
  6. theorem OAI.EditApproximation.bandChildEnvelope_congr_initial line 90
  7. theorem OAI.EditApproximation.bandRoundSpacing_congr_initial line 100
  8. theorem OAI.EditApproximation.canonicalRoundedBandAction_congr_initial line 110
  9. theorem OAI.EditApproximation.representativeBandEnvelope_congr line 119
  10. theorem OAI.EditApproximation.testUnskippedBand_isSome_iff line 137
  11. theorem OAI.EditApproximation.testUnskippedBand_isSome_congr line 174
  12. theorem OAI.EditApproximation.testUnskippedBand_center_projection line 199
  13. theorem OAI.EditApproximation.testUnskippedBand_center_congr line 211
  14. theorem OAI.EditApproximation.wideAction_child_agreement_of_cover line 230

    Source documentation

    The actual wide coordinates are in the earlier-input cover at every stored history time. This specializes the congruence premise without requiring equality of a full child table.

    theorem wideAction_child_agreement_of_cover {nx ny M : ℕ} (parent : TargetInterval nx)
    (P history b t : ℕ) (r : TargetInterval ny)
    (representatives : List (ℕ × TargetInterval ny)) (hrep : (b, r) ∈ representatives)
    (ht : t < history) (left right : PhysicalChildTables M ny)
    (heq : ∀ i s q, (i, s, q) ∈ wideEarlierInputCover parent P history representatives →
      left i s q = right i s q) :
    ∀ action ∈ wideActionList M parent r b P,
      ∀ i, left i t (action i) = right i t (action i) := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.wideEarlierInputCover, OAI.EditApproximation.wideActionList