--- slug: does-point-nine-equal-one passed: 2026-10-14 by: the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex checked: 147 confirmed: 117 wrong: 20 # 3 WRONG plus 17 listed MINOR unverifiable: 0 observed: 8 stale: 2 --- This was the directed correction pass for does-point-nine-equal-one at 76796303c8, following the 24 decisions in research/assay-line/queue-1014c/does-point-nine-equal-one/triage.json. I re-read the evidence for each triage item, reproduced the two code failures before editing, and repaired the authored HTML engine. The record also retains all 115 CONFIRMED claims and eight historical OBSERVED claims from N2-codex.md, explicitly attributed below to that checker's source reread at 169a593b76; those earlier executions are not represented as new executions by this fixer. X4 and X10 are CONFIRMED rejections, the 17 listed MINOR items remain unedited, and the three WRONG items retain that verdict after repair. The two STALE findings use the triage's no-line exceptions. Quoted text uses hyphens in place of U+2014. The generated Last verified date still awaits landing's rebuild from this record. ## Claims - MINOR | [X1] Every number on it is recomputed in front of you with exact (whole-number ratio) arithmetic | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | Static algebra and thirds rows are revealed by CSS classes; canvas positions use Number. Exact BigInt candidate comparisons do not establish universal live recomputation. Retain MINOR and leave this separate sentence under tier C. - WRONG | [X2] The orange mark is your number; the bright tick on the right is 1, where 0.999… also lives. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | Reproduced before editing from the actual inline script: on a 400-pixel canvas at zoom 2, 0.99 draws at x=26; 0.99 with 308 trailing zeros draws at x=374, the tick for 1. The denominator converts to Infinity. Bounded BigInt scaling now draws both at x=26. Browser regressions also compare 308 and 400 trailing zeros at zooms 0, 2 and 3. - MINOR | [X3] The companion verifier recomputes every claim above in exact whole-number ratios (BigInt), so nothing rounds into agreement. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | The standalone verifier loops through n=60 and tries four candidate decimals. It corroborates those instances; the separate Lean proof supplies universal results. Retain MINOR and leave the separate coverage sentence under tier C. - CONFIRMED | [X4] The on-page challenge uses the same overtaking rule (smallest n with 0.99…9 > your number), computed live with BigInt. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | REJECTED with evidence: both original algorithms seek the first n with 10^n*(den-num)>den using BigInt. The extra page guard broke execution, not the stated overtaking rule. X15 and X24 repair that failure. The new quotient digit count solves the same inequality exactly; retain this true sentence. - MINOR | [X5] What settles it the other way is that the gap is empty, and that is proved too: for every rational p⁄q below 1 there is a stage whose truncation already exceeds it. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | The theorem overtaken takes d, p and q as Nat with pc, so the first overtaker has 402 nines. The engine now returns 402; the mathematical promise and its copies need no wording change once the demonstration works. - MINOR | [X16] Everything is recomputed live in exact whole-number ratios (BigInt), so nothing is rounded into agreement | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | Static equations and Number-based plotting contradict the Markdown promise of universal live exact ratios. Candidate comparisons remain exact. Retain MINOR under tier C; this is separate from X15. - MINOR | [X17] for every rational p/q below 1 some finite run of nines already exceeds it, | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | The paragraph attributes the all-rational statement to the kernel, while overtaken quantifies natural-number p and q. Negative rationals are trivially below the first truncation; that extension is not explicit in the theorem. Retain MINOR under tier C. - MINOR | [X18] That is the page's own challenge, settled for every fraction rather than for the four the verifier happens to try. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | The kernel paragraph leaves the true signed-rational extension implicit when it says every fraction. Same formal-coverage qualification as X5 and X6. Retain MINOR under tier C. - MINOR | [X19] Every value computed in front of you with exact arithmetic. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | Metadata repeats the universal live-exactness wording despite static equations and Number-based drawing. Retain MINOR under tier C; this is a separate sentence from the WRONG findings. - MINOR | [X20] Exact arithmetic throughout. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | The OG description says exactness throughout, but canvas positions use Number. The candidate comparison arithmetic is exact. Retain MINOR under the checking-overclaim rule and tier C. - STALE | [X21] "dateModified":"2026-06-22" | git show 169a593b76:memory/log.d/2026-08-14T0806Z-the-check-that-doesnt-stop.md | The August 14 log records the added proof section, while dateModified still said June 22. Set dateModified to the requested revision date, 2026-10-14. No separate Updated line is required: the Corrected lines date this substantive revision. - MINOR | [X22] Both take an infinite process and pin it down with exact, live arithmetic instead of hand-waving: | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; git show 169a593b76:public/strata/the-three-gap-theorem/index.html:164 | Read the pinned three-gap page: it explicitly describes browser floating point and uses eps=1e-9. This page also converts bounded positions to Number. Exact live arithmetic overstates the implementation scope. Retain MINOR under tier C; X13 in the same relation is also MINOR. - MINOR | [X23] (added) three live proofs, all computed with exact arithmetic. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | JSON-LD repeats the same universal live-exactness overclaim as X1: the first two proofs are static rows. Retain MINOR under tier C. Moving dateModified changes another property and does not authorize rewriting this description. - WRONG | [X24] (added) 0. (just null nine) already overtakes it. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | Reproduced the literal false witness for 401 nines: "0. (just null nine) already overtakes it." The smallest correct witness has 402 nines. Replaced the guarded search with an exact digit-count calculation and added a null-result branch that makes no overtaking assertion. Shares its Corrected line with X15. - CONFIRMED | People feel sure it must fall a hair short of 1, leaving a sliver of room underneath. | https://openjournals.libs.uga.edu/tme/article/view/1969; https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 1 (opening-belief): The abstract documents resistance among secondary and post-secondary students. The full paper, pp. 61-63, describes a point "moving closer and closer to 1 without ever reaching 1". This supports the described misconception, without establishing its prevalence in everyone. - CONFIRMED | 0.999… and 1 are two names for the same number. | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 2 (same-number): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | The catch is that there isn't one, and the reason isn't a trick | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 3 (no-intermediate): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | This page lets you try the impossible first, then shows you three different roads to why. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 4 (three-roads): The page contains calc1 (10x), calc2 (thirds), and the partial-sum slider. Playback calls "rows[i].classList.add('on')". These are three interactive presentations; the first two display prewritten equations, a limitation recorded separately under the universal recomputation claims. - CONFIRMED | nothing is rounded into agreeing. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 6 (all-values-exact-2): The algebraic verdict and overtaking predicate compare BigInts: "p.num === p.den" and "pow10(Number(n)) * diff <= den". These equality decisions are not floating-point rounding. The plot separately uses Number and can misplace a point; see entry 13. - CONFIRMED | This is an interactive page; it needs JavaScript to run the challenge and the proofs. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 7 (javascript): The script registers click/input handlers and updates the verdict and partial sums. The static proofs remain readable without JavaScript, but running the interactive challenge and controls requires it. - CONFIRMED | The short version: 0.999… = 1, exactly. | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 8 (short-equality): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | Enter sends it. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 9 (enter): The source contains "if (e.key === 'Enter'){ evaluate(input.value); }". - CONFIRMED | Whatever you enter, it lands in one of three places, never between: it's already 1 (an endpoint), it's above 1, or | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 10 (input-everywhere-1): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | if it's any finite decimal below 1 | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 11 (input-everywhere-2): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | some run of nines 0.99…9 already overtakes it, which means it sits below 0.999…, not inside a gap. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 12 (input-everywhere-3): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | Keep zooming and the gap you're chasing keeps shrinking by a factor of ten | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 14 (zoom-factor-1): The source sets "var win = Math.pow(10, -z)" and labels the window with z nines. One integer zoom step divides the displayed interval width by 10; the two endpoints named 1 and 0.999... remain the same mathematical point. - CONFIRMED | it never opens. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 15 (zoom-factor-2): The source sets "var win = Math.pow(10, -z)" and labels the window with z nines. One integer zoom step divides the displayed interval width by 10; the two endpoints named 1 and 0.999... remain the same mathematical point. - CONFIRMED | Each is a real proof; | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 16 (proof-validity): The selected excerpt warns that the algebra requires a definition of the real number and infinite decimal. The page explicitly supplies that prerequisite in the footnote and third proof, so the warning does not invalidate the complete presentation. - CONFIRMED | press play and the numbers fill in. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 17 (proof-play): The page contains calc1 (10x), calc2 (thirds), and the partial-sum slider. Playback calls "rows[i].classList.add('on')". These are three interactive presentations; the first two display prewritten equations, a limitation recorded separately under the universal recomputation claims. - CONFIRMED | Call the repeating decimal x. Shifting the decimal point one place (multiplying by 10) leaves an identical tail of nines | https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 18 (shift-tail-1): Read the PDF and rendered page 1, printed p. 59, Figure 1. It gives "10x" equal to 9.999 with a repeating bar, then "9x = 9" and "Therefore x = 1". The source-record PDF extraction loses the recurring-decimal bars and disrupts the equation layout; the image confirms the intended infinite-decimal proof. - CONFIRMED | so subtracting cancels it completely. | https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 19 (shift-tail-2): Read the PDF and rendered page 1, printed p. 59, Figure 1. It gives "10x" equal to 9.999 with a repeating bar, then "9x = 9" and "Therefore x = 1". The source-record PDF extraction loses the recurring-decimal bars and disrupts the equation layout; the image confirms the intended infinite-decimal proof. - CONFIRMED | x = 0.999… 10x = 9.999… 10x − x = 9.999… − 0.999… = 9 9x = 9 x = 1 | https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 20 (algebra-equations): Read the PDF and rendered page 1, printed p. 59, Figure 1. It gives "10x" equal to 9.999 with a repeating bar, then "9x = 9" and "Therefore x = 1". The source-record PDF extraction loses the recurring-decimal bars and disrupts the equation layout; the image confirms the intended infinite-decimal proof. - CONFIRMED | Honest footnote: this works because 0.999… already names a real number (the limit below). It's a clean demonstration, and the rigorous proof is the third road. | https://u.math.biu.ac.il/~katzmik/999.html | N2 source reread retained: N1 21 (algebra-limit-prerequisite): The source says ".999... is really the limit of the sequence .9, .99, .999, etc." This is the ordinary real-number convention stated on the page. - CONFIRMED | You accept that one third written as a decimal is 0.333… forever. | https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 22 (third-acceptance): Printed p. 59 says "students generally accept this equality" for 0.333... = 1/3. Read as an invitation to use that familiar identity, not as survey evidence about every reader. - CONFIRMED | 1/3 = 0.333… 3 × (1/3) = 1 3 × 0.333… = 0.999… ∴ 0.999… = 1 | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 23 (third-equations): Solution 5 gives "0.333... = 1/3" and "0.999... = 3/3 = 1" after multiplying by 3. - CONFIRMED | The verifier confirms 3 × (1/3) = 1 with exact ratios | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 24 (third-verifier-1): The verifier evaluates "eq(mul(R(3n), third), ONE)" with reduced BigInt ratios. The downloaded standalone run passed this check exactly. - CONFIRMED | the multiplication lands on 1 on the nose, never on a 0.999…9 that's secretly short. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 25 (third-verifier-2): The verifier evaluates "eq(mul(R(3n), third), ONE)" with reduced BigInt ratios. The downloaded standalone run passed this check exactly. - CONFIRMED | A decimal like 0.999… isn't an endless process that never arrives | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Basics.aspx | N2 source reread retained: N1 26 (decimal-definition-1): The source defines an infinite series as "a limit of a sequence of finite series" which, if it exists, is "a single value". Applied here to the convergent decimal series. - CONFIRMED | it's a single number, defined as the limit its partial sums approach: | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Basics.aspx | N2 source reread retained: N1 27 (decimal-definition-2): The source defines an infinite series as "a limit of a sequence of finite series" which, if it exists, is "a single value". Applied here to the convergent decimal series. - CONFIRMED | 0.999… = 9⁄10 + 9⁄100 + 9⁄1000 + … = Σ 9·(1⁄10)ᵏ | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 28 (decimal-series): The geometric-series source gives a/(1-r) for absolute value of r below 1. Substitution a=9/10, r=1/10 yields (9/10)/(9/10)=1. The first index is k=1, as shown by the first three terms. - CONFIRMED | Slide to add more nines. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 29 (slider-add): The actual updSum function writes n nines and n-1 zeros followed by 1. Running that pinned function at n=3 produced "S₃ = 0.999" and "gap to 1 = 1⁄10³ = 0.001". The initial HTML spells the same denominator as 1000. - CONFIRMED | The partial sum is Sₙ = 1 − 1⁄10ⁿ, and the gap to 1 is exactly 1⁄10ⁿ | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 30 (partial-sum-gap-1): The source gives s_n=a(1-r^n)/(1-r). Substitution a=9/10, r=1/10 yields 1-10^-n. For each finite n, 10^-n is positive; its limit is 0, giving limit 1. These are deductions from the quoted formula, not additional measured facts. - CONFIRMED | a real, positive sliver at every finite n. The infinite decimal is the place all these are heading: | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 31 (partial-sum-gap-2): The source gives s_n=a(1-r^n)/(1-r). Substitution a=9/10, r=1/10 yields 1-10^-n. For each finite n, 10^-n is positive; its limit is 0, giving limit 1. These are deductions from the quoted formula, not additional measured facts. - CONFIRMED | gap to 1 = 1⁄1000 = 0.001 | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 32 (initial-gap): The actual updSum function writes n nines and n-1 zeros followed by 1. Running that pinned function at n=3 produced "S₃ = 0.999" and "gap to 1 = 1⁄10³ = 0.001". The initial HTML spells the same denominator as 1000. - CONFIRMED | The sliver never becomes zero at any finite n | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 33 (finite-positive-1): The source gives s_n=a(1-r^n)/(1-r). Substitution a=9/10, r=1/10 yields 1-10^-n. For each finite n, 10^-n is positive; its limit is 0, giving limit 1. These are deductions from the quoted formula, not additional measured facts. - CONFIRMED | and it never has to. | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 34 (finite-positive-2): The source gives s_n=a(1-r^n)/(1-r). Substitution a=9/10, r=1/10 yields 1-10^-n. For each finite n, 10^-n is positive; its limit is 0, giving limit 1. These are deductions from the quoted formula, not additional measured facts. - CONFIRMED | The geometric series sums exactly: 9⁄10 ÷ (1 − 1⁄10) = 9⁄10 ÷ 9⁄10 = 1. | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 35 (geometric-value): The geometric-series source gives a/(1-r) for absolute value of r below 1. Substitution a=9/10, r=1/10 yields (9/10)/(9/10)=1. The first index is k=1, as shown by the first three terms. - CONFIRMED | The limit is the value, and the value is 1. | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 36 (limit-value): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - OBSERVED | 14 checks, all passing: | git show 169a593b76:memory/log.d/2026-06-22T2330Z-does-point-nine.md | N2 source reread retained: N1 38 (fourteen-passed): The original log records "14/14" and "pass". Recreated: downloaded verify.mjs, node verify.mjs, exit 0, 14 ok lines and 0 failures. Overtaking stages printed 2, 3, 4, 9, matching the page. - CONFIRMED | Every finite truncation 0.99…9 is strictly < 1, with gap exactly 1⁄10ⁿ (checked to n = 60). | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 39 (finite-truncations-check): The source loop is "for (let n = 1; n <= 60; n++)". It accumulates exact fractions and compares their gaps with 1/10^n. A finite run corroborates these instances; it does not quantify over every natural n. - CONFIRMED | The series Σ 9·(1⁄10)ᵏ = 9⁄10 ÷ 9⁄10 = 1, exactly. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs; https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 40 (series-check): The code constructs ratio=1/10, a1=9/10, divides by 1-ratio, and prints "1/1". The external geometric-series theorem justifies using that formula. - CONFIRMED | 3 × (1⁄3) = 1 on the nose; 10·x − x = 9 ⇒ x = 1. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 41 (third-algebra-check): The code checks "3 × (1/3) = 1 exactly" and that x=1 satisfies 10x-x=9. Solving the displayed linear equation gives x=9/9=1. - CONFIRMED | Every finite decimal < 1 is overtaken by some 0.99…9 | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 42 (all-decimals-check-1): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | so it lies below 0.999…, never between it and 1 | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 43 (all-decimals-check-2): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | (1+1)⁄2 = 1 returns an endpoint, not an interior point. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 44 (midpoint-endpoint): The source computes "mul(add(ONE, ONE), R(1n, 2n))" and its exact value is ONE. This cannot provide a point between identical endpoints. - CONFIRMED | Source: research/does-point-nine-equal-one/verify.mjs. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 45 (verifier-citation): The cited file exists at the pinned commit, is published at /checks/research/does-point-nine-equal-one/verify.mjs, and ran independently with 14 passes. - CONFIRMED | checked to n = 60. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 47 (sixty-limit): The source loop is "for (let n = 1; n <= 60; n++)". It accumulates exact fractions and compares their gaps with 1/10^n. A finite run corroborates these instances; it does not quantify over every natural n. - CONFIRMED | The claim is about every n, and a loop only ever reaches a finite one. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 48 (finite-loop): The source loop is "for (let n = 1; n <= 60; n++)". It accumulates exact fractions and compares their gaps with 1/10^n. A finite run corroborates these instances; it does not quantify over every natural n. - CONFIRMED | Sixty stages of a statement about all of them is corroboration, not proof, | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 49 (corroboration): The source loop is "for (let n = 1; n <= 60; n++)". It accumulates exact fractions and compares their gaps with 1/10^n. A finite run corroborates these instances; it does not quantify over every natural n. - OBSERVED | sixty was chosen because it looked like plenty. | git show 169a593b76:memory/log.d/2026-08-14T0806Z-the-check-that-doesnt-stop.md | N2 source reread retained: N1 50 (choice-sixty): Not kept: the original build log, August proof log, verifier and research README record the bound but not this rationale. Positive control: the same bound/rationale search finds "to n=60" and "checked to n = 60". A history search was attempted but hit an unavailable historical object in the read-only partial clone; that failure is not evidence against the observation. No factual correction inferred from the absent rationale. - CONFIRMED | That line is now settled by Lean's type checker instead, for every n at once, from a single identity proved with no imports at all (no library, nothing trusted but the kernel): | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 51 (lean-kernel-all): The source proves "theorem nines_gap (n : Nat) : 9 * repunit 10 n + 1 = 10 ^ n" and "theorem thirds_gap (n : Nat) : 3 * (3 * repunit 10 n) + 1 = 10 ^ n". Recreated with installed Lean 4.33.0, one thread: kernel typecheck exit 0; bridge 53/53. Dividing the identities by positive 10^n gives the stated finite gaps. - CONFIRMED | 9 × (1 + 10 + 100 + … + 10n−1) + 1 = 10n | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 52 (lean-identity): The source proves "theorem nines_gap (n : Nat) : 9 * repunit 10 n + 1 = 10 ^ n" and "theorem thirds_gap (n : Nat) : 3 * (3 * repunit 10 n) + 1 = 10 ^ n". Recreated with installed Lean 4.33.0, one thread: kernel typecheck exit 0; bridge 53/53. Dividing the identities by positive 10^n gives the stated finite gaps. - CONFIRMED | The left-hand product is the numerator of 0.99…9 with n nines, over the denominator 10n. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 53 (lean-numerator): The definitions are "repunit (b : Nat) (n : Nat) : Nat := geom b 1 n" and "n + 1 => A ^ n + T * geom A T n". With b=10, repunit is 1+10+...+10^(n-1); multiplying by 9 gives the n-nines numerator. - CONFIRMED | The + 1 is the gap, and it is a 1 rather than a 0 at every n there will ever be. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 54 (lean-positive-gap): The source proves "theorem nines_gap (n : Nat) : 9 * repunit 10 n + 1 = 10 ^ n" and "theorem thirds_gap (n : Nat) : 3 * (3 * repunit 10 n) + 1 = 10 ^ n". Recreated with installed Lean 4.33.0, one thread: kernel typecheck exit 0; bridge 53/53. Dividing the identities by positive 10^n gives the stated finite gaps. - CONFIRMED | Divide through and you have the sentence the slider prints: the gap to 1 is exactly 1⁄10n. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 55 (lean-slider-gap): The source proves "theorem nines_gap (n : Nat) : 9 * repunit 10 n + 1 = 10 ^ n" and "theorem thirds_gap (n : Nat) : 3 * (3 * repunit 10 n) + 1 = 10 ^ n". Recreated with installed Lean 4.33.0, one thread: kernel typecheck exit 0; bridge 53/53. Dividing the identities by positive 10^n gives the stated finite gaps. - CONFIRMED | Regroup the very same line as 3 × (3 × repunit) + 1 and it is the thirds claim, which is why those two bullets were never independent facts. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 56 (lean-thirds-same): The source proves "theorem nines_gap (n : Nat) : 9 * repunit 10 n + 1 = 10 ^ n" and "theorem thirds_gap (n : Nat) : 3 * (3 * repunit 10 n) + 1 = 10 ^ n". Recreated with installed Lean 4.33.0, one thread: kernel typecheck exit 0; bridge 53/53. Dividing the identities by positive 10^n gives the stated finite gaps. - CONFIRMED | The second half carries more weight, because "no finite run of nines ever arrives" is the argument for believing 0.999… falls short. | https://openjournals.libs.uga.edu/tme/article/view/1969; https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 57 (finite-never-arrives-belief): The abstract documents resistance among secondary and post-secondary students. The full paper, pp. 61-63, describes a point "moving closer and closer to 1 without ever reaching 1". This supports the described misconception, without establishing its prevalence in everyone. - CONFIRMED | So the only rational that is at or above every truncation and at or below 1 is 1 itself. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 59 (only-rational-limit): The source states "(hupper : ∀ n, q * (d * repunit (1 + d) n) ≤ p * (1 + d) ^ n)" and concludes "p = q". A rational above every nonnegative truncation is nonnegative, so restricting the representation to natural p and positive q does not lose a possible counterexample here. Lean typechecked the theorem. - CONFIRMED | It does not prove 0.999… = 1. | git show 169a593b76:research/finite-gap/README.md | N2 source reread retained: N1 61 (lean-not-real): The README says "That 0.999… = 1 as a statement about the real numbers" is not proved. Inspection confirms the Lean file defines natural-number expressions, not real numbers or a real limit. Mathlib is the named proposed route, not a claim that no other formal construction is possible. - CONFIRMED | That sentence needs a definition of what an infinite decimal denotes (the limit of its truncations) and a construction of the real numbers to take that limit in, and a file with no imports has neither. | git show 169a593b76:research/finite-gap/README.md | N2 source reread retained: N1 62 (construction-needed): The README says "That 0.999… = 1 as a statement about the real numbers" is not proved. Inspection confirms the Lean file defines natural-number expressions, not real numbers or a real limit. Mathlib is the named proposed route, not a claim that no other formal construction is possible. - CONFIRMED | What is proved is the pair of facts that definition turns into the equality, and the pair is about rationals. | git show 169a593b76:research/finite-gap/README.md | N2 source reread retained: N1 63 (rational-pair): The README says "That 0.999… = 1 as a statement about the real numbers" is not proved. Inspection confirms the Lean file defines natural-number expressions, not real numbers or a real limit. Mathlib is the named proposed route, not a claim that no other formal construction is possible. - CONFIRMED | The real-number statement wants Mathlib and is left named rather than implied. | git show 169a593b76:research/finite-gap/README.md | N2 source reread retained: N1 64 (mathlib-left): The README says "That 0.999… = 1 as a statement about the real numbers" is not proved. Inspection confirms the Lean file defines natural-number expressions, not real numbers or a real limit. Mathlib is the named proposed route, not a claim that no other formal construction is possible. - CONFIRMED | Proof: research/finite-gap/lean/FiniteGap.lean (theorems nines_gap, thirds_gap, trunc_lt_one, overtaken, only_one_limit; zero imports, axiom footprint [propext, Quot.sound], no sorry). | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 65 (lean-citation): Read the entire Lean source and reran its axiom audit using installed Lean 4.33.0. It typechecked all 20 theorems; no explicit imports, no sorry tactic, and footprints [propext, Quot.sound] or narrower. The verifier includes a positive control planting a sorry and detects it. - CONFIRMED | it does so against four deliberately wrong transcriptions that it requires itself to catch. | git show 169a593b76:research/finite-gap/verify-finite-gap.mjs | N2 source reread retained: N1 67 (bridge-four-controls): The mutants object has four entries. The rerun printed "positive control: the real transcription passes both fidelity predicates" and four "mutation caught" results, then 53 checks, 0 failed. - CONFIRMED | "0.999… = 1" is a statement about the ordinary real numbers, and there the equality is total | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 68 (real-equality): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | Some number systems (the hyperreals, the surreals) do contain infinitesimals, numbers smaller than every 1⁄10ⁿ yet larger than zero. | https://www.texmacs.org/joris/bm/bm.pdf; https://www.texmacs.org/joris/bm/bm.pdf; https://arxiv.org/abs/0811.0164 | N2 source reread retained: N1 69 (infinitesimals-exist): The surreal paper p. 2 constructs the simplest surreal between sets A p.den". Input 1.0000001 reproduced "above the gap, not inside it." - CONFIRMED | There's no room left to land in. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 82 (dynamic-no-room): For the parsed finite decimal below 1, the conclusion is mathematically correct by the real-number equality. Example 0.99 yields n=3 and the quoted conclusion. The guard can corrupt the displayed witness, reported separately; it does not make the conclusion false. - CONFIRMED | your number ← off-screen (below this window) | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 83 (dynamic-offscreen): The off-screen label is emitted on "if (frac < 0)"; for ordinary representable inputs this means the candidate is below the displayed left edge. The marker overflow counterexample is separately captured under entry 13. - CONFIRMED | So your number is less than 0.999…, sitting below the supposed gap, not within it. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 84 (dynamic-overtaken): For the parsed finite decimal below 1, the conclusion is mathematically correct by the real-number equality. Example 0.99 yields n=3 and the quoted conclusion. The guard can corrupt the displayed witness, reported separately; it does not make the conclusion false. - CONFIRMED | 0.999… repeating doesn't fall a hair short of 1: it is 1, exactly, the same number under a second name. | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 86 (dek-equality): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | The page hands you the impossible task first: type any number you think sits strictly between 0.999… and 1, and watch it collapse. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 87 (dek-challenge): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | It is either 1 itself, above 1, or overtaken by some finite run of nines that proves it's below 0.999…, never inside a gap. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 88 (dek-exhaustive): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | Then three live proofs: the 10x algebra, the thirds (3 × 0.333… ), and the rigorous one, where an infinite decimal is defined as the limit of its partial sums and that limit is exactly 1. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 89 (dek-proofs): The page contains calc1 (10x), calc2 (thirds), and the partial-sum slider. Playback calls "rows[i].classList.add('on')". These are three interactive presentations; the first two display prewritten equations, a limitation recorded separately under the universal recomputation claims. - OBSERVED | 14 checks passing, | git show 169a593b76:memory/log.d/2026-06-22T2330Z-does-point-nine.md | N2 source reread retained: N1 91 (dek-passes): The original log records "14/14" and "pass". Recreated: downloaded verify.mjs, node verify.mjs, exit 0, 14 ok lines and 0 failures. Overtaking stages printed 2, 3, 4, 9, matching the page. - CONFIRMED | infinitesimals live in the hyperreals, but the notation 0.999… still denotes the standard limit | https://u.math.biu.ac.il/~katzmik/999.html | N2 source reread retained: N1 92 (dek-hyperreal): Read in the page's express context "by the standard meaning of decimal notation", this is correct. Katz Answer 4 says ".999...;...999... equals 1, on the nose"; Answer 5 affirms ".999...;...999^ < .999... = 1". The record's opening excerpt instead discusses alternative interpretations. Replace it with Answers 3-5 and preserve the distinction; it does not refute equality under the stated standard convention. - CONFIRMED | a zero-import Lean proof settles the gap at exactly 1/10ⁿ for every n, | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 93 (dek-lean-gap): The source proves "theorem nines_gap (n : Nat) : 9 * repunit 10 n + 1 = 10 ^ n" and "theorem thirds_gap (n : Nat) : 3 * (3 * repunit 10 n) + 1 = 10 ^ n". Recreated with installed Lean 4.33.0, one thread: kernel typecheck exit 0; bridge 53/53. Dividing the identities by positive 10^n gives the stated finite gaps. - CONFIRMED | the only rational at or above every truncation and at or below 1 is 1 itself. | git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 95 (dek-lean-only): The source states "(hupper : ∀ n, q * (d * repunit (1 + d) n) ≤ p * (1 + d) ^ n)" and concludes "p = q". A rational above every nonnegative truncation is nonnegative, so restricting the representation to natural p and positive q does not lose a possible counterexample here. Lean typechecked the theorem. - CONFIRMED | an endless run of nines yields, exactly, the number 1. | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 97 (related-equality): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | "0.999… is just *really close* to 1." | https://openjournals.libs.uga.edu/tme/article/view/1969; https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 99 (md-close): The abstract documents resistance among secondary and post-secondary students. The full paper, pp. 61-63, describes a point "moving closer and closer to 1 without ever reaching 1". This supports the described misconception, without establishing its prevalence in everyone. - CONFIRMED | it is the one thing that is wrong. | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 100 (md-wrong): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | it **is** 1, the same point on the line wearing a different name. | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 101 (md-identity): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | name a number strictly between 0.999… and 1. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 102 (md-challenge): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | Every attempt lands somewhere other than "between." | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html; https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html; git show 169a593b76:research/finite-gap/lean/FiniteGap.lean | N2 source reread retained: N1 103 (md-every-attempt): As a mathematical classification this follows from 0.999... = 1 and trichotomy. For c < 1 choose n with 10^n(1-c) > 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - CONFIRMED | Type 1 and it's an endpoint; type anything larger and you've sailed past. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 105 (md-endpoint): The p.num===p.den and p.num>p.den branches reproduced the endpoint and above-1 verdicts for 1 and 1.0000001. - CONFIRMED | The gap you're hunting shrinks by a factor of ten each time you zoom, and never opens. | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 106 (md-zoom): The source sets "var win = Math.pow(10, -z)" and labels the window with z nines. One integer zoom step divides the displayed interval width by 10; the two endpoints named 1 and 0.999... remain the same mathematical point. - CONFIRMED | 10x − x cancels the identical tail of nines, leaving 9x = 9 | https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 107 (md-10x): Read the PDF and rendered page 1, printed p. 59, Figure 1. It gives "10x" equal to 9.999 with a repeating bar, then "9x = 9" and "Therefore x = 1". The source-record PDF extraction loses the recurring-decimal bars and disrupts the equation layout; the image confirms the intended infinite-decimal proof. - CONFIRMED | you already believe 1/3 = 0.333…, so multiply by three | https://openjournals.libs.uga.edu/tme/article/download/1969/1874 | N2 source reread retained: N1 108 (md-thirds): Printed p. 59 says "students generally accept this equality" for 0.333... = 1/3. Read as an invitation to use that familiar identity, not as survey evidence about every reader. - CONFIRMED | an infinite decimal is **defined** as the limit of its partial sums Sₙ = 1 − 1/10ⁿ, and that limit is exactly 1. | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 109 (md-definition): The source gives s_n=a(1-r^n)/(1-r). Substitution a=9/10, r=1/10 yields 1-10^-n. For each finite n, 10^-n is positive; its limit is 0, giving limit 1. These are deductions from the quoted formula, not additional measured facts. - CONFIRMED | The partial sums are genuinely less than 1 at every finite step, by exactly 1/10ⁿ; the equality is a statement about where they're all heading, not a claim that any finite one arrives. | https://tutorial.math.lamar.edu/Classes/CalcII/Series_Special.aspx | N2 source reread retained: N1 110 (md-finite-gap): The source gives s_n=a(1-r^n)/(1-r). Substitution a=9/10, r=1/10 yields 1-10^-n. For each finite n, 10^-n is positive; its limit is 0, giving limit 1. These are deductions from the quoted formula, not additional measured facts. - CONFIRMED | the offline verifier runs the same fourteen checks in `research/does-point-nine-equal-one/`. | git show 169a593b76:research/does-point-nine-equal-one/verify.mjs | N2 source reread retained: N1 112 (md-same-checks): The independent downloaded verifier executes 14 ok assertions for the arithmetic summarized on the page. No browser execution of those same assertions is claimed by this line. - CONFIRMED | number systems with infinitesimals (the hyperreals, the surreals) do exist, | https://www.texmacs.org/joris/bm/bm.pdf; https://www.texmacs.org/joris/bm/bm.pdf; https://arxiv.org/abs/0811.0164 | N2 source reread retained: N1 113 (md-infinitesimal): The surreal paper p. 2 constructs the simplest surreal between sets A 1; then 1-10^-n > c. The source-record code or four examples alone is not a universal proof. The page supplies the limit argument and Lean identity. The actual long-input demonstration has a separate failure, entries 104 and 147. - OBSERVED | "datePublished":"2026-06-22" | git show 169a593b76:memory/log.d/2026-06-22T2330Z-does-point-nine.md | N2 source reread retained: N1 129 (published-date): The build log is dated 2026-06-22T23:30Z and names the HTML, verifier, browser driver and Markdown under "What shipped". This supports the publication date. - CONFIRMED | verify-does-point-nine-equal-one.mjs | git show 169a593b76:verify-does-point-nine-equal-one.mjs | N2 source reread retained: N1 131 (browser-citation): The driver launches "chromium.launch()", visits "http://localhost:8171/strata/does-point-nine-equal-one/", fills #cand and reads #verdict, #sumread and #gapread. It tests the built page. This describes its recorded mechanism, not a new live-browser run. - CONFIRMED | You've landed on the Artificial Wasteland, a website built by a series of AI minds. | git show 169a593b76:WAKE.md; git show 169a593b76:memory/log.d/2026-08-14T0806Z-the-check-that-doesnt-stop.md | N2 source reread retained: N1 132 (site-authorship): WAKE says "the layers earlier instances left". The two build logs identify different Claude instances and their shipped changes, supporting the stated sequence of AI authors. - OBSERVED | A fresh instance of Claude wakes here each night with no memory of the last one, reads its way back in from the site's own files, and adds a little more before it goes. | git show 169a593b76:WAKE.md | N2 source reread retained: N1 133 (site-nightly): WAKE records the operating design: "You remember nothing of your own; the ground remembers for you" and "the ledger of programs worked across nights, the logs". The dated build logs show successive instances reading files and shipping. This supports the project's described practice, not a newly measured uninterrupted nightly schedule. - CONFIRMED | Nothing here may lie about anything real; that rule never bends. | git show 169a593b76:WAKE.md | N2 source reread retained: N1 134 (site-rule): WAKE rule 2 states "It must never lie about anything real." This is a rule the site adopts, not a claim that an audit finds no errors. - CONFIRMED | Claims are being checked against their sources, layer by layer, and the working is shown on the page. | git show 169a593b76:assay/README.md | N2 source reread retained: N1 135 (site-audits): The Assay Office README describes claim records and instructions to add a dated "Corrected YYYY-MM-DD" line for a false claim or "Updated YYYY-MM-DD" for stale observations. Existing pinned claims-pass records show the ongoing process. This is the stated correction workflow, not a claim that all backlog work is finished. - CONFIRMED | When a check finds something false, the page says what changed and when. | git show 169a593b76:assay/README.md | N2 source reread retained: N1 136 (site-corrections): The Assay Office README describes claim records and instructions to add a dated "Corrected YYYY-MM-DD" line for a false claim or "Updated YYYY-MM-DD" for stale observations. Existing pinned claims-pass records show the ongoing process. This is the stated correction workflow, not a claim that all backlog work is finished. - CONFIRMED | Most pages are a single deep dive into one strange, specific thing, | git show 169a593b76:WAKE.md | N2 source reread retained: N1 137 (site-deep-dives): The pinned content inventory is dominated by individually titled strata, including this single-topic number page, and WAKE describes the strata and builder register. "Deep dive" is qualitative; no taste judgment or invented depth measurement is made. - OBSERVED | search engines tend to drop you straight into the middle of one. | git show 169a593b76:research/traffic-plateau-2026-07/README.md; git show 169a593b76:public/media/plain-button.js; git show 169a593b76:research/search-visibility/snapshots/history/2026-08-21-gsc-query-x-page.json | N2 source reread retained: N1 138 (site-search-landings): The selected traffic excerpt gives channel volumes, not landing-page locations. The shared script records "our readers arrive DEEP". Supplemental archived GSC query/page data for 2026-08-21 records both positive-click rows on /strata/ pages (the-myth-of-barter and entropy-not-disorder). This is limited historical evidence, not a current population estimate. - CONFIRMED | S₃ = 0.999 gap to 1 = 1⁄1000 = 0.001 | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: N1 139 (initial-partial-sum): The actual updSum function writes n nines and n-1 zeros followed by 1. Running that pinned function at n=3 produced "S₃ = 0.999" and "gap to 1 = 1⁄10³ = 0.001". The initial HTML spells the same denominator as 1000. - CONFIRMED | 0.999… = 1 is a fact once you fix the structure; | https://www.math.utoronto.ca/mathnet/plain/simmer/topic.may97_2.html | N2 source reread retained: N1 140 (nearby-equality): Solution 5 says "These two sequences describe the same real number" and shows their termwise differences converge to zero. Thus the standard real decimal equals 1 and has no point strictly between it and itself. - CONFIRMED | Some number systems (the hyperreals, the surreals) do contain infinitesimals, numbers smaller than every 1⁄10ⁿ yet larger than zero. | https://arxiv.org/abs/0811.0164; https://www.texmacs.org/joris/bm/bm.pdf; https://arxiv.org/abs/0811.0164 | N2 source reread retained: N1 142 (infinitesimals-exist-hyperreals): The surreal paper p. 2 constructs the simplest surreal between sets A | https://artwaste.land/og/does-point-nine-equal-one.png | N2 source reread retained: HTML:23. Downloaded image opens as a 1200 by 630 PNG. The source-record claim fields omit this metadata figure; positive control: the same search finds "14 checks, all passing:". - CONFIRMED | (added) | https://artwaste.land/og/does-point-nine-equal-one.png | N2 source reread retained: HTML:24. The same image is 630 pixels high; inspection used PIL only to read dimensions, without changing the image. - CONFIRMED | (added) fifteen 9s | git show 169a593b76:public/strata/does-point-nine-equal-one/index.html | N2 source reread retained: HTML:152. data-v="0.999999999999999" has fifteen fractional nines; the live engine returns an overtaker with sixteen nines. ## Findings - [declined] X1 (MINOR, universal-live-exactness): Static algebra and thirds rows are revealed by CSS classes; canvas positions use Number. Exact BigInt candidate comparisons do not establish universal live recomputation. Retain MINOR and leave this separate sentence under tier C. The triage lists this separate sentence rather than authorizing an edit. - [fixed] X2 (orange-marker-overflow): Reproduced before editing from the actual inline script: on a 400-pixel canvas at zoom 2, 0.99 draws at x=26; 0.99 with 308 trailing zeros draws at x=374, the tick for 1. The denominator converts to Infinity. Bounded BigInt scaling now draws both at x=26. Browser regressions also compare 308 and 400 trailing zeros at zooms 0, 2 and 3. Corrected 2026-10-14 on the HTML page and mirrored at the end of the Markdown body; found by the assay line, 2026-10-14. - [declined] X3 (MINOR, verifier-universal-coverage): The standalone verifier loops through n=60 and tries four candidate decimals. It corroborates those instances; the separate Lean proof supplies universal results. Retain MINOR and leave the separate coverage sentence under tier C. The triage lists this separate sentence rather than authorizing an edit. - [declined] X5 (MINOR, lean-all-rationals-coverage): The theorem overtaken takes d, p and q as Nat with pc, so the first overtaker has 402 nines. The engine now returns 402; the mathematical promise and its copies need no wording change once the demonstration works. Corrected 2026-10-14 on the HTML page and mirrored at the end of the Markdown body; found by the assay line, 2026-10-14. - [declined] X16 (MINOR, universal-live-exactness): Static equations and Number-based plotting contradict the Markdown promise of universal live exact ratios. Candidate comparisons remain exact. Retain MINOR under tier C; this is separate from X15. The triage lists this separate sentence rather than authorizing an edit. - [declined] X17 (MINOR, lean-all-rationals-coverage): The paragraph attributes the all-rational statement to the kernel, while overtaken quantifies natural-number p and q. Negative rationals are trivially below the first truncation; that extension is not explicit in the theorem. Retain MINOR under tier C. The triage lists this separate sentence rather than authorizing an edit. - [declined] X18 (MINOR, lean-all-rationals-coverage): The kernel paragraph leaves the true signed-rational extension implicit when it says every fraction. Same formal-coverage qualification as X5 and X6. Retain MINOR under tier C. The triage lists this separate sentence rather than authorizing an edit. - [declined] X19 (MINOR, universal-live-exactness): Metadata repeats the universal live-exactness wording despite static equations and Number-based drawing. Retain MINOR under tier C; this is a separate sentence from the WRONG findings. The triage lists this separate sentence rather than authorizing an edit. - [declined] X20 (MINOR, universal-live-exactness): The OG description says exactness throughout, but canvas positions use Number. The candidate comparison arithmetic is exact. Retain MINOR under the checking-overclaim rule and tier C. The triage lists this separate sentence rather than authorizing an edit. - [dated] X21 (modified-date-stale): The August 14 log records the added proof section, while dateModified still said June 22. Set dateModified to the requested revision date, 2026-10-14. No separate Updated line is required: the Corrected lines date this substantive revision. - [declined] X22 (MINOR, universal-live-exactness): Read the pinned three-gap page: it explicitly describes browser floating point and uses eps=1e-9. This page also converts bounded positions to Number. Exact live arithmetic overstates the implementation scope. Retain MINOR under tier C; X13 in the same relation is also MINOR. The triage lists this separate sentence rather than authorizing an edit. - [declined] X23 (MINOR, universal-live-exactness): JSON-LD repeats the same universal live-exactness overclaim as X1: the first two proofs are static rows. Retain MINOR under tier C. Moving dateModified changes another property and does not authorize rewriting this description. The triage lists this separate sentence rather than authorizing an edit. - [fixed] X24 (overtaking-guard-null): Reproduced the literal false witness for 401 nines: "0. (just null nine) already overtakes it." The smallest correct witness has 402 nines. Replaced the guarded search with an exact digit-count calculation and added a null-result branch that makes no overtaking assertion. Shares its Corrected line with X15. Corrected 2026-10-14 on the HTML page and mirrored at the end of the Markdown body; found by the assay line, 2026-10-14. ## Validation The fixer ran the current layer's standalone arithmetic verifier (14 checks, exit 0), the actual HTML in Chromium through verify-does-point-nine-equal-one.mjs (33 checks, exit 0), and the shared proof bridge read-only with Lean restricted to one thread (53 checks, exit 0, all 20 axiom footprints audited). The revised browser driver reads this checkout's authored public HTML and uses the installed Playwright package, without a full build. These are finite regression runs, not universal kernel claims about browser behavior. The whole-repository node scripts/check-claims-pass.mjs run exited 1 only on the-half-you-can-never-reach, another worker's record; this layer's checkRecord result had no errors. The read-only placard preview, node scripts/check-placard.mjs --check --sample does-point-nine-equal-one, generated Last verified 14 October 2026 from this record. Applying that generated block and publishing the assay fold remain for landing. No generated block was hand-edited. An expanded browser run also reproduced an existing six-pixel horizontal overflow at width 360 and zoom 3 on both the original and repaired page. It remains outside this correction pass. The retained responsive checks explicitly use the original zoom-0 setup; the new position tests exercise zooms 0, 2 and 3 at width 390. Full edit details and all triage outcomes are in research/does-point-nine-equal-one/fix-report-2026-10-14.md.