Challenge.lean

import Mathlib

/-!
# Challenge: ordinary elements of one-generated Heyting algebras

This file states, **using only Mathlib vocabulary**, the principal theorems of

> *The Unique Ordinary Element of a One-Generated Heyting Algebra, the
> Subgroup Lattice of ℤ/12ℤ, and a Characterization of n = p²q*
> (`preprints/ordinary-elements-z6/` in this repository).

Every theorem below is stated with `sorry`. The proofs are imported by the
companion `Solution.lean` (via `FalseWorkPapers/Examples/ChallengeBridge.lean`),
and [comparator](https://github.com/leanprover/comparator) mechanically checks
that the solution proves **these exact statements** using only the axioms
`propext`, `Classical.choice`, `Quot.sound`.

A reviewer only needs to read this file to know what is claimed. Notation:
in a Heyting algebra, `aᶜ` is the pseudocomplement `a ⇨ ⊥` (provided by
Mathlib's `HeytingAlgebra`), and `⇨` is Heyting implication.

This file imports Mathlib **only** — nothing project-local.
-/

variable {H : Type*} [HeytingAlgebra H]

/-- An element of a Heyting algebra is **ordinary** (Citkin's term) if it is
neither *regular* (`aᶜᶜ = a`) nor *dense* (`aᶜ = ⊥`). -/
def OrdinaryElement (a : H) : Prop := aᶜᶜ ≠ a ∧ aᶜ ≠ ⊥

/-- `HeytingGeneratedBy g x`: `x` lies in the Heyting subalgebra generated
by `g` — the closure of `{g}` under `⊤`, `⊥`, `⊔`, `⊓`, `⇨`, and `ᶜ`.
(The `compl` constructor is redundant given `himp` and `bot`, since
`xᶜ = x ⇨ ⊥`; it is kept so the closure reads off the signature directly.) -/
inductive HeytingGeneratedBy (g : H) : H → Prop
  | gen : HeytingGeneratedBy g g
  | top : HeytingGeneratedBy g ⊤
  | bot : HeytingGeneratedBy g ⊥
  | sup {x y} : HeytingGeneratedBy g x → HeytingGeneratedBy g y → HeytingGeneratedBy g (x ⊔ y)
  | inf {x y} : HeytingGeneratedBy g x → HeytingGeneratedBy g y → HeytingGeneratedBy g (x ⊓ y)
  | himp {x y} : HeytingGeneratedBy g x → HeytingGeneratedBy g y → HeytingGeneratedBy g (x ⇨ y)
  | compl {x} : HeytingGeneratedBy g x → HeytingGeneratedBy g xᶜ

/-- The **Rieger–Nishimura ladder** over `g`: an enumeration of the
one-variable Heyting terms (recursion as in §2.2 of the paper; indexing
conventions vary across the literature). Rungs `0`–`4` are `⊥`, `gᶜ`, `g`,
`gᶜᶜ`, `gᶜ ⊔ g`; above that the ladder alternates implication rungs and
join rungs. -/
def rnLadder (g : H) : ℕ → H
  | 0 => ⊥
  | 1 => gᶜ
  | 2 => g
  | 3 => gᶜᶜ
  | 4 => gᶜ ⊔ g
  | (n + 5) =>
      if n % 2 = 0 then rnLadder g (n + 3) ⇨ rnLadder g (n + 2)
      else rnLadder g (n + 2) ⊔ rnLadder g (n + 3)

/-- The four regions of a Heyting algebra relative to a fixed element `a` are
all (non-trivially) inhabited:
1. something non-`⊥` lies below `a`;
2. something meets both `a` and `aᶜ` non-trivially;
3. something lies below the double negation `aᶜᶜ` without lying below `a`;
4. something non-`⊥` lies below the pseudocomplement `aᶜ`. -/
def FourRegionsInhabited (a : H) : Prop :=
  (∃ x, x ≠ ⊥ ∧ x ≤ a) ∧
  (∃ x, x ⊓ a ≠ ⊥ ∧ x ⊓ aᶜ ≠ ⊥) ∧
  (∃ x, x ≤ aᶜᶜ ∧ ¬ x ≤ a) ∧
  (∃ x, x ≠ ⊥ ∧ x ≤ aᶜ)

/-- **Non-degeneracy.** The four regions relative to `a` are simultaneously
inhabited if and only if `a` is ordinary. -/
theorem four_regions_iff_ordinary (a : H) :
    FourRegionsInhabited a ↔ OrdinaryElement a := by
  sorry

/-- **Nishimura's one-variable normal form.** Every element of the Heyting
subalgebra generated by `g` is `⊤` or a value of the Rieger–Nishimura ladder
over `g`. -/
theorem nishimura_normal_form (g : H) {x : H} (h : HeytingGeneratedBy g x) :
    x = ⊤ ∨ ∃ n : ℕ, x = rnLadder g n := by
  sorry

/-- **Uniqueness of the ordinary element.** If a Heyting algebra is generated
(as a Heyting algebra) by an ordinary element `g`, then `g` is its one and
only ordinary element. The statement appears without proof in Citkin,
arXiv:2512.05633 (p. 13). -/
theorem unique_ordinary_element (g : H) (hg : OrdinaryElement g)
    (hgen : ∀ y : H, HeytingGeneratedBy g y) (a : H) :
    OrdinaryElement a ↔ a = g := by
  sorry

/-- **The six-element threshold.** Any finite Heyting algebra containing an
ordinary element has at least six elements. -/
theorem ordinary_forces_card_ge_six [Fintype H] {g : H} (hg : OrdinaryElement g) :
    6 ≤ Fintype.card H := by
  sorry

/-- **The Z₆ order-embedding.** Any Heyting algebra containing an ordinary
element admits an order-embedding of the six-element lattice `Fin 3 × Fin 2`
(the product of a three-chain and a two-chain under the componentwise order —
equivalently, the divisor lattice of 12, or the one-generated Heyting algebra
Z₆). -/
theorem ordinary_gives_z6_embedding {g : H} (hg : OrdinaryElement g) :
    Nonempty ((Fin 3 × Fin 2) ↪o H) := by
  sorry

/-- **The arithmetic instance at n = 12.** In the divisor lattice of 12 —
`Fin 3 × Fin 2` under the componentwise order, coordinates the 2-adic and
3-adic valuations, carrying Mathlib's product Heyting structure — the four
regions are simultaneously inhabited at exactly one point: `(1, 0)`, the
divisor 2 (in the pitch-class reading of ℤ/12ℤ, the tritone). -/
theorem twelve_unique_kernel :
    ∀ a : Fin 3 × Fin 2, FourRegionsInhabited a ↔ a = (1, 0) := by
  sorry