module module high

`IndisputableMonolith.Foundation.ArithmeticFromLogic`

ArithmeticFromLogic defines the natural numbers forced by the Law of Logic as an inductive type whose identity constructor supplies the zero-cost multiplicative identity and whose step constructor generates the orbit. Modules that recover arithmetic, integers, time orbits, and recognition lattices import it to obtain the initial Peano algebra. The module supplies only the data type and basic constructors; all further arithmetic is built downstream.

claimThe natural numbers are realized as the smallest set containing the identity element (multiplicative identity of the orbit) and closed under the step operation that iterates a fixed generator $\gamma$, yielding the orbit $\{1,\gamma,\gamma^2,\gamma^3,\dots\}\subset\mathbb{R}_+$.

background

The module imports LogicAsFunctionalEquation, which encodes the Law of Logic as a functional equation whose realizations supply identity and step data. It introduces the inductive type whose two constructors mirror the multiplicative orbit starting at 1. Sibling definitions then equip this type with zero, successor, induction, and addition, all derived from the same orbit structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the LogicNat object imported by ArithmeticOf (which extracts the initial Peano algebra from any Law-of-Logic realization), by TimeAsOrbit (which identifies the temporal Tick sequence with the forced natural-number object), and by the recovered tower audit LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex. It also feeds RecognitionLatticeFromRecognizer and the number-theoretic modules that rely on the same initial algebra.

scope and limits

Does not construct a concrete numerical model or embedding into $\mathbb{R}$.
Does not prove initiality or uniqueness up to isomorphism.
Does not define addition, multiplication, or ordering; those appear in sibling files.
Does not address continuous or categorical realizations of the Law of Logic.
Does not contain the induction principle or recursion theorems; those are added downstream.

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.ArithmeticOf module_import
IndisputableMonolith.Foundation.IntegersFromLogic module_import
IndisputableMonolith.Foundation.LogicRealization module_import
IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer module_import
IndisputableMonolith.Foundation.RecoveredTowerAxiomAudit module_import
IndisputableMonolith.Foundation.TimeAsOrbit module_import
IndisputableMonolith.NumberTheory.LogicErdosStrausBoxPhase module_import
IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LogicAsFunctionalEquation module_import

declarations in this module (72)

inductive LogicNat L66
def zero L77
def succ L80
theorem zero_ne_succ L89
theorem succ_ne_zero L93
theorem succ_injective L99
theorem induction L106
def add L124
theorem add_def L132
theorem zero_def L133
theorem one_def L134
theorem add_zero L136
theorem add_succ L138
theorem zero_add L140
theorem succ_add L147
theorem add_assoc L154
theorem add_comm L161
def mul L171
theorem mul_def L177
theorem mul_zero L179
theorem mul_succ L181
theorem zero_mul L183
theorem mul_one L190
theorem one_mul L194
theorem mul_add L203
def toNat L221
def fromNat L226
theorem toNat_zero L230
theorem toNat_succ L231
theorem fromNat_zero L232
theorem fromNat_succ L233
theorem fromNat_toNat L235
theorem toNat_fromNat L243
def equivNat L253
theorem toNat_add L261
theorem toNat_mul L274
theorem add_left_cancel L286
theorem add_right_cancel L295
theorem eq_iff_toNat_eq L302
def le L325
def lt L328
theorem le_def L333
theorem lt_def L334
theorem le_refl L336
theorem zero_le L338
theorem le_trans L340
theorem le_succ L346
theorem succ_le_succ L350
theorem lt_iff_succ_le L356
theorem lt_irrefl L375
theorem lt_trans L383
theorem zero_lt_succ L387
theorem lt_iff_le_and_ne L390
theorem le_antisymm L409
theorem toNat_le L452
theorem toNat_lt L472
structure back L513
structure Generator L529
def generatorOfLawsOfLogic L541
def embed L556
theorem embed_zero L560
theorem embed_succ L562
theorem embed_pos L566
theorem embed_add L576
theorem embed_eq_pow L588
theorem log_generator_ne_zero L608
theorem embed_injective L620
theorem pow_le_pow_iff_of_one_lt L650
theorem pow_lt_pow_iff_of_one_lt L662
theorem embed_le_iff_of_one_lt L674
theorem embed_lt_iff_of_one_lt L679
theorem embed_strictMono_of_one_lt L684