LogicNat
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 1205)
-
AI optimizers cannot recognize or settle hard choices
"Hájek and Rabinowicz propose that incommensurability arises from multiple permissible orderings"
-
Contextual model explains Heisenberg microscope back-action
"COM uses a specific initial distribution of its state, and a slightly modified measurement update with respect to SSTR"
-
vMODB Unifies Events and Data for ACID Microservices
"deterministic transaction execution scheme... TiD assignment... batch commit"
-
LLM datetime primitives unreliable but learnable via synthetic data
"PRIMETIME synthetic generator delivers non-conflated, uncontaminated datetime exemplars... primitives themselves prove individually unreliable... fine-tuning... Event Planning task reaches frontier-level accuracy"
-
All final-year students reconstruct experiences to guide future practice
"By the final year, all students demonstrate the ability to reconstruct their experiences to inform future practice."
-
Tauberian theorems explained with proofs and sharpness checks
"Hypothesis A... A(s) = g(s)/(s−α)^m + h(s) ... Theorem A: X_{λ_n ≤ x} a_n ∼ c x^α (log x)^{m−1}"
-
Aggregation rules normalize utilities for fair choices under uncertainty
"0–1 normalization of individual utilities ... Independence of Inessential Expansion (IIE)"
-
Exact algorithm finds two-layer network with fewest misclassifications
"DeepICE(D, K) = min 0-1 (K) ◦ eval(K) ◦ cp(basgns(K)) ◦ nestedCombs(D, K)"
-
Compositions count permutations avoiding pattern chains with squares
"π = ⊕ ϵ_{d_i} for composition d of n; π² = ⊕ ϵ²_{d_i}; avoidance of chain (312,321:σ) ⇔ d avoids C(σ)"
-
Explicit 1-point functions computed for Z2-orbifolds of lattice VOAs
"Z2-twisted Zhu Theory ... Twisted Recursion Formulas"
-
Drum grooves edited zero-shot by plain LLMs via spatial text grid
"We introduce a novel text-based “drumroll” notation that translates musical mechanics into a spatial, syntax-driven grid... each character represents a 16th note, grouped by 4 into beats separated by |."
-
Explicit formulas given for sumset sizes of k-element sets
"RZ(h,k) = {|hA| : A subset Z, |A|=k}"
-
Representer theorem yields finite sparse RBF solutions for nonlinear PDEs
"the function space of Reproducing Kernel Banach Spaces induced by one-hidden-layer neural networks"
-
Two-level sketching halves Anderson acceleration time in PDEs
"alternating Picard/Anderson updates with window m and sketching percentages (10% matvec, 80% QR)"
-
ServeGen halves under-provisioning in LLM serving benchmarks
"ServeGen performs principled modeling of workloads on a per-client basis... to generate realistic workloads"
-
Personalized AI adapts foundation models without sharing data
"RAG-assisted Fine-Tuning and Continual Pre-Training for Foundation Models"
-
Explicit formula for Gauss sums on finite ring units
"Theorem 4.5: If MR((x)ℓ) is minimal subset of itself, then Cα(x) = μ_R(K,(x)ℓ) |[x]ℓ| / φ_R(K,(x)ℓ)"
-
Diffusion repair turns evolutionary crossovers into valid 3D molecules
"tri-population architecture with distinct goals: exploring novel chemical scaffolds, refining partially assembled intermediates, and fine-tuning perfectly feasible elite molecules"
-
QCP verifies C programs by mixing automatic checks with Rocq proofs
"QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof."
-
Latent-space attacks fool pose estimators without visible changes
"strict test budget... only three queries of the model outputs"
-
Limited old prompts reduce forgetting when tuning LLMs on new tasks
"The results demonstrate the superior performance of our method in improving generalization on new tasks and reducing forgetting in old tasks."
-
Multiple schema views let cheap models match costly text-to-SQL
"N-rep adopts a confidence-aware two-stage candidate selection strategy that combines regular self-consistency voting with CHASE-SQL’s LLM-based pair-wise voting."
-
Benchmark divides math reasoning into four parts to expose LLM gaps
"Inspired by Pólya’s problem-solving theory, we propose SMART, a benchmark that decomposes mathematical problem-solving into four cognitive dimensions: Semantic Understanding, Mathematical Reasoning, Arithmetic Computation, and Reflection & Refinement"
-
MCTS templates steer RL to higher-quality LLM reasoning paths
"Proposition 3.1 (Stability and positive-sample guarantee) ... grouping increases Ppos"
-
Rubidium vapor cavity switch reaches 22 ns rise time at 2.4 dB loss
"The maximum operational speed is governed by the cavity ring-down time which is estimated down to approximately 20 ns."
-
Dataization dampens tech-driven equilibrium shifts
"numerical simulation of θ,η effects on k*,c*; phase diagrams; DID on data-openness policies"
-
Higher dimensions tolerate stronger attacks in two-way QKD
"Purified LM05 protocol... entropic uncertainty relation S_B|E + S_B|E >= log2(1/gamma)"
-
Exact Shapley values for product kernels in quadratic time
"Definition 1. ... νxxx(S) = α⊤ kS(XS, xxxS). ... removing a feature replaces its kernel factor with the multiplicative identity."
-
Event adaptation lifts performance in dynamic graph prompts
"extract K historical events... event aggregation... plug-in to existing methods"
-
One Transformer forecasts stability across any power grid
"GPT architecture ... causal attention mechanisms ... two-stage fine-tuning scheme (teacher forcing + scheduled sampling)"