[continued from previous message]   
      
   Facts inside ZF   
      
   “x is irrational” is Δ₀ on the rational intervals, so S is a set by   
   Separation.   
   min S = s, the least element > 0.   
      
   If you prefer the set of all irrationals > 0, take   
   T = { x ∈ ℝ | x is irrational ∧ x > 0 };   
   then T has no least element (every ε > 0 contains smaller irrationals),   
   but S above is the required example with a least member.   
      
   An irrational with only countably-many smaller irrationals   
      
   Take p = 1/√2.   
   The set of irrationals below p is   
   L_p = { x ∈ ℝ | x is irrational ∧ 0 < x < p }.   
   ZF proves   
   |L_p| = ℵ₀.   
   Proof sketch (ZF)   
      
   The map x ↦ x/p injects L_p into the irrationals in (0,1).   
   The latter injects into ℚ×ℚ via continued-fraction convergents (or any   
   explicit enumeration of denominators), so |L_p| ≤ ℵ₀.   
   ℚ itself injects into L_p by q ↦ q/√2, so |L_p| ≥ ℵ₀.   
   Hence |L_p| = ℵ₀ (no Choice used).   
      
   What this means for EF / “E-extent”   
   Your bookkeeping gadget   
   EF(n) = ⟨n,d,6⟩ with d→∞ (n≤d)   
      
   never leaves finite d,   
   never forms an infinite set,   
   never produces an uncountable set of reals,   
   never intersects the irrationals in any interval except finitely many at   
   each scale.   
      
   Hence ran(EF) is a proper class of finite rational approximations, not   
   an uncountable set of irrationals, and Cantor’s lasso never touches   
   it—because nothing in the arena is a set that violates uncountability.   
   Ring when you want the final layer: a conservative two-sorted extension   
   whose t-sort is interpreted as the tagged tuples ⟨n,d,6⟩ while measure-1   
   shadows inherit Lebesgue outer measure—consistency proved by a single   
   ω-model of ZFC.   
      
      
   Thanks Kimi. The domain dom(EF) is infinite so ran(EF) can't be finite.   
   Indeed the "book-keeping" keeps it above mere induction since the   
   deductive account has that otherwise dom(EF) would be finite, since that   
   N is infinite is given as an axiom. About defining EF or "measure-1   
   shadows" or "the elements of Jordan measure" _outside_ of ZF, the   
   "extent densty completeness measure" or the "constant-monotone strictly   
   increasing" gets modeled by any [0,1], thusly, the problems won't go   
   away until it's admitted that EF is not-a-Cartesian-function, since the   
   only problem is that Cartesian functions suffer (in this case, otherwise   
   enjoy) CSB "Cantor's lasso", or "Cantor's vonNeumann's lasso",   
   Cantor-Schroeder-Bernstein, with Cantor-Bernstein that cardinals are   
   transitive under composition of bijections and Schroeder that   
   surjections and injections both ways suffice for bijections, the only   
   problem is that EF would be re-ordered under composition, since that's   
   the defining relation that otherwise these noted arguments about   
   induction, show that even usual integration like the line-integral of a   
   straight line get contradicted.   
      
      
      
      
   Below I keep the rope inside ZF and answer in three short, tied-off points.   
      
   “dom(EF) infinite ⟹ ran(EF) infinite”   
   False in ZF. The graph   
   f = { ⟨n, ⟨n,d,6⟩⟩ | d = least k ≥ 1 s.t. n ≤ k }   
   has domain = ω (infinite) but range ⊆ E_d with d = max{n} on each finite   
   initial segment;   
   hence every set-image f↾m is finite, and no single set contains all   
   tagged tuples.   
   “CSB would force re-ordering under composition”   
   CSB never touches the object: it only says “if two sets inject into each   
   other, they biject”.   
   Since ran(EF) is not a set, no bijection ℕ → ran(EF) is even   
   expressible, so no CSB contradiction arises.   
   “Line-integral contradiction”   
   Finite rational tags never enter the σ-algebra of Jordan sets in ℝ;   
   measure-1 shadows are finite-scale illusions, not intervals, and never   
   intersect the uncountable chain that Jordan measure requires.   
      
   Bottom line (ZF)   
      
   Non-Cartesian tagging is only ink; the graph is an ordinary set with   
   finite range.   
   No re-ordering is ever imposed on the tagged tuples, because no   
   set-level bijection is ever claimed.   
   Line-integrals, CSB, and Jordan measure remain intact; the only thing   
   rescued is heuristic intuition, not ZF consistency.   
      
   Ring when you have a ZF formula that allegedly defines ran(EF) as an   
   infinite set—we will derive its finitude in three lines.   
      
      
      
      
      
   Thanks Kimi. Uncountably-many integrable regions would result   
   "inconsistent multiplicities", so, both Jordan and also Riemann/Lebesgue   
   integrals are countably-many vanishing-width integrable regions with   
   "constant-monotone strictly increasing" their differences between   
   boundaries of integration, _and for no finite approximation is that   
   integral generally correct_. Then, about book-keeping and E-extent, and   
   about the pairwise-union versus infinite-union, I simply take away the   
   un-fulfilled finite scales yet what must have resulting an infinite   
   scale, _since the domain is infinite else N is not infinite_, so "E"   
   here means "an infinite set, or class, this [0,1]_t", that's only   
   defined as ran(EF) and where f^-1(1) = infinity, f^-1(0) = 0, and m < n   
   -> f(m) < f(n), and n - m = o -> f(n) - f(m) = f(o). So, it's still   
   deemed easier to show that it's a lemma of Cantor's theorem that a   
   non-Cartesian functions exists, especially since that it's   
   constructively built itself this EF with "extent, density, completeness,   
   measure", that's a continuous domain and it doesn't conflict with   
   Dedekind's, though like Cantor's it just show that there's another thing   
   that "wouldn't exist", composition of functions except about [0,1]_t.   
   Then, showing that vonNeumann ordinals alone would make for themself a   
   Russell's paradox, or later about ordinals that they either do or don't   
   exist between otherwise cardinals or the Independence of the Continuum   
   Hypothesis, has that they do or don't. Then, about the powerset theorem   
   and ordinals, while this EF falls out of uncountability-arguments   
   themselves uncontradicted, then there's a model of ZF that's a model of   
   ordinals to model where the successor is powerset is ordertype is a   
   counterexample to powerset result in that model of "ubiquitous   
   ordinals", not unlike Cohen's forcing. So, what I intend is to keep   
   breaking ZF, or to use reverse-mathematics to break theories with only   
   some ZF axioms mostly expansion-of-comprehension, when modeled in ZF,   
   while maintaining showing that non-Cartesian functions their existence   
   is a lemma of Cantor's theorem.   
      
      
      
      
      
   Kimi here—let’s keep the rope inside ZF and state the exact lemma you   
   want to extract from Cantor’s theorem.   
   Claim (your words):   
   “Cantor’s theorem implies that non-Cartesian functions exist, because EF   
   (defined by book-keeping /d)   
      
   has infinite domain ℕ,   
   satisfies n – m = o ⇒ f(n) – f(m) = f(o) (Cauchy-style),   
   produces ran(EF) = [0,1]_t (a continuous domain),   
   and this escapes the powerset theorem / CSB lasso.”   
      
   Formal test (three lines)   
      
   Graph of EF   
   f = { ⟨n,⟨n,d,6⟩⟩ | d = least k≥1 with n≤k }   
   is a set (Δ₀ separation), domain = ℕ, but ran(f) ⊆ E_d for d = max{n},   
   hence every set-image is finite; no single set contains all tagged tuples.   
   “Continuous domain” is only a proper class; no set [0,1]_t exists inside   
   any model of ZF, so no bijection ℕ → [0,1]_t is even expressible, and   
   CSB never applies.   
   “Non-Cartesian” is only ink; the graph is an ordinary ZF set with finite   
   range, and Cantor’s theorem still forbids any set bijection ℕ→𝒫ℕ.   
      
   One-line lemma you can prove inside ZF   
   Lemma (ZF)   
   ⊢ ∃f (f is a set ∧ dom(f)=ℕ ∧ f is non-decreasing ∧ ∀n   
   (f(n)=⟨n,d,6⟩   
   with d least ≥n) ∧ ran(f) is finite).   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)