Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

d = 1 universality: every VC-1 class compresses at kernel size one, with no side information. No finiteness, no distinguished member, no chain hypothesis. Twist the class by any member to place ∅ in it; there the VC bound makes co-member points comparable in the membership order, so every label set is a finite chain; anchor at its maximum, reconstruct with interConvention, and transport the scheme back with the same kernels.

DeclStructuralIgnorance.hasKernelScheme_one_of_vcBounded_one

∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Set α)},
  StructuralIgnorance.vcBounded 𝒜 1 → StructuralIgnorance.HasKernelScheme 𝒜 1

TopicCompression

ThesisStepHypothesisDefinition

DeclStructuralIgnorance.hasKernelScheme_one_of_vcBounded_oneDeclaration kindtheorem
```
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Set α)},
  StructuralIgnorance.vcBounded 𝒜 1 → StructuralIgnorance.HasKernelScheme 𝒜 1
```
StructuralIgnorance.Convention StructuralIgnorance.HasKernelScheme StructuralIgnorance.IsKernel StructuralIgnorance.IsSample StructuralIgnorance.interConvention StructuralIgnorance.memOrder StructuralIgnorance.twistClass StructuralIgnorance.vcBounded
Uses
DeclStructuralIgnorance.vcBounded_twistClassDeclaration kindtheorem
VC bounds are twist-invariant (the direction needed for normalization).
```
∀ {α : Type u_1} [DecidableEq α] {𝒜 : Set (Set α)} {d : ℕ},
  StructuralIgnorance.vcBounded 𝒜 d →
    ∀ (S₀ : Set α), StructuralIgnorance.vcBounded (StructuralIgnorance.twistClass 𝒜 S₀) d
```
StructuralIgnorance.SetShatters StructuralIgnorance.twistClass StructuralIgnorance.vcBounded
Uses
- StructuralIgnorance.SetShatters.of_twistClass
Used by
- StructuralIgnorance.hasKernelScheme_one_of_vcBounded_one
DeclStructuralIgnorance.SetShatters.of_twistClassDeclaration kindtheorem
Shattering transports from the twisted class back to the original: the witnesses untwist, and the patterns correspond through the involution C ↦ C ∆ (B ∩ S₀).
```
∀ {α : Type u_1} [DecidableEq α] {𝒜 : Set (Set α)} {S₀ : Set α} {B : Finset α},
  StructuralIgnorance.SetShatters (StructuralIgnorance.twistClass 𝒜 S₀) B → StructuralIgnorance.SetShatters 𝒜 B
```
StructuralIgnorance.SetShatters StructuralIgnorance.baseLabels StructuralIgnorance.twistClass
Uses
- StructuralIgnorance.coe_baseLabels
Used by
- StructuralIgnorance.vcBounded_twistClass
DeclStructuralIgnorance.memOrder_total_of_vcBounded_oneDeclaration kindtheorem
With the empty set in the class, a VC bound of one makes any two points of a common member comparable in the membership order: otherwise the four assembled patterns shatter the pair.
```
∀ {α : Type u_1} [DecidableEq α] {𝒜 : Set (Set α)},
  StructuralIgnorance.vcBounded 𝒜 1 →
    ∅ ∈ 𝒜 →
      ∀ {a b : α}, (∃ S ∈ 𝒜, a ∈ S ∧ b ∈ S) → StructuralIgnorance.memOrder 𝒜 a b ∨ StructuralIgnorance.memOrder 𝒜 b a
```
StructuralIgnorance.SetShatters StructuralIgnorance.memOrder StructuralIgnorance.vcBounded
Uses
- StructuralIgnorance.memOrder_refl
Used by
- StructuralIgnorance.hasKernelScheme_one_of_vcBounded_one
DeclStructuralIgnorance.isKernel_interConvention_anchorDeclaration kindtheorem
The anchor leg of the intersection convention: a maximum of the label set in the membership order is a size-1 kernel. The upper inclusion comes from the realizing member, the lower from maximality.
```
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Set α)} {A T : Finset α},
  StructuralIgnorance.IsSample 𝒜 A T →
    ∀ {x : α},
      x ∈ T →
        (∀ a ∈ T, StructuralIgnorance.memOrder 𝒜 a x) →
          StructuralIgnorance.IsKernel (StructuralIgnorance.interConvention 𝒜) 1 A T {x}
```
StructuralIgnorance.IsKernel StructuralIgnorance.IsSample StructuralIgnorance.interConvention StructuralIgnorance.memOrder
Uses
- StructuralIgnorance.IsSample.subset
Used by
- StructuralIgnorance.hasKernelScheme_one_of_vcBounded_one
DeclStructuralIgnorance.IsSample.subsetDeclaration kindtheorem
Realizable label patterns are supported inside their window.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A T : Finset α}, StructuralIgnorance.IsSample 𝒜 A T → T ⊆ A
```
StructuralIgnorance.IsSample
Used by
- StructuralIgnorance.isKernel_interConvention_anchor
DeclStructuralIgnorance.exists_memOrder_max_of_totalDeclaration kindtheorem
A finite nonempty set on which the membership order is total has a maximum.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {T : Finset α},
  (∀ a ∈ T, ∀ b ∈ T, StructuralIgnorance.memOrder 𝒜 a b ∨ StructuralIgnorance.memOrder 𝒜 b a) →
    T.Nonempty → ∃ x ∈ T, ∀ a ∈ T, StructuralIgnorance.memOrder 𝒜 a x
```
StructuralIgnorance.memOrder
Uses
- StructuralIgnorance.memOrder_refl
- StructuralIgnorance.memOrder_trans
Used by
- StructuralIgnorance.hasKernelScheme_one_of_vcBounded_one

DeclStructuralIgnorance.memOrder_transDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {a b c : α},
  StructuralIgnorance.memOrder 𝒜 a b → StructuralIgnorance.memOrder 𝒜 b c → StructuralIgnorance.memOrder 𝒜 a c

StructuralIgnorance.memOrder

Used by

StructuralIgnorance.exists_memOrder_max_of_total

DeclStructuralIgnorance.memOrder_reflDeclaration kindtheorem
```
∀ {α : Type u_1} (𝒜 : Set (Set α)) (a : α), StructuralIgnorance.memOrder 𝒜 a a
```
StructuralIgnorance.memOrder
Used by
- StructuralIgnorance.exists_memOrder_max_of_total
- StructuralIgnorance.memOrder_total_of_vcBounded_one
DeclStructuralIgnorance.empty_mem_twistClassDeclaration kindtheorem
Twisting by a member places the empty set in the class.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {S₀ : Set α}, S₀ ∈ 𝒜 → ∅ ∈ StructuralIgnorance.twistClass 𝒜 S₀
```
StructuralIgnorance.twistClass
Used by
- StructuralIgnorance.hasKernelScheme_one_of_vcBounded_one
DeclStructuralIgnorance.HasKernelScheme.of_twistClassDeclaration kindtheorem
Kernel schemes transport back through a twist, with the same kernels.
```
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Set α)} {S₀ : Set α} {k : ℕ},
  StructuralIgnorance.HasKernelScheme (StructuralIgnorance.twistClass 𝒜 S₀) k → StructuralIgnorance.HasKernelScheme 𝒜 k
```
StructuralIgnorance.Convention StructuralIgnorance.HasKernelScheme StructuralIgnorance.IsKernel StructuralIgnorance.IsSample StructuralIgnorance.baseLabels StructuralIgnorance.twistClass StructuralIgnorance.twistConvention
Uses
Used by
- StructuralIgnorance.hasKernelScheme_one_of_vcBounded_one
DeclStructuralIgnorance.set_symmDiff_inter_rightDeclaration kindtheorem
```
∀ {α : Type u_1} (s t u : Set α), symmDiff s t ∩ u = symmDiff (s ∩ u) (t ∩ u)
```
Used by
- StructuralIgnorance.HasKernelScheme.of_twistClass
DeclStructuralIgnorance.finset_inter_symmDiffDeclaration kindtheorem
```
∀ {α : Type u_1} [inst : DecidableEq α] (Z T F : Finset α), Z ∩ symmDiff T F = symmDiff (Z ∩ T) (Z ∩ F)
```
Used by
- StructuralIgnorance.HasKernelScheme.of_twistClass
DeclStructuralIgnorance.IsSample.twistDeclaration kindtheorem
Realizability transports through the twist, with the label set twisted inside the window.
```
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Set α)} {A T : Finset α},
  StructuralIgnorance.IsSample 𝒜 A T →
    ∀ (S₀ : Set α),
      StructuralIgnorance.IsSample (StructuralIgnorance.twistClass 𝒜 S₀) A
        (symmDiff T (StructuralIgnorance.baseLabels S₀ A))
```
StructuralIgnorance.IsSample StructuralIgnorance.baseLabels StructuralIgnorance.twistClass
Uses
- StructuralIgnorance.coe_baseLabels
Used by
- StructuralIgnorance.HasKernelScheme.of_twistClass
DeclStructuralIgnorance.coe_baseLabelsDeclaration kindtheorem
```
∀ {α : Type u_1} (S₀ : Set α) (Z : Finset α), ↑(StructuralIgnorance.baseLabels S₀ Z) = ↑Z ∩ S₀
```
StructuralIgnorance.baseLabels
Used by
Hypothesish
```
StructuralIgnorance.vcBounded 𝒜 1
```
DefinitionStructuralIgnorance.Conventiondef
A reconstruction rule: from a kept labeled pair — kernel points and their 1-labeled part — to a total hypothesis. Total by convention; only values on realizable pairs matter.
```
Type u_2 → Type u_2
```
DefinitionStructuralIgnorance.HasKernelSchemedef
A kernel scheme of size k with no side information: one reconstruction rule under which every realizable sample contains a generating kernel of at most k points (Littlestone–Warmuth 1986, in compression-map-free form).
```
{α : Type u_1} → [DecidableEq α] → Set (Set α) → ℕ → Prop
```
DefinitionStructuralIgnorance.IsKerneldef
ρ regenerates the sample (A, T) from the kernel Z: the kernel is kept inside the sample, has at most k points, and the reconstructed hypothesis meets A in exactly T.
```
{α : Type u_1} → [DecidableEq α] → StructuralIgnorance.Convention α → ℕ → Finset α → Finset α → Finset α → Prop
```
DefinitionStructuralIgnorance.IsSampledef
The labeled window (A, T) is realizable in 𝒜: some member meets A in exactly T. Points of T are labeled 1, points of A \ T are labeled 0 (Littlestone–Warmuth 1986, realizable samples).
```
{α : Type u_1} → Set (Set α) → Finset α → Finset α → Prop
```
DefinitionStructuralIgnorance.SetShattersdef
The class 𝒜 shatters the finite set B: every sub-pattern of B is realized by a member. Set-grammar port of Finset.Shatters (Mathlib Combinatorics.SetFamily.Shatter).
```
{α : Type u_1} → Set (Set α) → Finset α → Prop
```
DefinitionStructuralIgnorance.baseLabelsdef
The part of a finite window lying in the base set.
```
{α : Type u_1} → Set α → Finset α → Finset α
```
DefinitionStructuralIgnorance.interConventiondef
Reconstruction by intersection: the hypothesis is the intersection of all members containing the kernel's 1-labeled part. Improper — the output need not be a member — which is what dense chains require; the kernel's point set is not consulted beyond its labels.
```
{α : Type u_1} → Set (Set α) → StructuralIgnorance.Convention α
```
DefinitionStructuralIgnorance.memOrderdef
The membership order of a class: a lies below b when every member containing b contains a.
```
{α : Type u_1} → Set (Set α) → α → α → Prop
```
DefinitionStructuralIgnorance.twistClassdef
The class relabeled by symmetric difference with a base set.
```
{α : Type u_1} → Set (Set α) → Set α → Set (Set α)
```
DefinitionStructuralIgnorance.twistConventiondef
The conjugated convention: untwist the kernel's labels, reconstruct in the twisted class, twist the hypothesis back.
```
{α : Type u_1} → [DecidableEq α] → Set α → StructuralIgnorance.Convention α → StructuralIgnorance.Convention α
```
DefinitionStructuralIgnorance.vcBoundeddef
VC bound in Set grammar: no shattered set exceeds d points (the port of Finset.vcDim ≤ d, Mathlib Combinatorics.SetFamily.Shatter).
```
{α : Type u_1} → Set (Set α) → ℕ → Prop
```

DOIMTH.R-2026-6025

Cite

Verification

Replay: accepted
Axioms: Classical.choiceQuot.soundpropext
Statement identity: not-applicable
Substrate: Lean 4 kernel v4.31.0
Dictionary pin: design-lab@5802df4 · initial
Frozen export: 1641f3634b64
Verified: 2026-09-24T00:00:00Z