# A continuous CDF with a flat interval [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-continuous-real-distribution-function/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-continuous-real-distribution-function-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Construct a complete knot-based CDF and audit atomlessness. An exact piecewise-linear family; continuity alone will not imply general density existence. ## Givens and symbols - work - G1 — The knots are(0,0),(1,1/2),(2,1/2),(3,1); interpolate linearly, with left tail 0 and right tail 1. - F — real CDF - t — arbitrary real threshold ## Rules and sources Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged. - mko_definition · cited — A continuous CDF has no jumps, so every singleton has probability 0. This is not continuity of a random-variable map on the sample space and does not imply a density or absolute continuity. An affine Cantor distribution supplies a continuous, atomless, singular boundary. Flat CDF intervals are allowed; strict increase is not required. · mko-continuous-real-distribution-function - work · prerequisite — Piecewise-linear functions are continuous on each piece; matching junctions ensure global continuity; CDF existence and the jump identity are prerequisites. ## Main derivation S01 · impliesBefore 0<1<2<3,\quad0\le1/2\le1/2\le1 After \text{strict knot order and nondecreasing levels} Conditions: none Rule: work · Uses: G1, work Leaf basis: work First audit strict knot order and legal nondecreasing CDF levels. S02 · impliesBefore t\le0\text{ or }t\ge3 After F(t)=0\ (t\le0),\quad F(t)=1\ (t\ge3) Conditions: none Rule: work · Uses: G1, S01, work Leaf basis: work Specify both tails to cover the exterior real-line regions. S03 · impliesBefore 0\le t\le1 After F(t)=t/2 Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work The first slope is(1/2-0)/(1-0)=1/2. S04 · impliesBefore 1\le t\le2 After F(t)=1/2 Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work Equal endpoint levels produce a valid flat middle interval. S05 · impliesBefore 2\le t\le3 After F(t)=1/2+(t-2)/2=(t-1)/2 Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work The last slope is also1/2 and reaches level1. S06 · impliesBefore t\in\{0,1,2,3\} After F(t^-)=F(t)=F(t^+) Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work All pieces and tails agree at four knots; their interiors are continuous. S07 · impliesBefore F\text{ nondecreasing and continuous, with tails }0,1 After \exists X:\ F(t)=P(X\le t);\quad P(X=t)=F(t)-F(t^-)=0\quad(t\in\mathbb R) Conditions: none Rule: work · Uses: G1, S06, work Leaf basis: work Nonnegative piece slopes, tails identically0 and 1, and proved continuity first invoke the explicitly assumed CDF-existence theorem to obtain a law X; then the jump identity gives zero singleton mass for every t. S08 · impliesBefore \lim_{t\to-\infty}F(t)=0,\quad\lim_{t\to\infty}F(t)=1 After F\text{ is a continuous CDF, not strictly increasing} Conditions: none Rule: work · Uses: G1, S07, work Leaf basis: work Monotonicity, continuity and tail limits qualify a continuous CDF, retaining its flat interval. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07, work — General continuous CDFs may be singular, as with a Cantor law; this example cannot imply densities generally. - S07 · premise_audit · G1, S06, work — Obtain the law before writing P(X=t); atomless does not mean zero interval mass, since P(0