module module high

`IndisputableMonolith.Foundation.ArithmeticFromLogic`

This module defines the natural numbers forced by the Law of Logic as an inductive structure with identity (zero-cost multiplicative identity) and step (generator). Researchers building the number tower from functional equations cite it as the initial Peano algebra. The module consists of inductive definitions that realize the smallest orbit closed under the generator.

claimThe natural numbers are the inductive type generated by the zero-cost element (identity) and the successor (step), realizing the orbit $1, γ, γ^2, …$ as the smallest subset of $ℝ_+$ containing 1 and closed under multiplication by $γ$.

background

The module imports LogicAsFunctionalEquation, which supplies the underlying functional equation whose solutions force arithmetic structure. It introduces LogicNat with two constructors: identity (the multiplicative identity at zero cost) and step (one iteration of the generator). This mirrors the orbit construction in positive reals and supplies the initial object for subsequent arithmetic extraction.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies LogicNat as the initial Peano algebra that ArithmeticOf uses to extract arithmetic and that feeds the number-tower recovery in RecoveredTowerAxiomAudit and TimeAsOrbit. It realizes the first step of Universal Forcing by turning the Law-of-Logic realization into the canonical natural-number object.

scope and limits

Does not prove any arithmetic identities or induction principles.
Does not define addition, multiplication, or ordering.
Does not address integers, rationals, or reals.
Does not depend on specific constants such as phi or the eight-tick octave.

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