Lax Lean Archive

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

Finite deterministic container recursion

Lax342547.ContainerRun · concepts/Lax342547/ContainerRun.lean · lax-342547

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

    The fingerprint procedure preserves every independent residual set, terminates by strict cardinality decrease, and reconstructs its terminal set from its ordered fingerprint. A stepwise entropy increase bounds the fingerprint length.

    Concept map
    1 concept; 10 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.

    1 next_card_lt proven

    2 next_preserves proven

    3 next_subset proven

    4 recorded_subset proven

    5 run_entropy_budget proven

    6 run_preserves proven

    7 run_replay proven

    8 run_terminal proven

    Lean source view on GitHub

    1import Mathlib.Data.Finset.Card
    2import Mathlib.Data.List.Basic
    3import Mathlib.Data.Real.Basic
    4import Mathlib.Tactic
    5
    6/-!
    7---
    8title: Finite deterministic container recursion
    9type: lemma
    10---
    11The fingerprint procedure preserves every independent residual set, terminates by strict cardinality decrease, and reconstructs its terminal set from its ordered fingerprint. A stepwise entropy increase bounds the fingerprint length.
    12-/
    13
    14namespace Lax342547.ContainerRun
    15
    16
    17
    18noncomputable def next {U : Type} (H : U → U → Prop) (I R : Finset U) (v : U) : Finset U := by
    19 classical
    20 exact if v ∈ I then R.filter (fun w => ¬ H v w) else R.erase v
    21
    22noncomputable def run {U : Type} (active : Finset U → Prop) (pick : Finset U → U)
    23 (H : U → U → Prop) (I : Finset U) : ℕ → Finset U → Finset U × List U := by
    24 classical
    25 exact fun fuel R => match fuel with
    26 | 0 => (R,[])
    27 | n+1 => if active R then
    28 let v := pick R
    29 let result := run active pick H I n (next H I R v)
    30 (result.1,if v ∈ I then v::result.2 else result.2)
    31 else (R,[])
    32
    33noncomputable def replay {U : Type} (active : Finset U → Prop) (pick : Finset U → U)
    34 (H : U → U → Prop) : ℕ → Finset U → List U → Finset U := by
    35 classical
    36 exact fun fuel R record => match fuel with
    37 | 0 => R
    38 | n+1 => if active R then
    39 let v := pick R
    40 if record.head? = some v then
    41 replay active pick H n (R.filter (fun w => ¬ H v w)) record.tail
    42 else replay active pick H n (R.erase v) record
    43 else R
    44
    45axiom next_subset {U : Type} (H : U → U → Prop) (I R : Finset U) (v : U) : next H I R v ⊆ R
    46
    47axiom next_preserves {U : Type} (H : U → U → Prop) (I R : Finset U) (v : U)
    48 (hI : I ⊆ R) (hind : ∀ x ∈ I, ∀ y ∈ I, ¬ H x y) : I ⊆ next H I R v
    49
    50axiom next_card_lt {U : Type} (H : U → U → Prop) (I R : Finset U) (v : U)
    51 (hv : v ∈ R) (hne : ∃ w ∈ R, H v w) : (next H I R v).card < R.card
    52
    53axiom recorded_subset {U : Type} (active : Finset U → Prop) (pick : Finset U → U)
    54 (H : U → U → Prop) (I R : Finset U) (fuel : ℕ) :
    55 ∀ v ∈ (run active pick H I fuel R).2, v ∈ I
    56
    57axiom run_replay {U : Type} (active : Finset U → Prop) (pick : Finset U → U)
    58 (H : U → U → Prop) (I R : Finset U) (fuel : ℕ) :
    59 replay active pick H fuel R (run active pick H I fuel R).2 = (run active pick H I fuel R).1
    60
    61axiom run_preserves {U : Type} (active : Finset U → Prop) (pick : Finset U → U)
    62 (H : U → U → Prop) (I R : Finset U) (fuel : ℕ)
    63 (hI : I ⊆ R) (hind : ∀ x ∈ I, ∀ y ∈ I, ¬ H x y) :
    64 I ⊆ (run active pick H I fuel R).1 ∧ (run active pick H I fuel R).1 ⊆ R
    65
    66axiom run_terminal {U : Type} (active : Finset U → Prop) (pick : Finset U → U)
    67 (H : U → U → Prop) (I R : Finset U) (fuel : ℕ)
    68 (hpick : ∀ T, active T → pick T ∈ T ∧ ∃ w ∈ T, H (pick T) w)
    69 (hsize : R.card < fuel) : ¬ active (run active pick H I fuel R).1
    70
    71axiom run_entropy_budget {U : Type} (active : Finset U → Prop) (pick : Finset U → U)
    72 (H : U → U → Prop) (I R : Finset U) (fuel : ℕ) (E : Finset U → ℝ) (B δ : ℝ)
    73 (hδ : 0 ≤ δ) (hb : ∀ T, active T → E T ≤ B)
    74 (hstep : by
    75 classical
    76 exact ∀ T, active T → active (next H I T (pick T)) →
    77 E T + (if pick T ∈ I then δ else 0) ≤ E (next H I T (pick T)))
    78 (hR : active R) :
    79 (((run active pick H I fuel R).2.length : ℝ)-1)*δ ≤ B-E R
    80
    81end Lax342547.ContainerRun
    82
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…