pith. sign in
inductive

LogicNat

definition
show as:
module
IndisputableMonolith.Foundation.ArithmeticFromLogic
domain
Foundation
line
66 · github
papers citing
1323 papers (below)

plain-language theorem explainer

LogicNat encodes the natural numbers forced by the Law of Logic, with identity as the zero J-cost base element and step as the generator. Researchers deriving arithmetic primitives from the recognition functional equation cite this inductive type as the starting point. The definition is a direct two-constructor inductive that mirrors the multiplicative orbit closed under the generator.

Claim. The type of natural numbers is defined inductively with constructors identity (the zero J-cost multiplicative identity) and step (one iteration of the generator), forming the smallest subset of positive reals closed under multiplication by the generator and containing 1.

background

LogicNat appears in the ArithmeticFromLogic module, which builds arithmetic from the functional equation imported via LogicAsFunctionalEquation. The identity constructor matches the zero-cost event defined in ObserverForcing.identity, where state equals 1 and J-cost reaches its minimum. The step constructor parallels the successor operation in CellularAutomata.step, which applies a local rule to produce the next tape state.

proof idea

This is a direct inductive definition with exactly two constructors. No lemmas or tactics are invoked; the declaration itself supplies the type and its generators.

why it matters

LogicNat supplies the base type for add, add_assoc, add_comm, and related arithmetic theorems in the same module. It fills the initial step in deriving Peano primitives from the Law of Logic, linking to the forcing chain where J-uniqueness produces the phi fixed point and the eight-tick structure. The declaration touches the open question of recovering full induction and cancellation laws inside the recognition framework.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 1323)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.