OAI/Analysis/Nonexpansive/CandidateLedgerJoin.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

The candidate ledger of the actual recursively constructed tree

The full ordered candidate groups supply the ledger's records. The actual positive-support embeddings select its retained entries. Thus its parent map and its retained maps agree with the tree extracted from the frontier tower, including all discarded records in every earlier prefix.

  1. def OAI.ReflexiveFixedPoints.CandidateContext.levelPrefix line 33

    Source documentation

    The literal immutable history preceding a candidate in the full level.

    def levelPrefix (i : Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ))) :
    List (CandidateRecord C) :=
…

    Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total, OAI.ReflexiveFixedPoints.CandidateRecord

  2. theorem OAI.ReflexiveFixedPoints.CandidateContext.levelPrefix_length line 37
  3. def OAI.ReflexiveFixedPoints.CandidateContext.levelPrefixInclusion line 44

    Source documentation

    The prefix indices are the corresponding initial candidate ordinals.

    def levelPrefixInclusion
    (i : Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ))) :
    Fin (C.levelPrefix A hanchor hτ i).length ↪
      Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ)) :=
…

    Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total

  4. theorem OAI.ReflexiveFixedPoints.CandidateContext.levelPrefix_get line 51

    Source documentation

    Reading the immutable prefix returns exactly the full ledger record.

    theorem levelPrefix_get
    (i : Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ)))
    (j : Fin (C.levelPrefix A hanchor hτ i).length) :
    (C.levelPrefix A hanchor hτ i).get j =
      C.levelRecord A hanchor hτ (C.levelPrefixInclusion A hanchor hτ i j) := by
…

    Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total

  5. theorem OAI.ReflexiveFixedPoints.CandidateContext.levelPrefix_legal line 62

    Source documentation

    Legality was established against this literal preceding prefix.

    theorem levelPrefix_legal
    (i : Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ))) :
    C.Legal (C.levelPrefix A hanchor hτ i) (C.levelRecord A hanchor hτ i) :=
…

    Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total

  6. theorem OAI.ReflexiveFixedPoints.CandidateContext.levelRecord_retainedCandidate_map line 68

    Source documentation

    The retained record stores the very map installed in the extension.

    theorem levelRecord_retainedCandidate_map
    (v : Fin (C.selectedExtension A hanchor).size) :
    (C.levelRecord A hanchor C.runTolerance_pos
      (C.retainedCandidate A hanchor v)).map =
        (C.selectedExtension A hanchor).map v := by
…
  7. def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger line 97

    Source documentation

    The concrete ledger retains every candidate chosen at this level.

    def candidateLedger (k : ℕ) :
    CandidateLedger (tower D A U).toOrderedTree k
      (CandidateRecord (context D A U k)) where
…

    Mentions: OAI.ReflexiveFixedPoints.CandidateLedger, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.CandidateRecord, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context

  8. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger_count line 120
  9. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger_retain line 124
  10. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger_point_parent line 129

    Source documentation

    Each ledger entry's stored parent equals its ordered ledger parent.

    theorem candidateLedger_point_parent (k : ℕ)
    (i : Fin (candidateLedger D A U k).count) :
    ((candidateLedger D A U k).point i).parent =
      (candidateLedger D A U k).parent i :=
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger

  11. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger_retainedPoint_parent line 137

    Source documentation

    Retaining a record preserves the parent of the final tree node.

    theorem candidateLedger_retainedPoint_parent (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    ((candidateLedger D A U k).retainedPoint v).parent =
      (tower D A U).toOrderedTree.parent k v := by
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger

  12. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger_retainedPoint_map line 145

    Source documentation

    The retained point is the actual map used by the infinite evaluator.

    theorem candidateLedger_retainedPoint_map (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    ((candidateLedger D A U k).retainedPoint v).map =
      (tower D A U).toEvaluation.map (k + 1) v := by
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger

  13. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger_retainedPoint_generated line 158

    Source documentation

    Each actual retained map carries its original generation derivation.

    theorem candidateLedger_retainedPoint_generated (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    Generated D.closed D.convex D.T D.nonexpansive
      (((candidateLedger D A U k).retainedPoint v).map) :=
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.Generated, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger

  14. def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateFunctional line 165

    Source documentation

    The detector functional is the one chosen for this candidate record.

    def candidateFunctional (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) : X →L[ℝ] ℝ :=
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower

  15. def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger line 170

    Source documentation

    The same actual ledger, evaluated at the single fixed anchor.

    def candidatePointLedger (k : ℕ) :
    CandidateLedger (tower D A U).toOrderedTree k D.K where
…

    Mentions: OAI.ReflexiveFixedPoints.CandidateLedger, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower

  16. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger_retainedPoint line 180

    Source documentation

    Its retained outputs are the actual final tree maps at the fixed anchor.

    theorem candidatePointLedger_retainedPoint (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    (candidatePointLedger D A U k).retainedPoint v =
      (tower D A U).toEvaluation.map (k + 1) v A.x := by
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger

  17. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger_earlierParent line 187
  18. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger_earlierPoint line 192
  19. def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix line 199

    Source documentation

    The actual history at the instant this retained candidate was chosen.

    def candidatePrefix (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    List (CandidateRecord (context D A U k)) :=
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.CandidateRecord, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context

  20. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix_length line 205
  21. def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixIndex line 212

    Source documentation

    This equivalence only changes the proof of the same prefix length.

    def candidatePrefixIndex (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    Fin (candidatePrefix D A U k v).length ≃
      (candidatePointLedger D A U k).Earlier v :=
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger

  22. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixIndex_val line 218
  23. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix_record line 224

    Source documentation

    Every earlier ledger entry is the record in the actual earlier history.

    theorem candidatePrefix_record (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1))
    (i : Fin (candidatePrefix D A U k v).length) :
    (candidatePrefix D A U k v).get i =
      (candidateLedger D A U k).earlierPoint v
        (candidatePrefixIndex D A U k v i) :=
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixIndex

  24. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix_parent line 234

    Source documentation

    The history and the final prediction parameter use the same parent labels.

    theorem candidatePrefix_parent (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1))
    (i : Fin (candidatePrefix D A U k v).length) :
    (context D A U k).historyParent (candidatePrefix D A U k v) i =
      (candidatePointLedger D A U k).earlierParent v
        (candidatePrefixIndex D A U k v i) := by
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixIndex

  25. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix_point line 245

    Source documentation

    History outputs and the prediction ledger agree at the original anchor.

    theorem candidatePrefix_point (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1))
    (i : Fin (candidatePrefix D A U k v).length) :
    (context D A U k).historyPoint (candidatePrefix D A U k v) i =
      (candidatePointLedger D A U k).earlierPoint v
        (candidatePrefixIndex D A U k v i) := by
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePointLedger, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixIndex

  26. theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix_legal line 256

    Source documentation

    The retained candidate's detector was proved for this exact prefix.

    theorem candidatePrefix_legal (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    (context D A U k).Legal (candidatePrefix D A U k v)
      ((candidateLedger D A U k).retainedPoint v) :=
…

    Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLedger