FPRD LabShare an approach

← Claims

Theorem · explicit separation

AFD-11

A binary ZILP function of exact floor depth two

Exact statement

The increasing binary ZILP function f(x,y)=⌊x/3⌋+⌊y/3⌋+1{x≡y≡2(mod3)}f(x,y)=\lfloor x/3\rfloor+\lfloor y/3\rfloor+\mathbf1_{\{x\equiv y\equiv2\pmod3\}} belongs to R2∖R1R_2\setminus R_1, so its exact floor depth is two.

StatusProved internally; literature and priority audit pending
External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

This resolves the program's selected binary alternative by separation. The source paper provides the hierarchy, upper bound, and question; the explicit witness and all-denominator lower bound are internal FPRD work.

Definitions

  • R0R_0 is the nonnegative affine class; RnR_n closes addition and floors of functions from Rn−1R_{n-1}.
  • A binary ZILP function is zero at zero, weakly increasing, integer-valued, and rational-linear plus periodic.

Hypotheses and scope

  • The depth-one normal form has nonnegative coefficients and permits arbitrary positive denominators and primings.
  • Floor depth is formula depth, not circuit size or number of summands.

Proof or evidence

The horizontal increment support modulo three is a noncollinear three-point set. Every nonempty pulse fiber of a primitive horizontal depth-one term projects to a line or the full torus; positivity prevents cancellation. A displayed nested-floor formula supplies direct R2 membership.

Binary depth-two theorem and proof structure →

Verification notes

The complete Run 5 proof artifact was read. Its hostile audit checks denominator scope, positivity, priming, and the distinction between finite candidate search and the all-denominator proof. This site has not completed the requested external literature/priority audit.

Limitations

  • No novelty or priority claim is made.
  • The result settles the selected two-input target, not sharpness for all arities.

Open work

Conduct a focused primary-literature and priority audit before novelty or current-open language.