Lax Lean Archive

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

Finite metadata and exact-image records for additional pins

Lax342547.MetadataPins · concepts/Lax342547/MetadataPins.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

    A coefficient choice determines finitely many nominal subspaces. A split record contains that choice and all prescribed images on those spaces. Its fiber fixes the new pins and can be joined to the previous pins.

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

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

    1 image_count proven

    2 key_count proven

    3 refined_fiber proven

    Lean source view on GitHub

    1import Lax342547.ExactPins
    2import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
    3import Mathlib.SetTheory.Cardinal.Finite
    4
    5/-!
    6---
    7title: Finite metadata and exact-image records for additional pins
    8type: lemma
    9---
    10A coefficient choice determines finitely many nominal subspaces. A split
    11record contains that choice and all prescribed images on those spaces.
    12Its fiber fixes the new pins and can be joined to the previous pins.
    13-/
    14
    15namespace Lax342547.MetadataPins
    16
    17open Lax342547.MomentSpace Lax342547.ExactPins
    18
    19def Images {Axis I : Type} (N : Type) (S : Axis → Submodule Binary (I → Binary)) :=
    20 ∀ a, S a →ₗ[Binary] (N → Binary)
    21
    22noncomputable instance {Axis I N : Type} [Fintype Axis] [Fintype I] [Fintype N]
    23 (S : Axis → Submodule Binary (I → Binary)) : Fintype (Images N S) := by
    24 classical
    25 let : ∀ a, Finite (S a →ₗ[Binary] (N → Binary)) := fun a =>
    26 Finite.of_injective (fun f : S a →ₗ[Binary] (N → Binary) => (f : S a → N → Binary))
    27 DFunLike.coe_injective
    28 exact Fintype.ofFinite (∀ a, S a →ₗ[Binary] (N → Binary))
    29
    30def Key {J Axis I : Type} (N : Type) (S : J → Axis → Submodule Binary (I → Binary)) :=
    31 Σ j, Images N (S j)
    32
    33noncomputable instance {J Axis I N : Type} [Fintype J] [Fintype Axis] [Fintype I] [Fintype N]
    34 (S : J → Axis → Submodule Binary (I → Binary)) : Fintype (Key N S) :=
    35 inferInstanceAs (Fintype (Σ j, Images N (S j)))
    36
    37def record {Ω J Axis I N : Type}
    38 (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary)) (choice : Ω → J)
    39 (S : J → Axis → Submodule Binary (I → Binary)) (o : Ω) : Key N S :=
    40 ⟨choice o, fun a => (A o a).comp (S (choice o) a).subtype⟩
    41
    42def pin {J Axis I N : Type} {S : J → Axis → Submodule Binary (I → Binary)}
    43 (k : Key N S) : Pin Axis I N := ⟨S k.1, k.2⟩
    44
    45axiom image_count {Axis I N : Type} [Fintype Axis] [Fintype I] [Fintype N]
    46 (S : Axis → Submodule Binary (I → Binary)) :
    47 Nat.card (Images N S) = 2 ^ ((∑ a, Module.finrank Binary (S a)) * Fintype.card N)
    48
    49axiom key_count {J Axis I N : Type}
    50 [Fintype J] [Fintype Axis] [Fintype I] [Fintype N]
    51 (S : J → Axis → Submodule Binary (I → Binary)) (u : ℕ)
    52 (hu : ∀ j, ∑ a, Module.finrank Binary (S j a) ≤ u) :
    53 Nat.card (Key N S) ≤ Fintype.card J * 2 ^ (u * Fintype.card N)
    54
    55axiom refined_fiber {Ω J Axis I N : Type} [Fintype Axis] [Fintype I]
    56 (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary)) (choice : Ω → J)
    57 (S : J → Axis → Submodule Binary (I → Binary)) (u : ℕ)
    58 (hu : ∀ j, ∑ a, Module.finrank Binary (S j a) ≤ u)
    59 (P₀ : Pin Axis I N) (R : Set Ω) (hR : R ⊆ P₀.event A) (o : Ω) (ho : o ∈ R) :
    60 ∃ P : Pin Axis I N, P₀.Extends P ∧ (pin (record A choice S o)).Extends P ∧
    61 P.rank ≤ P₀.rank + u ∧
    62 R ∩ {x | record A choice S x = record A choice S o} ⊆ P.event A
    63
    64end Lax342547.MetadataPins
    65
    Show ProofShow ProofShow Proof
    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…