Reference · Logic

rainbow.math.logic.exhaustive-carrier-fintype

Logicsrc/rainbow/math/logic/exhaustive_carrier_fintype.clj1 definitions, 2 theorems

Constructively connect executable exhaustive carriers to extensional Fintype. `finset-data/Finset` retains a duplicate-free enumeration in Type, while `fintype/Fintype` packages an extensional finite set complete for its ambient type. A certified exhaustive carrier has exactly the evidence needed to map in the constructive direction: keep its executable enumeration, project it to an extensional finset, and reuse coverage as Fintype completeness. The reverse direction is intentionally not claimed: propositional Fintype completeness cannot in general be eliminated to recover executable data. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.diagonal-spike

finite/fintype-of-certified-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool)
  (certificate : finite/certified-exhaustive-carrier S states decision)
  → fintype/Fintype S

finite/fintype-elements-of-certified-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool)
  (certificate : finite/certified-exhaustive-carrier S states decision)
  → fintype/elements S (carrier) = finset-data/to-extensional S states
  where carrier := finite/fintype-of-certified-exhaustive-carrier S states decision certificate

finite/type-finite-of-certified-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool)
  (certificate : finite/certified-exhaustive-carrier S states decision)
  → type/finite S