The theorem induction in module IndisputableMonolith.Foundation.ArithmeticFromLogic recovers Peano induction as a theorem for the type LogicNat forced by the Law of Logic.
LogicNat is defined inductively with constructors identity (zero) and step (successor). The theorem states:
∀ {motive : LogicNat → Prop},
motive zero →
(∀ n, motive n → motive (succ n)) →
∀ n, motive n
Proof: apply Lean's induction tactic to the constructors of LogicNat. Base case identity uses the zero hypothesis directly. Inductive step step n applies the successor hypothesis to the inductive hypothesis.
This establishes Peano axiom P3 without positing it: any property holding at the identity element and closed under the generator step holds for the entire orbit. The surrounding module shows LogicNat is isomorphic to Nat via equivNat, transferring the induction principle to standard arithmetic.