theorem
proved
embed_eq_pow
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 588.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
step -
embed -
Generator -
LogicNat -
succ -
toNat -
of -
embed -
identity -
is -
of -
from -
is -
of -
for -
is -
of -
is -
and -
value -
succ -
identity
used by
formal source
585 ring
586
587/-- The embedding is the natural-number power of `γ.value`. -/
588theorem embed_eq_pow (γ : Generator) (n : LogicNat) :
589 embed γ n = γ.value ^ (LogicNat.toNat n) := by
590 induction n with
591 | identity => simp [embed, LogicNat.toNat]
592 | step n ih =>
593 show γ.value * embed γ n = γ.value ^ (Nat.succ (LogicNat.toNat n))
594 rw [ih, pow_succ]
595 ring
596
597/-! ## Embedding Injectivity (J-positivity off identity)
598
599The key fact: a non-trivial generator `γ ≠ 1` cannot have `γⁿ = γᵐ`
600for `n ≠ m`. Structurally, this is forced by J-positivity off
601identity: `J(γᵏ) > 0` for any `k ≥ 1` (since `γᵏ ≠ 1` whenever
602`γ ≠ 1` and `k ≥ 1`), and `J(x) = 0 ↔ x = 1`. Analytically, it
603follows from `Real.log γ.value ≠ 0` and the rule `log(γⁿ) = n · log γ`
604on positive reals. The latter route is shorter and is what we use
605here. -/
606
607/-- Logarithm of a non-trivial generator is non-zero. -/
608private theorem log_generator_ne_zero (γ : Generator) :
609 Real.log γ.value ≠ 0 := by
610 intro h
611 -- Real.log_eq_zero_iff: log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
612 rcases (Real.log_eq_zero.mp h) with h0 | h1 | hneg
613 · exact (lt_irrefl (0 : ℝ)) (h0 ▸ γ.pos)
614 · exact γ.nontrivial h1
615 · linarith [γ.pos]
616
617/-- **Embedding injectivity**: distinct natural numbers map to distinct
618points in the orbit. This closes the bridge from the abstract `LogicNat`
papers checked against this theorem (showing 16 of 16)
-
HfTe5 oscillations evolve from Landau levels to log-periodic
"discrete scale-invariant energy spectrum of quasi-bound states ... ε_{i+1}/ε_i = λ"
-
Congruential Euler numbers satisfy p-adic congruences and yield zeta expressions
"Theorem 1.3 ... λ(4n) = ... sum binom E^(4,0)_{4m} ... ζ(4n) = ..."
-
Multidimensional binomial matrix joins Riordan group
"The multidimensional binomials appear in the expansions (1+x)^k = sum binom(k,k') x^{k'} and the generating-function representation of the Riordan basis (G,X)."
-
Nonlinear quantum waves recover linear Fourier-Bessel spectra
"a linear spectral structure re-emerges through a Jacobi–Anger expansion, yielding a Fourier–Bessel representation with square-summable coefficients"
-
Gaussian POVMs remap image intensities continuously
"The remapped intensities are obtained as expectation values... ˆI(x,y) = Σ μ_k P_k(x,y)"
-
Mobility data places cities in hyperbolic geometry
"distributions of hierarchy measures... exhibit power law behavior... double pareto distributions"
-
Fourier transform turns pixel shifts into diagonal multiplications for QCNNs
"The shift operator T is diagonal in the Fourier basis: F_N T F†_N = diag(ω^k)"
-
Non-Hermitian system shows complementary Lucas sequences
"Eq. (2) is a special example of the linear recurrence relation... α = 1 for linear localization is satisfied by γ = 2t"
-
Weighted SFT matches KL-regularized RLVR policy
"Refreshed Boltzmann projection ≡ KL policy mirror descent: π_{θ_{k+1}} ∝ π_{θ_k} exp(r/β); after K rounds π ∝ π_0 exp(Kr/β)."
-
Dual-branch model predicts glioma infiltration zones on MRI
"Zone 3 (high risk) ... within 10 mm ... Zone 2 (medium risk) covers the 10–20 mm transition region. Zone 1 (low risk) includes brain tissue beyond 20 mm."
-
DFT parameters feed scale-bridging simulations of cobalt ferrite magnetism
"H = −Σ J_ij S_i·S_j + H_ani + H_Z (classical Heisenberg Hamiltonian with Zeeman and cubic anisotropy K1(α1²α2² + α2²α3² + α3²α1²))."
-
POO optimizes noisy functions with unknown smoothness within sqrt(log n) of optimal
"POO's simple regret: E[R_n] ≤ O((ln² n / n)^{1/(2+d(ν⋆,ρ⋆))})"
-
Reasoning models still miss many false user assumptions
"five presupposition levels (ℓ ∈ {0,1,2,3,4}) ... Neutral, Mild Presupposition, Unequivocal Presupposition, Writing Request, Writing Demand"
-
Hyperbolic group metrics correspond to reparameterized flows with integer periodic orbits
"we produce the first examples of continuous reparameterizations of geodesic flows on negatively curved manifolds with all periodic orbits having integer lengths"
-
Non-Markovian master equation gains exact memory integral
"K_{n+1}[pϱ_n,...,pϱ_0] = p K_{n+1}[ϱ_n,...,ϱ_0] ... convex-linear maps on the base of a convex cone have a unique extension to the whole cone which is homogeneous of degree one"
-
Schwinger integral captures instantons in cutoff-bounded window
"α_i := −∇ log(m_i / M_Pl^(d)); S-vectors S_i := −∇ log S_i (gradients in canonically normalized moduli)."