Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Growth of Temporal Reachability

Lax623795.TemporalExploration · concepts/Lax623795/TemporalExploration.lean · lax-623795

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Let XX be a nonempty proper set of vertices in an always-connected temporal graph. Fix a nonempty time interval ending at endTimeendTime. If the vertices reachable from XX during this interval do not yet comprise the whole vertex set, extending the interval by one valid time step strictly enlarges the reachable vertex set.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax623795.TemporalGraphs
    2
    3/-!
    4---
    5title: Growth of Temporal Reachability
    6type: lemma
    7---
    8
    9Let `X` be a nonempty proper set of vertices in an always-connected temporal
    10graph. Fix a nonempty time interval ending at `endTime`. If the vertices reachable
    11from `X` during this interval do not yet comprise the whole vertex set, extending
    12the interval by one valid time step strictly enlarges the reachable vertex set.
    13-/
    14
    15universe u
    16
    17namespace Lax623795.TemporalExploration
    18
    19open Lax623795.TemporalGraphs
    20
    21/-- Extending a reachability interval by one connected snapshot discovers a new vertex. -/
    22axiom reachableVertexSet_ssubset_next
    23 {V : Type u} (G : TemporalGraph V) (X : Set V)
    24 (startTime endTime nextTime : G.Timestep)
    25 (h_connected : G.AlwaysConnected)
    26 (hX_nonempty : X.Nonempty)
    27 (_hX_proper : X ≠ Set.univ)
    28 (h_interval : startTime.val.val ≤ endTime.val.val)
    29 (h_next : nextTime.val.val = endTime.val.val + 1)
    30 (h_reachable_proper :
    31 G.reachableVertexSet X startTime endTime ≠ Set.univ) :
    32 G.reachableVertexSet X startTime endTime ⊂
    33 G.reachableVertexSet X startTime nextTime
    34
    35end Lax623795.TemporalExploration
    36
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…