Lax Lean Archive

Inductive counting certificates

Lax362205.Counting · concepts/Lax362205/Counting.lean · lax-362205

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 Lax362205.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 Lax362205.Counting
    17
    18open scoped Classical
    19
    20open Lax362205.Reachability
    21
    22/-- The vertices reachable from `a` using at most `k` directed edges. -/
    23noncomputable def layer {N : ℕ} (G : Graph N) (a : Fin N) (k : ℕ) : Finset (Fin N) :=
    24 Finset.univ.filter (fun v => Within (fun u v => G u v = true) k a v)
    25
    26/-- A set of `c` distinct vertices, each reachable within `k` steps. -/
    27def Census {N : ℕ} (G : Graph N) (a : Fin N) (k c : ℕ) (S : Finset (Fin N)) : Prop :=
    28 S.card = c ∧ ∀ v ∈ S, Within (fun u v => G u v = true) k a v
    29
    30/-- A positive answer supplies a path; a negative answer supplies a census that has no edge to `v`. -/
    31def Classify {N : ℕ} (G : Graph N) (a : Fin N) (k c : ℕ) (v : Fin N) : Bool → Prop
    32 | true => Within (fun u v => G u v = true) (k + 1) a v
    33 | false => ∃ S, Census G a k c S ∧ v ≠ a ∧ ∀ u ∈ S, G u v = false
    34
    35/-- Classify every vertex for the next layer and count exactly `d` positive answers. -/
    36def CountStep {N : ℕ} (G : Graph N) (a : Fin N) (k c d : ℕ) : Prop :=
    37 ∃ answers : Fin N → Bool, (∀ v, Classify G a k c v (answers v)) ∧
    38 (Finset.univ.filter (fun v => answers v = true)).card = d
    39
    40/-- Start with the source alone and certify the size of each successive reachable layer. -/
    41def CountTrace {N : ℕ} (G : Graph N) (a : Fin N) (counts : ℕ → ℕ) : Prop :=
    42 counts 0 = 1 ∧ ∀ k < N, CountStep G a k (counts k) (counts (k + 1))
    43
    44/-- A certified sequence of layer counts whose final census omits the target `b`. -/
    45def NonreachCertificate {N : ℕ} (G : Graph N) (a b : Fin N) : Prop :=
    46 ∃ counts, CountTrace G a counts ∧
    47 ∃ S, Census G a N (counts N) S ∧ b ∉ S
    48
    49end Lax362205.Counting
    50
    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…