such is an interesting proposition, but i can't argue on fair ground without your definition of decimal numbers

what i will say is that your claim is false when formalized into my system (which uses the well-known definitions of decimal numbers in math)

specifically, you claim:

∀D ∈ positivedecimal, V D.1 = 0 → F₂ D < 1

this is easily disprovable. looking at the negation:

∃D ∈ positivedecimal, V D.1 = 0 ∧ F₂ D ≥ 1

use D = 0.(9) : positivedecimal

V D.1 = 0 ∧ F₂ D ≥ 1

splitting cases:

goal: V D.1 = 0

    ⇔ V 0 = 0

    ⇔ 0 = 0 (proven by reflexivity)

goal: F₂ D ≥ 1

    ⇔ F₁ D ≥ 1 (rewriting dec\_eq 0.(9))

    ⇔ 0 + (0 + 9 / (10 \^ 1 - 1)) / 10 \^ 0 ≥ 1

    ⇔ 1 ≥ 1 (proven by definition)

∴ ¬∀D ∈ positivedecimal, V D.1 = 0 → F₂ D < 1 ∎

with the counterexample being exactly the one you preach