OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/BalancedRules.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

The balanced three-stack table in paper 379-09, balanced.tex. Every row preserves total prefix length, and its record identifies the individual work-step row. The table acts on arbitrary independent tails.

  1. inductive OAI.ForcedComputation.Balanced.Record line 16
  2. inductive OAI.ForcedComputation.Balanced.Symbol line 23
  3. inductive OAI.ForcedComputation.Balanced.Control line 30
  4. inductive OAI.ForcedComputation.Balanced.Row line 37
  5. def OAI.ForcedComputation.Balanced.Row.Allowed line 51
  6. def OAI.ForcedComputation.Balanced.Row.sourceControl line 59
  7. def OAI.ForcedComputation.Balanced.Row.targetControl line 65
  8. def OAI.ForcedComputation.Balanced.Row.sourcePrefixes line 71
  9. def OAI.ForcedComputation.Balanced.Row.targetPrefixes line 82
  10. theorem OAI.ForcedComputation.Balanced.Row.balanced line 95

    Source documentation

    Balance is an identity for the complete table, without assumptions on tails.

    theorem Row.balanced (M : Recorder.Machine Q A) (blank : A) (r : Row Q A) :
    (∑ j : Fin 3, (r.sourcePrefixes blank j).length) =
      ∑ j : Fin 3, (r.targetPrefixes M blank j).length := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Row

  11. abbrev OAI.ForcedComputation.Balanced.Stack line 100
  12. abbrev OAI.ForcedComputation.Balanced.Tails line 101
  13. structure OAI.ForcedComputation.Balanced.Configuration line 103
  14. def OAI.ForcedComputation.Balanced.prefixConfiguration line 107
  15. def OAI.ForcedComputation.Balanced.Row.source line 111
  16. def OAI.ForcedComputation.Balanced.Row.target line 114
  17. def OAI.ForcedComputation.Balanced.Step line 119

    Source documentation

    A row replaces exactly its three specified prefixes and preserves every tail.

    def Step (M : Recorder.Machine Q A) (blank : A)
    (x y : Configuration Q A) : Prop :=
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Configuration

  18. theorem OAI.ForcedComputation.Balanced.Row.step line 123
  19. theorem OAI.ForcedComputation.Balanced.prependWord_injective line 129

    Source documentation

    Finite words followed by an independent infinite tail decompose uniquely.

    theorem prependWord_injective (w : List (Symbol Q A)) :
    Function.Injective (Radix.prependWord w) := by
…

    Mentions: OAI.ForcedComputation.Balanced.Symbol, OAI.ForcedComputation.Radix.prependWord

  20. theorem OAI.ForcedComputation.Balanced.Row.source_tails_injective line 139
  21. theorem OAI.ForcedComputation.Balanced.Row.target_tails_injective line 146
  22. def OAI.ForcedComputation.Balanced.targetKey line 154

    Source documentation

    Every target control specifies the stack whose top identifies the incoming row.

    def targetKey (c : Configuration Q A) : Control Q × Symbol Q A :=
…

    Mentions: OAI.ForcedComputation.Balanced.Configuration, OAI.ForcedComputation.Balanced.Control, OAI.ForcedComputation.Balanced.Symbol

  23. def OAI.ForcedComputation.Balanced.Row.targetKey line 161
  24. theorem OAI.ForcedComputation.Balanced.Row.targetKey_eq line 172
  25. theorem OAI.ForcedComputation.Balanced.Row.targetKey_injective line 178
  26. theorem OAI.ForcedComputation.Balanced.Row.target_rows_eq line 184

    Source documentation

    Incoming branches are disjoint for arbitrary independent stack tails.

    theorem Row.target_rows_eq (M : Recorder.Machine Q A) (blank : A)
    {r s : Row Q A} {u v : Tails Q A}
    (h : r.target M blank u = s.target M blank v) : r = s := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Row, OAI.ForcedComputation.Balanced.Tails

  27. theorem OAI.ForcedComputation.Balanced.Row.target_unique line 191

    Source documentation

    The complete target state recovers both the row and all three original tails.

    theorem Row.target_unique (M : Recorder.Machine Q A) (blank : A)
    {r s : Row Q A} {u v : Tails Q A}
    (h : r.target M blank u = s.target M blank v) : r = s ∧ u = v := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Row, OAI.ForcedComputation.Balanced.Tails

  28. def OAI.ForcedComputation.Balanced.decodeSource line 200

    Source documentation

    A finite source decoder. It need not accept malformed configurations; on each guarded source cylinder it recovers the unique table row.

    def decodeSource (M : Recorder.Machine Q A) (c : Configuration Q A) : Option (Row Q A) :=
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Configuration, OAI.ForcedComputation.Balanced.Row

  29. theorem OAI.ForcedComputation.Balanced.Row.decode_source line 226
  30. theorem OAI.ForcedComputation.Balanced.Row.source_rows_eq line 233

    Source documentation

    Outgoing guarded branches are disjoint on the complete tail domains.

    theorem Row.source_rows_eq {M : Recorder.Machine Q A} {blank : A}
    {r s : Row Q A} (hr : r.Allowed M) (hs : s.Allowed M) {u v : Tails Q A}
    (h : r.source blank u = s.source blank v) : r = s := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Row, OAI.ForcedComputation.Balanced.Tails

  31. theorem OAI.ForcedComputation.Balanced.Step.deterministic line 240
  32. theorem OAI.ForcedComputation.Balanced.Step.predecessor_unique line 249