module module high

`IndisputableMonolith.Foundation.ArithmeticFromLogic`

This module defines the natural numbers as the initial algebra forced by the Law of Logic, using an inductive type whose identity constructor supplies the zero-cost base and whose step constructor supplies the generator. Researchers recovering arithmetic from functional equations or building the universal forcing tower cite it as the entry point for LogicNat. The definition is given directly by a two-constructor inductive structure that encodes the smallest multiplicative orbit containing 1.

claimLet $N$ be the inductive type generated by an identity element $e$ (the zero-cost multiplicative identity) and a successor operation $s$ (one iteration of the generator). This $N$ is the smallest subset of the positive reals containing 1 and closed under multiplication by the generator, forming the initial Peano algebra under the Law of Logic.

background

The module sits inside the Recognition Science program that derives arithmetic from a single functional equation. It imports the Law of Logic realization from LogicAsFunctionalEquation and introduces LogicNat together with its constructors identity and step. Identity stands for the zero-cost element of the orbit while step encodes one further iteration of the generator, exactly as described in the module doc-comment.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the LogicNat object that downstream files use to extract arithmetic. ArithmeticOf treats it as the initial Peano algebra generated by the supplied identity and step data, thereby realizing the universal forcing mechanism. TimeAsOrbit identifies the temporal sequence Tick with this same natural-number object, and the recovered tower audit chains it onward to LogicInt through LogicComplex.

scope and limits

Does not derive addition or multiplication operations.
Does not prove the full Peano axioms in this file.
Does not connect explicitly to the J-functional equation or phi-ladder.
Does not treat continuous or non-discrete realizations.

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