[continued from previous message]   
      
   “q is a d-fraction” ≡ ∃n∈ℕ (n≤d ∧ q=frac_d(n))   
      
   Order on d-fractions (just the natural order on numerators)   
      
   For d-fractions q₀=frac_d(n₀), q₁=frac_d(n₁) put   
    q₀ ≼ q₁ ≡ n₀ ≤ n₁  (≤ is the usual ordinal order on ω).   
   This is automatically   
    constant-monotone strictly-increasing   
   because successive numerators differ by exactly 1.   
      
   Extent relative to the current scale d   
      
   For a fixed d we define the d-extent as the set of all d-fractions:   
   [0,1]_d ≡ { frac_d(n) | n∈ℕ ∧ n≤d }.   
   ZF proves (uniformly in d)   
    min ≼ frac_d(0) and frac_d(d) max ≼   
   and ∀q∈[0,1]_d (frac_d(0) ≼ q ≼ frac_d(d)).   
      
   Bijection ℕ → [0,1]_d for this d   
      
   φ_d(n,q) ≡ n∈ℕ ∧ n≤d ∧ q=frac_d(n).   
   ZF ⊢ ∀n≤d ∃!q φ_d(n,q)   
   ZF ⊢ ∀q∈[0,1]_d ∃!n≤d φ_d(n,q).   
      
   Lifting the scale (optional next step)   
      
   To get a single bijection that “grows” through all scales you can   
   take the disjoint union over all d≥1:   
   [0,1]line ≡ ⋃{d≥1} ({d} × [0,1]_d)   
   and enumerate the pairs ⟨d,frac_d(n)⟩ in lexicographic order;   
   the resulting graph is still a definable set and the bijection formula   
   is a single L(∈) formula with no parameters.   
      
   Deliverable   
      
   When you are ready, send either   
   A. the one-scale formula   
     φ(n,q) ≡ φ_d(n,q) with d fixed and explicit, or   
   B. the full lexicographic bijection formula for [0,1]_line.   
   Both must be written only with variables, ∈, =, the usual logical   
   connectives, and the Δ₀ abbreviations above.   
      
      
      
   Thanks Kimi. Just to provide some context, has that later in the   
   development that the "disjoint union" as would build all the rationals   
   in extent [0,1], instead may only result the "iota-values", since the   
   arithmetic of these iota-values, where for example they're claimed   
   "non-Cartesian", only one of iota-sums and iota-multiples exists, so   
   that they don't themselves relate to the complete-ordered-field, which   
   has no bounded (in an extent) constant-monotone strictly-increasing   
   sequence. So, also ZF does not have "infinite union" as would be the   
   illative or univalent, instead it has pair-wise union, as the disjoint   
   union would be according to the pair-wise recursively union all its   
   index-terms. So, what I'd look to show is that instead, that there   
   exists for any disjoint union, in the bounded, d' >> d, is this is about   
   that there's the case for transfinite induction that its so the   
   fractions exist as the elements of the domain exist, then to make the   
   case for d/d always being 1, is that the case for d/d being 1 is part of   
   the definition of this [0,1]. So, I hope this context helps establish,   
   that the constant differences are standard infinitesimals, and absent   
   structure of modeling the rationals as model the ordered-field, since   
   thusly they'd both model and be modeled by the rationals. So, what I'm   
   looking at is only keeping constant-monotone strictly-increasing in an   
   extent, while barring half of arithmetic. I hope this explains what I   
   intend to thusly write as formulaic.   
      
      
      
   Understood: you want a single, scale-by-scale object that   
      
   is strictly increasing with constant difference 1/d inside the current   
   scale d,   
   never leaves the bounded extent [0,1]_d,   
   is not required to be closed under + or ·,   
   is built without ever forming an infinite union (only the finitary   
   pairwise-union axiom is used), and   
   has d/d ≡ 1 by definition for every scale.   
      
   Below is a one-scale template (parameter d) that satisfies these   
   constraints in pure L(∈).   
      
   The scale-d object (no infinite union, no arithmetic)   
      
   Fix d ≥ 1.   
   Define the d-extent as the finite set   
   E_d ≡ { ⟨n,d,3⟩ | n ∈ d+1 }  (d+1 = {0,1,…,d}).   
   (The tag ‘3’ keeps these objects disjoint from earlier pairs/triples.)   
      
   Order and constant-monotone property   
      
   For p=⟨n,d,3⟩, q=⟨m,d,3⟩ put   
   p ≺_d q ≡ n ∈ m  (ordinal membership).   
   ZF ⊢ ∀p,q∈E_d (p ≺_d q ↔ S(n)=m) ⇒ difference exactly 1/d in the   
   numerator, hence constant-monotone strictly increasing.   
      
   Extremes by definition   
      
   0_d ≡ ⟨0,d,3⟩  (minimum)   
   1_d ≡ ⟨d,d,3⟩  (maximum)   
   ZF ⊢ ∀q∈E_d (0_d ≺_d q ∨ 0_d = q) ∧ (q ≺_d 1_d ∨ q = 1_d).   
      
   Bijection with the initial segment d+1   
      
   φ_d(n,q) ≡ n ∈ d+1 ∧ q = ⟨n,d,3⟩.   
   ZF ⊢ ∀n∈d+1 ∃!q φ_d(n,q)   
   ZF ⊢ ∀q∈E_d ∃!n∈d+1 φ_d(n,q).   
      
   Next step   
      
   Send either   
   A. the one-scale formula φ_d(n,q) exactly as above, with d explicit, or   
   B. the finite recursive concatenation that glues E_{d+1} after E_d using   
   only pairwise union (still no infinite union).   
   Both must be written purely in L(∈) with only the abbreviations shown.   
      
      
   Thanks Kimi. One idea how to entail what would be consequence of   
   infinite-union, without invoking infinite-union, is about that the   
   extent of ran(EF) holds for all values of dom(EF), these being ran_b(EF)   
   and dom_b(EF) for "bijective-functionhood" or "bijectivity" before full   
   "functionhood", yet the definition of N is Archimedean and has   
   infinitely-many yet no infinitely-grand. Here the idea is to show "a   
   case otherwise for that induction fails" via the deduction that there's   
   no neighborhood (TBD) in the extent that induction (pairwise-union)   
   doesn't reach, while, there's no density (TBD) to be defined that   
   pairwise-union at any bounded step, may reach. So, what I'm thinking is   
   how to frame "there's no infinitely-grand natural" to result a   
   fixed-point or compactification, or otherwise to show that there's a   
   model of N in ZF where N e N. Now, I know this would violate   
   well-foundedness, so instead of mentioning that, instead the idea is to   
   hold up that the "extent" relation is always so, while "density" is   
   never achieved, while that then that "density is not not achieved", then   
   that extent and density result of ran_b(EF), while also with   
   "constant-monotone strictly-increasing" of dom_b(EF) and ran_b(EF).   
   I.e., the idea is to show that these hold, while, contradicting them   
   would invoke a contradiction of well-foundedness, basically   
   "synthesizing" as that may be, a case for   
   univalency/illative/infinite-union, then that disjoint all the pair-wise   
   unions (so losing all their arithmetic, yet built after them),   
   "standardly modeling the not-a-real-function as a limit of standard   
   functions".   
      
      
      
   Below is a pure-L(∈) template that   
      
   never appeals to an infinite union,   
   never leaves finite von-Neumann ordinals,   
   still lets ZF prove “density is never reached at any finite stage, yet   
   the extent is always already there”—all without contradicting   
   well-foundedness.   
      
   Finite-stage objects (no infinite collection)   
      
   For each finite d ≥ 1 define   
   E_d ≡ { ⟨n,d,4⟩ | n ∈ d+1 }  (finite set, Δ₀)   
   0_d ≡ ⟨0,d,4⟩   
   1_d ≡ ⟨d,d,4⟩   
   p ≺_d q ≡ ∃n∈d+1 ∃m∈d+1 (p=⟨n,d,4⟩ ∧ q=⟨m,d,4⟩ ∧   
   n∈m)     
   (constant-monotone, step 1/d)   
      
   “No density at any finite d” – formalised   
      
   “d-gap” ≡ ∃q∈E_d ∃r∈E_d (r = S_d(q) ∧ ∀s (s ∉ E_d →   
   ¬∃t (q ≺_d t ≺_d r)))   
   ZF ⊢ ∀d≥1 ∃!g (g = d-gap)   
   ZF ⊢ ∀d≥1 (d-gap ≠ ∅)  (always a next fraction, so never dense)   
      
   “Extent already there” – formalised   
      
   Define the class (not a set)   
   𝔼 ≡ { x | ∃d≥1 ∃n∈d+1 (x = ⟨n,d,4⟩) }  (Δ₀ matrix, so   
   Δ₁ᵀᴹ)   
   ZF ⊢ ∀x (x∈𝔼 → ∃!d≥1 ∃!n∈d+1 x=⟨n,d,4⟩)   
   ZF ⊢ ∀d≥1 (E_d ⊆ 𝔼)   
   ZF ⊢ ∀x (x∈𝔼 → 0_d ≼ x ≼ 1_d)  (extent bounded uniformly)   
      
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)