Grace/Cumulus/Cardinal/LeastCode.g17

Open in Workbench Download source

Imports

Countable · Set

Declarations

Source

1-- Choice-free selection by least code: a set coded injectively into the2-- naturals lets every point of a domain pick, among the candidates a3-- relation offers it, the one of least code; a domain whose points are4-- separated by candidates from a countable set is countable5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Cardinal.LeastCode11import Countable12import Set1314-- Selection by least code. A relation R offers each point x of D the15-- candidates W ∈ B with relates(R, x, W); under an injective code16-- g : B → ℕ the point selects the candidate of least code. No choice is17-- involved: the least code is the least element of a set of naturals.1819def candidates (R x B : Set) : Set := { W ∈ B | relates(R, x, W) }2021def candidateCodes (g R x B : Set) : Set := { g(W) | W ∈ candidates(R, x, B) }2223def leastCoded (g R D B : Set) : Set :=24  { p ∈ D × B | ∃ x ∈ D, ∃ W ∈ B, p = (x ↦ W) ∧25    relates(R, x, W) ∧ (∀ V ∈ B, relates(R, x, V) → g(W) ⊆ g(V)) }2627theorem leastCoded.relates (g R D B x W : Set)28  shows relates(leastCoded(g, R, D, B), x, W) ↔29    x ∈ D ∧ W ∈ B ∧ relates(R, x, W) ∧30      (∀ V ∈ B, relates(R, x, V) → g(W) ⊆ g(V))31proof32  constructor33  . intro edge34    unfold relates at edge35    have parts := leastCoded.membership.forward with edge36    obtain ⟨x2, hx2, W2, hW2, shape, related, least⟩ := parts.right37    obtain ⟨rfl, rfl⟩ := orderedPair.injective with shape38    exact ⟨hx2, hW2, related, least⟩39  . intro h40    obtain ⟨hx, hW, related, least⟩ := h41    unfold relates42    apply leastCoded.membership.backward43    constructor44    . exact product.pair with hx, hW45    . exact ⟨x, hx, W, hW, rfl, related, least⟩4647-- Existence: the codes of the candidates form a nonempty set of naturals,48-- hence of ordinals, and its least element is the code of a candidate.49theorem leastCoded.exists (g R D B x : Set)50  requires code : InjectiveBetween(g, B, ℕ)51  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)52  requires hx : x ∈ D53  shows ∃ W ∈ B, relates(leastCoded(g, R, D, B), x, W)54proof55  have function := Injective.function with code56  obtain ⟨W0, hW0, related0⟩ := offered with x, hx57  have candidate0 : W0 ∈ candidates(R, x, B)58    exact candidates.membership.backward with ⟨hW0, related0⟩59  have code0 : g(W0) ∈ candidateCodes(g, R, x, B)60    exact candidateCodes.membership.backward with ⟨W0, candidate0, rfl⟩61  have ordinals : ∀ n ∈ candidateCodes(g, R, x, B), n ∈ Ordinal62    intros n hn63    obtain ⟨W, hW, shape⟩ := candidateCodes.membership.forward with hn64    have parts := candidates.membership.forward with hW65    have natural := FunctionBetween.apply_closed with function, parts.left66    rw ← shape67    exact Ordinal.member with Ordinal.omega, natural68  have inhabited : Nonempty(candidateCodes(g, R, x, B)) := ⟨g(W0), code0⟩69  have nonempty := Nonempty.ne_empty with inhabited70  obtain ⟨m, hm, least⟩ := Ordinal.least with ordinals, nonempty71  obtain ⟨W, hW, shape⟩ := candidateCodes.membership.forward with hm72  have parts := candidates.membership.forward with hW73  witness W74  constructor75  . exact parts.left76  . apply leastCoded.relates.backward77    refine ⟨hx, parts.left, parts.right, ?_⟩78    intros V hV relatedV79    have candidateV : V ∈ candidates(R, x, B)80      exact candidates.membership.backward with ⟨hV, relatedV⟩81    have codeV : g(V) ∈ candidateCodes(g, R, x, B)82      exact candidateCodes.membership.backward with ⟨V, candidateV, rfl⟩83    rw shape84    exact least with g(V), codeV8586-- Uniqueness: two least codes are each below the other, so they are equal,87-- and the code is injective.88theorem leastCoded.unique (g R D B x W V : Set)89  requires code : InjectiveBetween(g, B, ℕ)90  requires first : relates(leastCoded(g, R, D, B), x, W)91  requires second : relates(leastCoded(g, R, D, B), x, V)92  shows W = V93proof94  obtain ⟨hx, hW, relatedW, leastW⟩ := leastCoded.relates.forward with first95  obtain ⟨hx2, hV, relatedV, leastV⟩ := leastCoded.relates.forward with96    second97  have below := leastW with V, hV, relatedV98  have above := leastV with W, hW, relatedW99  have same := Subset.antisymmetric with below, above100  exact Injective.apply_cancel with code, hW, hV, same101102theorem leastCoded.function (g R D B : Set)103  requires code : InjectiveBetween(g, B, ℕ)104  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)105  shows leastCoded(g, R, D, B) : D → B106proof107  refine ⟨?_, ?_, ?_⟩108  . intros p hp109    have parts := leastCoded.membership.forward with hp110    exact parts.left111  . intros x W first V second112    exact leastCoded.unique with code, first, second113  . intros x hx114    exact leastCoded.exists with code, offered, hx115116-- When no candidate is offered to two different points, the selection is117-- injective.118theorem leastCoded.injective (g R D B : Set)119  requires code : InjectiveBetween(g, B, ℕ)120  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)121  requires separated : ∀ x ∈ D, ∀ y ∈ D, ∀ W ∈ B,122    relates(R, x, W) → relates(R, y, W) → x = y123  shows InjectiveBetween(leastCoded(g, R, D, B), D, B)124proof125  constructor126  . exact leastCoded.function with code, offered127  . intros x hx y hy W hW first second128    obtain ⟨hx2, hW2, relatedX, leastX⟩ := leastCoded.relates.forward with129      first130    obtain ⟨hy2, hW3, relatedY, leastY⟩ := leastCoded.relates.forward with131      second132    exact separated with x, hx, y, hy, W, hW, relatedX, relatedY133134-- Hence a domain whose points are separated by candidates from a countable135-- set is countable: compose the selection with the code.136theorem leastCoded.countable (g R D B : Set)137  requires code : InjectiveBetween(g, B, ℕ)138  requires offered : ∀ x ∈ D, ∃ W ∈ B, relates(R, x, W)139  requires separated : ∀ x ∈ D, ∀ y ∈ D, ∀ W ∈ B,140    relates(R, x, W) → relates(R, y, W) → x = y141  shows Countable(D)142proof143  have injective := leastCoded.injective with code, offered, separated144  have composite := compose.injective with injective, code145  exact ⟨compose(g, leastCoded(g, R, D, B), D, B, ℕ), composite⟩146