feat(Incompleteness): discharge the 𝗣𝗔 / 𝗜𝚺₁ Δ₁-definability axioms

[gotrevor]

What

Discharges the two axioms upstream master currently ships in
FirstOrder/Incompleteness/Examples.lean (they rode in via the v4.31 port FormalizedFormalLogic#830):

axiom ISigma1_delta1Definable : 𝗜𝚺₁.Δ₁
axiom PA_delta1Definable       : 𝗣𝗔.Δ₁

Both are now proven (the axiom keyword + attribute [instance] block are removed;
the proofs live in the new InductionSchemeDelta1.lean and are picked up as instances).

A note on review scope

This proof was Claude Code generated, and I (@gotrevor) cannot defend or
validate the ~1400 lines of InductionSchemeDelta1.lean , formally or mathematically.

What I can stand behind is mechanical and checkable:

• It discharges the exact two axioms already in your tree (Examples.lean), under identical
  signatures — nothing new is asserted; the axiom keyword is simply replaced by a proof.

So the kernel vouches for internal consistency, but whether the internal Σ₁ recognizer faithfully
captures the induction schema is a mathematical judgment I'd rather leave to your review than assert
myself.

Route

𝗣𝗔 = 𝗣𝗔⁻ ∪ InductionScheme ℒₒᵣ Set.univ, 𝗜𝚺₁ = 𝗣𝗔⁻ ∪ InductionScheme ℒₒᵣ (Hierarchy 𝚺 1).
𝗣𝗔⁻ is finite (Theory.Δ₁.ofFinite); Theory.Δ₁.add/.ofEq reduce both headlines to the
single obligation (InductionScheme ℒₒᵣ C).Δ₁, established via an internal Σ₁ recognizer.

Port notes

Rebased the pre-FormalizedFormalLogic#794 proof onto current master. Three adjustments vs FormalizedFormalLogic#794's FirstOrder redesign:

• model satisfaction [V ⊧ₘ* 𝗜𝚺₁] → [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (language made explicit)
• re-introduced the SyntacticSemiformula / SyntacticFormula abbreviations (change(FirstOrder): redesign FirstOrder FormalizedFormalLogic/Foundation#794 removed the
  formula-level ones; the term-level SyntacticSemiterm/SyntacticTerm survive) — happy to inline
  Semiformula L ℕ n instead if you prefer the new convention
• Function.comp_apply in one simp only (Rew.func now normalises the arg map to ∘)

Verification

• Axiom-clean:

  #print axioms PA_delta1Definable   → [propext, Classical.choice, Quot.sound]
  #print axioms ISigma1_delta1Definable → [propext, Classical.choice, Quot.sound]
  

Audit surface

The load-bearing statements are the two axiom signatures being discharged, in Examples.lean.
Supersedes the fork-internal #6 (pre-FormalizedFormalLogic#794 base).

🤖 Generated with Claude Code

[gotrevor]

Submitted upstream: FormalizedFormalLogic#833