# Audit: A K=19 binary tree of eml operations evaluates to x + y - **Generated:** 2026-04-16 - **Reader summary:** [proof.md](proof.md) - **Proof script:** [proof.py](proof.py) ## Claim Interpretation The claim defines eml(a, b) = exp(a) - ln(b) and asserts that a specific binary tree of 9 eml operations and 10 leaves (drawn from {1, x, y}) evaluates to x + y. The total token count K = 9 + 10 = 19. The user's original claim referred to "depth 19"; in the paper's framework (arXiv:2603.21852), K denotes the RPN code length (total tree nodes), not the tree height. The actual tree height is 9. The formal interpretation uses exact equality (==) with threshold True. The operator_note documents the full inside-out derivation through 9 layers, identifying two known eml sub-patterns: the triple-nesting identity (steps 3-5, which computes ln of a sub-expression) and the subtraction identity eml(ln(a), exp(b)) = a - b (step 7). The expression has a removable singularity at x = e (where E2 = e - x = 0). The identity holds for all real x != e and at x = e in the limit sense, verified by SymPy's limit function from both sides. For the complex domain, the identity is interpreted as a formal algebraic identity where ln(exp(z)) = z (the paper's framework). On the principal branch of the complex logarithm, the identity holds when |Im(x + y)| < pi. Beyond that boundary, the error is exactly 2*k*pi*i for integer k. **Formalization scope:** The formal interpretation is a faithful mapping of the natural-language claim. The token count K = 19 is explicitly verified. The "for all complex x and y" clause is interpreted in the formal algebraic setting, with the principal-branch limitation documented. The expression was constructed analytically (not extracted from the referenced paper) and verified independently. The removable singularity at x = e is documented and verified via limit analysis. **Attribution:** This result was originally established in A. Odrzywołek, "All elementary functions from a single binary operator," arXiv:2603.21852 (2026). The proof presented here provides independent computational verification using symbolic algebra (SymPy), numerical methods, and exhaustive search, and was developed without reference to the original proof. *Source: proof.py JSON summary* ## Claim Specification | Field | Value | |-------|-------| | Subject | Binary operator eml(a, b) = exp(a) - ln(b) | | Property | eml(1, eml(eml(eml(1, eml(eml(1, eml(1, eml(x, 1))), 1)), eml(y, 1)), 1)) = x + y for all real x, y (x != e) | | Operator | == | | Threshold | True | | Operator Note | The claim asserts that a specific K=19 binary tree of eml operations evaluates to x + y. K denotes the total number of tree nodes (9 internal eml nodes + 10 leaves = 19). Working inside out through 9 layers: (1) E1 = eml(x, 1) = exp(x). (2) E2 = eml(1, E1) = e - x. (3) E3 = eml(1, E2) = e - ln(e-x). (4) E4 = eml(E3, 1) = exp(e)/(e-x). (5) E5 = eml(1, E4) = ln(e-x). Steps 3-5 are the triple-nesting identity applied to (e-x). (6) E6 = eml(y, 1) = exp(y). (7) E7 = eml(E5, E6) = (e-x) - y = e - x - y. This is the eml-subtraction identity eml(ln(a), exp(b)) = a - b. (8) E8 = eml(E7, 1) = exp(e - x - y). (9) E9 = eml(1, E8) = e - ln(exp(e-x-y)) = e - (e-x-y) = x + y. The expression is undefined at x = e (where E2 = 0 causes log(0) in E3); this is a removable singularity — the limit from both sides equals e + y = x + y, verified by SymPy. For complex x, y: the identity holds as a formal algebraic identity where ln(exp(z)) = z (i.e., on the Riemann surface of log). On the principal branch, it holds when |Im(x+y)| < pi; beyond that, the error is exactly 2*k*pi*i for integer k. | *Source: proof.py JSON summary* ## Fact Registry | ID | Label | Key | |----|-------|-----| | A1 | Token count K = 19 (9 eml operations + 10 leaves) | -- | | A2 | Step-by-step symbolic evaluation: E9 = x + y | -- | | A3 | Full expression minus (x + y) = 0 | -- | | A4 | Removable singularity at x = e: limit equals e + y | -- | | A5 | Numerical spot-check at 10 real-valued (x, y) pairs | -- | | A6 | Numerical spot-check at 5 complex-valued (x, y) pairs | -- | | A7 | Exhaustive search: no K <= 15 eml tree computes x + y | -- | *Source: proof.py JSON summary* ## Full Evidence Table ### Type A (Computed) Facts | ID | Fact | Method | Result | |----|------|--------|--------| | A1 | Token count K = 19 (9 eml operations + 10 leaves) | Programmatic parsing of the expression string to count eml operation nodes and leaf nodes (1, x, y) | Confirmed: 9 eml + 10 leaves = K = 19 | | A2 | Step-by-step symbolic evaluation: E9 = x + y | SymPy symbolic evaluation through 9 layers: build each sub-expression E1..E9 with simplification at each step, verify residuals at 5 critical algebraic cancellation points (E1=exp(x), E2=e-x, E4=exp(e)/(e-x), E7=e-x-y, E9=x+y) all equal zero | Confirmed: all 5 critical residuals = 0, E9 = x + y | | A3 | Full expression minus (x + y) = 0 | SymPy simplify(E9 - (x + y)) for real symbols x, y; verify residual equals 0 | Confirmed: residual = 0 | | A4 | Removable singularity at x = e: limit equals e + y | SymPy limit(E9, x, e) from left, right, and both sides; verify all three equal e + y | Confirmed: limit from left = y + E, from right = y + E, both = e + y | | A5 | Numerical spot-check at 10 real-valued (x, y) pairs | Numerical evaluation of the full 9-layer chain at 10 real-valued (x, y) pairs spanning [-100, 100], including x = 0, x > e, x near the singularity at e (within 1e-12); verify |result - (x+y)| < 1e-6 | Confirmed: max |diff| = 1.26e-14 | | A6 | Numerical spot-check at 5 complex-valued (x, y) pairs | Numerical evaluation of the full 9-layer chain at 5 complex-valued (x, y) pairs with |Im(x+y)| < pi (principal-branch domain); verify |result - (x+y)| < 1e-10 | Confirmed: max |diff| = 1.34e-15 | | A7 | Exhaustive search: no K <= 15 eml tree computes x + y | Embedded exhaustive bottom-up search: enumerate all distinct eml binary trees with leaves {1, x, y} at each odd K from 1 to 15 using numerical fingerprinting at a generic complex test point; check if x+y appears | Confirmed: 1,980,526 distinct values at K=15, x+y not found at any K <= 15 | *Source: proof.py JSON summary* ## Computation Traces ``` Token count: 9 eml operations + 10 leaves = K = 19 A1: K = 19: 19 == 19 = True Step-by-step evaluation: E1=eml(x,1) = exp(x) E2=eml(1,E1) = E - x E3=eml(1,E2) = E - log(E - x) E4=eml(E3,1) = -exp(E)/(x - E) E5=eml(1,E4) = -log(-1/(x - E)) E6=eml(y,1) = exp(y) E7=eml(E5,E6) = -x - y + E E8=eml(E7,1) = exp(-x - y + E) E9=eml(1,E8) = x + y A2a: E1 = exp(x): 0 == 0 = True A2b: E2 = e - x: 0 == 0 = True A2c: E4 = exp(e)/(e-x): 0 == 0 = True A2d: E7 = e - x - y: 0 == 0 = True A2e: E9 = x + y: 0 == 0 = True A3: E9 - (x+y) = 0: 0 == 0 = True Limit as x -> e-: y + E Limit as x -> e+: y + E Limit as x -> e: y + E A4: limit(E9, x->e) = e + y from both sides: True == True = True Numerical (real): x= 2, y= 3 |diff|=0.00e+00 x= -5, y= 8 |diff|=4.44e-16 x= 100, y= -99 |diff|=1.26e-14 x= 0.001, y= 0.002 |diff|=5.58e-16 x= 2.5, y= 3.14159 |diff|=0.00e+00 x= -100, y= 100.5 |diff|=4.00e-15 x= 0, y= 0 |diff|=0.00e+00 x= 2.718280828459, y= 0 |diff|=0.00e+00 x= 2.718282828459, y= 0 |diff|=1.22e-22 x= 2.718281828458, y= 2.71828 |diff|=0.00e+00 A5: all real spot-checks agree within 1e-6: True == True = True Numerical (complex, |Im(x+y)| < pi): x= (1+0.5j), y= (2-0.3j) |Im|=0.2 |diff|=1.67e-16 x= (0.5+1j), y= (-1.5+2j) |Im|=3.0 |diff|=0.00e+00 x= (-3+0.7j), y= (4-0.7j) |Im|=0.0 |diff|=1.34e-15 x= 1j, y= (-0-1j) |Im|=0.0 |diff|=4.58e-16 x= (2+3j), y= (-1-0.1j) |Im|=2.9 |diff|=0.00e+00 A6: all complex spot-checks agree within 1e-10: True == True = True Exhaustive search K=1..15: K= 1: 3 distinct values K= 3: 9 distinct values K= 5: 54 distinct values K= 7: 380 distinct values K= 9: 2,971 distinct values K=11: 24,836 distinct values K=13: 217,969 distinct values K=15: 1,980,526 distinct values Search time: 3.13s x+y found at K <= 15: None A7: no K <= 15 tree computes x+y: True == True = True All facts verified (symbolic + numerical + search): True == True = True ``` *Source: proof.py inline output (execution trace)* ## Adversarial Checks (Rule 5) ### Check 1: Does the identity hold for real x > e? - **Question:** Does the identity hold for real x > e, where the intermediate value e - x is negative? - **Verification performed:** For x > e (e.g., x = 100), E2 = e - x < 0. Then E3 = e - log(e-x) involves log of a negative real, producing a complex intermediate with imaginary part -pi*i. Tracing: E3 = (e - ln|e-x|) - pi*i, E4 = exp(E3) = -(exp(e)/|e-x|) (negative real), E5 = e - log(E4) = ln|e-x| - pi*i. Then E7 = exp(E5) - log(exp(y)) = -(e-x) - y = e-x-y (real). The +/-pi*i terms cancel exactly. Numerical tests at x=100/y=-99 and x=e+1e-6/y=0 confirm |diff| < 2e-14. - **Finding:** The identity holds for all real x != e (including x > e). Intermediate complex values with +/-pi*i cancel perfectly. - **Breaks proof:** No ### Check 2: Is x = e a genuine exception or a removable singularity? - **Question:** Is x = e a genuine exception or a removable singularity? - **Verification performed:** At x = e, E2 = 0, and E3 = eml(1, 0) = e - log(0) is undefined (log(0) = -infinity). SymPy's limit() function confirms: lim_{x->e-} E9 = e + y, lim_{x->e+} E9 = e + y, and the two-sided limit = e + y. Since both one-sided limits exist and equal x + y = e + y, this is a removable singularity. Numerical evaluation at x = e - 1e-12 gives |diff| < 1e-6, confirming the expression approaches the correct value. - **Finding:** x = e is a removable singularity. The expression is undefined at that single point but its limit from both sides equals e + y. The identity holds for all real x except this isolated point. - **Breaks proof:** No ### Check 3: Complex branch cut analysis - **Question:** Does the identity hold for arbitrary complex x, y on the principal branch of log? - **Verification performed:** E9 = e - log(exp(e - x - y)). On the principal branch, log(exp(z)) = z iff Im(z) in (-pi, pi]. Since Im(e - x - y) = -Im(x + y), the identity holds when |Im(x + y)| < pi. Verification: x=0.5+i, y=-1.5+2i gives Im(x+y)=3 < pi and |diff|=0. x=1+2i, y=1+2i gives Im(x+y)=4 > pi and |diff|=2*pi (branch-cut error of exactly 2*pi*i). In the paper's formal algebraic framework, ln(exp(z)) = z is an axiom (equivalently, working on the Riemann surface), and the identity holds for all complex x, y. - **Finding:** On the principal branch: holds when |Im(x+y)| < pi. As a formal algebraic identity: holds for all complex x, y. The branch-cut error is always exactly 2*k*pi*i. - **Breaks proof:** No ### Check 4: Minimality of K = 19 - **Question:** Is K = 19 the minimum code length for addition? - **Verification performed:** An embedded exhaustive search (A7) enumerated all distinct eml trees through K=15 (1,980,526 distinct values at K=15) and found no expression evaluating to x+y. A separate external search extended through K=17 (18,470,098 distinct values, 572 seconds) with the same result: closest match at K=17 was |diff|=2.0e-3, not a match. No expression at K <= 17 computes x+y. This is consistent with the result in arXiv:2603.21852 that K=19 is minimal for addition. - **Finding:** Exhaustive search through K=15 (embedded, reproducible) and K=17 (external) found no eml tree computing x+y. K=19 is confirmed minimal. - **Breaks proof:** No ### Check 5: Numerical overflow risk - **Question:** Could numerical overflow cause false agreement? - **Verification performed:** The largest intermediate value in the chain is E4 or E8. E4 = exp(e)/(e-x): for x near e, this diverges (the singularity), but E5 = log(E4) brings it back down. E8 = exp(e-x-y): for x=-100, y=100.5, E8 = exp(e-0.5) ~ 9.19. The log-exp cancellation in E5=ln(e-x) undoes the exponential growth from E4, keeping the chain bounded. The symbolic proof does not depend on floating-point. - **Finding:** No overflow risk. The log-exp cancellation at E5 bounds intermediate values. The proof rests on exact symbolic algebra. - **Breaks proof:** No *Source: proof.py JSON summary* ## Quality Checks - **Rule 1:** N/A -- pure computation, no empirical facts - **Rule 2:** N/A -- pure computation, no empirical facts - **Rule 3:** N/A -- proof is not time-sensitive; date.today() used only in generator metadata - **Rule 4:** CLAIM_FORMAL with operator_note present; documents the full 9-layer inside-out derivation, domain restrictions, removable singularity at x = e, and complex branch-cut behavior - **Rule 5:** 5 adversarial checks: large-x behavior with +/-pi*i cancellation, singularity analysis with limit verification, complex branch cut boundary, minimality cross-reference with embedded search, numerical overflow risk - **Rule 6:** N/A -- pure computation, no empirical facts. Cross-checks use mathematically independent methods (numerical evaluation via cmath vs. symbolic algebra via SymPy; exhaustive search vs. analytical construction) - **Rule 7:** All computations via SymPy (symbolic) and cmath (numerical); no hard-coded constants - **validate_proof.py result:** PASS -- 16/16 checks passed, 0 issues, 0 warnings *Source: author analysis* --- Generated by [proof-engine](https://github.com/yaniv-golan/proof-engine) v1.18.0 on 2026-04-16.