Lax Lean Archive

Inductive counting certificates

Lax733996.Counting · concepts/Lax733996/Counting.lean · lax-733996

definition

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

    Definition

    The kkth reachable layer contains vertices at distance at most kk from the source. A census lists distinct reachable vertices and their path witnesses. Given the correct census size, a negative classification checks that no listed vertex has an edge to the target. A counting step classifies every vertex and counts the positive answers.

    Concept map
    2 concepts; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Lax733996.Reachability
    2import Mathlib.Data.Fintype.Powerset
    3
    4/-!
    5---
    6title: Inductive counting certificates
    7type: definition
    8---
    9The kkth reachable layer contains vertices at distance at most kk from the
    10source. A census lists distinct reachable vertices and their path witnesses.
    11Given the correct census size, a negative classification checks that no
    12listed vertex has an edge to the target. A counting step classifies every
    13vertex and counts the positive answers.
    14-/
    15
    16namespace Lax733996.Counting
    17
    18open Lax733996.Reachability
    19
    20noncomputable def layer {N : ℕ} (G : Graph N) (a : Fin N) (k : ℕ) : Finset (Fin N) := by
    21 classical
    22 exact Finset.univ.filter (fun v => Within (fun u v => G u v = true) k a v)
    23
    24def Census {N : ℕ} (G : Graph N) (a : Fin N) (k c : ℕ) (S : Finset (Fin N)) : Prop :=
    25 S.card = c ∧ ∀ v ∈ S, Within (fun u v => G u v = true) k a v
    26
    27def Classify {N : ℕ} (G : Graph N) (a : Fin N) (k c : ℕ) (v : Fin N) : Bool → Prop
    28 | true => Within (fun u v => G u v = true) (k + 1) a v
    29 | false => ∃ S, Census G a k c S ∧ v ≠ a ∧ ∀ u ∈ S, G u v = false
    30
    31def CountStep {N : ℕ} (G : Graph N) (a : Fin N) (k c d : ℕ) : Prop :=
    32 ∃ answers : Fin N → Bool, (∀ v, Classify G a k c v (answers v)) ∧
    33 (Finset.univ.filter (fun v => answers v = true)).card = d
    34
    35def CountTrace {N : ℕ} (G : Graph N) (a : Fin N) (counts : ℕ → ℕ) : Prop :=
    36 counts 0 = 1 ∧ ∀ k < N, CountStep G a k (counts k) (counts (k + 1))
    37
    38def NonreachCertificate {N : ℕ} (G : Graph N) (a b : Fin N) : Prop :=
    39 ∃ counts, CountTrace G a counts ∧
    40 ∃ S, Census G a N (counts N) S ∧ b ∉ S
    41
    42end Lax733996.Counting
    43
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…