Re: Does the number of nines increase?

On 7/4/2024 9:49 AM, WM wrote:

Le 04/07/2024 à 05:20, Jim Burns a écrit :

On 7/3/2024 4:00 PM, WM wrote:

Always almost all digits are dark.

>
All.nonempty.digit.setsⁿᵒᵗᐧᵂᴹ hold a first member.
All.digitsⁿᵒᵗᐧᵂᴹ have a first.after.digit

>
Most are unknown.

Stop misquoting.

All.nonempty.digit.setsⁿᵒᵗᐧᵂᴹ hold a first member.
All.digitsⁿᵒᵗᐧᵂᴹ have a first.after.digit and a last.before.digit,
except the first.digit, which has only a first.after.digit.

Most are unknown.

Any unknownᵂᴹ digits have nonempty.digit.sets with first members
and first.after.digits and last.before.digits.

But it is impossible to
construct or define or find or recognize or communicate
a non-terminating decimal without using a finite formula,
and be it as simple as "0.111...".

>
Answer the questions
"What is a non.terminating.decimalⁿᵒᵗᐧᵂᴹ?"  and
"What is a line.pointⁿᵒᵗᐧᵂᴹ?"
and one can prove from very reasonable assumptions
that non.terminating.decimalsⁿᵒᵗᐧᵂᴹ _exist_
and line.pointsⁿᵒᵗᐧᵂᴹ _exist_
and
a non.terminating.decimalⁿᵒᵗᐧᵂᴹ determines
no less than one real number (line.pointⁿᵒᵗᐧᵂᴹ) and
no more than one real number (line.pointⁿᵒᵗᐧᵂᴹ).

 Yes, the line point is the limit of an infinite sequence.
Example: 0.999... --> 1.
But the sequence cannot be given other than
by its defining formula like  "0.999...".

Givingᵂᴹ the sequence isn't needed in order for us
to know there is only one line.point.
10 = {0,1,2,3,4,5,6,7,8,9}
Each nonempty.subset of ℕ₁ holds a first.in.subset
For each in ℕ₁, first.after and last.before are in ℕ₁
except 1 first.in.ℕ₁ with only first.after in ℕ₁
N₁×10 is the set of all pairs ⟨n,d⟩: n ∈ ℕ₁, d ∈ 10
𝒫(N₁×10) is the set of all subsets of N₁×10
All the non.terminating.decimalsⁿᵒᵗᐧᵂᴹ exist in 𝒫(N₁×10)
But not only they are in 𝒫(N₁×10)
We describe what we mean by 'non.terminating.decimal'
and that determines the set of
all and only non.terminating.decimals.
Define
y:N₁→10  "y is a non.terminating.decimal"   ⇔
y ∈ 𝒫(N₁×10)  ∧
∀n ∈ ℕ₁:
∃d ∈ 10: ⟨n,d⟩ ∈ y ∧ ¬∃d₂≠d: ⟨n,d₂⟩ ∈ y
For simplicity,
I exclude trailing 0s
y ∃0… "non.terminating decimal y has trailing 0s"   ⇔
y:N₁→10  ∧
∃j∈ℕ₁: ∀k>j: y(k)=0
{y: N₁→10: ¬∃0…} is the set of
all and only non.terminating.decimals not.trailing.0s
For each line.point in (0,1]  there is
exactly one non.terminating.decimal in {y:N₁→10:¬∃0…}
For each non.terminating.decimal in {y:N₁→10:¬∃0…}
there is exactly one line.point in (0,1]
The proof of those claims follows from
the description of {y:N₁→10:¬∃0…} as the set of
all and only non.terminating.decimals not.trailing.0s
The proof does not apply _and isn't intended to apply_
to things which aren't
non.terminating.decimals not.trailing.0s
but, where it applies,
it is complete, no exception exists.

because it cannot be handled with enough precision.

>
Then it _exists_ and is unable to be
  handled.with.enough.precisionᵂᴹ.

>
It is handled by a formula,
sometimes even with absolute precision like 0.999... --> 1.

Consider the _terminating_ decimals {q: N₁→10: ∃0…}
(terminate == ignore trailing 0s)
for each _non.terminating_ decimal x ∈ {y:N₁→10:¬∃0…}
there is a split Fₓ Hₓ of
the _terminating_ decimals {q:N₁→10:∃0…}
for each pair ⟨x₋,x₊⟩ ∈ Fₓ×Hₓ  of
terminating fore.decimals and hind.decimals
there is a pair ⟨x′₋,x′₊⟩ ∈ Fₓ×Hₓ of
terminating fore.decimals and hind.decimals which
is apart ⅒ the distance ⟨x₋,x₊⟩ is apart.
x′₊-x₋, = ⅒⋅(x₊-x₋)
The greatest.lower.bound βₓ of
terminating.pair.distances is not positive.
| Assume βₓ > 0
| 10⋅βₓ > βₓ > ⅒⋅βₓ > 0
|
| ⅒⋅βₓ is a lower.bound
|
| 10⋅βₓ isn't a lower.bound
| There is a terminating.pair closer than 10⋅βₓ
| There is a terminating.pair closer than ⅒⋅10⋅βₓ
| There is a terminating.pair closer than ⅒⋅⅒⋅10⋅βₓ
| ⅒⋅βₓ isn't a lower.bound
| Contradiction.
Therefore,
the greatest.lower.bound βₓ of
terminating.pair.distances is not positive.
For each non.terminating x ∈ {y:N₁→10:¬∃0…}
there aren't two or more line.points between
the terminating.split Fₓ Hₓ determined by x
Otherwise,
the greatest lower.bound βₓ of x₊-x₋ would be positive,
which is contradictory.

It is handled by a formula,
sometimes even with absolute precision like 0.999... --> 1.

For each non.terminating.decimal in {y:N₁→10:¬∃0…}
there is no more than one line.point in (0,1]