14. Model versus reality: the remainder¶

← 13. The fractal layer · Table of contents · 15. The chain to twins →

Lean: EuclidsPath/Engine/RealFourCorner.lean (real_four_corner_decomp, real_four_corner_of_remainder). Numerical measurement: tools/RESULTS_remainder.md.

In the previous chapter 13 we built the fractal layer of the engine and showed that the direction R_fc ≤ 1 is forced not by the density of primes but by the exclusivity of two: at each prime, the contribution to the ranks (r_-, r_+) is exclusive, whence the rank generating function is the product ∏_p (c_p + a_p x + b_p y) with no cross term xy. This gave the model four-corner.

But a model is not reality. In the present chapter we honestly separate these two things: we introduce an exact decomposition of the real four-corner into the model part and a remainder, write out the identity of the remainder term, and show exactly where the entire programme runs up against one single node — control of the remainder's sign.

Model and reality: two systems of accounts¶

Let us recall the setting. We work with rank counts N_{ij} — the number of carrier centres of a given layer for which the side 6m-1 has rank (number of distinguishing small divisors) i and the side 6m+1 has rank j. The four-corner is the inequality

\[ N_{00}\, N_{33} \;\le\; N_{03}\, N_{30}, \tag{14.1} \]

which expresses negative association of the ranks: "both high" is rarer than "crosswise".

We have two realisations of these counts.

Definition 14.1 (model counts). The model counts N_{ij}^{CRT} are generated by the CRT generating function ∏_q G_q, G_q = c_q(1 + w_q(x+z)), w_q = 1/(q-2). They factorise over the primes and by construction satisfy the model four-corner (ModelFourCorner, model_four_corner), which reduces to the binomial identity \(20\cdot C(n,6) \le C(n,3)^2\) (four_corner_binom).

Definition 14.2 (real counts). The real counts N_{ij}^{real} are the actual counts obtained by sieving, with no assumption of independence of the primes.

The model counts we have proven elementarily; the real ones are what we actually need. The difference between them is the only thing standing between the machine-verified route and the twin conjecture.

Definition 14.3 (sieve remainder). For each corner (i,j) set

\[ e_{ij} \;:=\; N_{ij}^{real} - N_{ij}^{CRT}. \tag{14.2} \]

The remainder e_{ij} is an integer of arbitrary sign (reality may either undercount or overshoot the model).

The key disciplinary requirement: e_{ij} ∈ ℤ with no assumptions about sign or smallness. All we allow ourselves to do with the remainder is ring algebra over ℤ. No analysis, no distribution, no sieve estimates.

The exact decomposition¶

For brevity, denote the model counts of the four corners by m00 = N_{00}^{CRT}, m03, m30, m33 and the corresponding remainders by e00, e03, e30, e33. The real count of each corner is m + e. Substitute this into the real four-corner and expand.

Theorem 14.4 (real_four_corner_decomp). For any integers m00, m03, m30, m33, e00, e03, e30, e33

\[ (m_{00}+e_{00})(m_{33}+e_{33}) - (m_{03}+e_{03})(m_{30}+e_{30}) \]

\[ =\; \underbrace{(m_{00}m_{33} - m_{03}m_{30})}_{\text{model difference } \Delta_{model}} \;+\; \underbrace{(m_{00}e_{33} + e_{00}m_{33} + e_{00}e_{33} - m_{03}e_{30} - e_{03}m_{30} - e_{03}e_{30})}_{\text{remainder term } R}. \tag{14.3} \]

In Lean this is a pure ring identity, closed by the ring tactic. No geometry, no sieve — just expanding brackets. The value of the theorem is that it is exact: not an approximation and not an estimate, but an identity. The real four-corner difference equals exactly the model difference plus the explicitly written remainder term R.

Note. Observe the structure of R. It splits into three groups. The cross terms linear in the remainder, m_{00}e_{33} - m_{03}e_{30} - e_{03}m_{30} + e_{00}m_{33}, are the first order of reality's deviation from the model. The quadratic terms e_{00}e_{33} - e_{03}e_{30} are the "four-corner of the remainder itself". This is precisely why we cannot simply bound R component by component: it mixes model and remainder, and its sign depends on the correlation between the corners.

The reduction: the real four-corner from the model one plus control of the remainder¶

The identity gives us a precise condition under which the real four-corner follows from the model one. The model part Δ_{model} = m_{00}m_{33} - m_{03}m_{30} we control: the model four-corner is \(m_{00}m_{33} \le m_{03}m_{30}\), that is, \(Δ_{model} \le 0\), and the model margin is \(m_{03}m_{30} - m_{00}m_{33} = -\Delta_{model} \ge 0\). Then the real four-corner holds exactly when the remainder fits within this margin.

Theorem 14.5 (real_four_corner_of_remainder). Suppose the model four-corner holds,

\[ m_{00}\, m_{33} \;\le\; m_{03}\, m_{30} \qquad (\text{hypothesis } \verb|_hmodel|), \]

and the remainder term fits within the model margin,

\[ R \;=\; m_{00}e_{33} + e_{00}m_{33} + e_{00}e_{33} - m_{03}e_{30} - e_{03}m_{30} - e_{03}e_{30} \;\le\; m_{03}m_{30} - m_{00}m_{33} \qquad (\text{hypothesis } \verb|hrem|). \]

Then the real four-corner holds as well:

\[ (m_{00}+e_{00})(m_{33}+e_{33}) \;\le\; (m_{03}+e_{03})(m_{30}+e_{30}). \]

The proof in Lean is straightforward: we substitute the decomposition of Theorem 14.4 (real_four_corner_decomp), from the hypothesis hrem we conclude that the real difference is \(\le 0\) (via linarith), whence the inequality. Logically the theorem asserts exactly what we wanted: real four-corner ⟺ model four-corner (proven) + one inequality on the remainder.

Conclusion. This is the programme's honest boundary, written out as a single formula. We have not hidden the difficulty — we have localised it. All the mathematical content of the twin conjecture left open in this branch is compressed into a single hypothesis hrem: the remainder must not flip the sign of the model four-corner, that is, it must not grow enough to overrun the model margin \(-\Delta_{model}\).

Note. We stress that Theorem 14.5 (real_four_corner_of_remainder) is a reduction, NOT a proof of the real four-corner. The hypothesis hrem is not proven and does not, in general, follow from what has already been established. Passing this theorem off as a proof would be a substitution: it merely shifts the burden from "the real four-corner" to "the remainder fits within the margin" — an exact but open goal.

The numbers: a remainder around 4× the model¶

To understand how narrow this node is, we measured the remainder directly (remainder_harness.py, summary in tools/RESULTS_remainder.md). We compared the real N_{ij}^{real} from the sieve with the model \(N_{ij}^{CRT} = T\cdot\prod_q c_q \cdot C(i+j,i)\cdot e_{i+j}\) (generating function ∏_q(1 + w_q(x+z)), w_q = 1/(q-2)).

The result is disheartening. The remainder is not small — it is huge and systematic:

corner	`e/model`, k=20	k=22	k=24
`N_{00}`	−17%	−18%	−18%
`N_{03}, N_{30}`	+85%	+85%	+87%
`N_{33}`	+283%	+298%	+326% (growing)

The CRT model undercounts N_{33} by a factor of 3.8–4.3; the remainder at high ranks is larger than the model counts themselves. In other words, the remainder term R is not a correction to the model — it is of the same order as (and larger than) the main term. The observation: reality in the corner (3,3) is systematically denser than the model, and the gap grows with scale.

Now — does the margin hold? Let us compare the real and model four-corner ratios R_{fc} = N_{00}N_{33}/(N_{03}N_{30}):

	k=20	k=22	k=24
`R_{fc}^{real}`	0.873	0.918	0.976
\(R_{fc}^{model} = 20\,e_6/e_3^2\)	0.937	0.959	0.973

Both ratios tend to 1 from below (the model margin \(-\Delta_{model} \to 0\)), but at k=24 they cross: the real excess overtakes the model one. The real four-corner still holds at that point (R_{fc}^{real} < 1), but the model margin no longer covers it.

Note. This is precisely the situation that hrem formalises. The hypothesis demands \(R \le -\Delta_{model}\). But at k=24 the real excess has exceeded the model one — that is, empirically R no longer fits within the model margin. The real four-corner holds for a different, non-model reason.

Where the node is open: the conjecture and the closure plan¶

Section takeaway. The numerical verdict is unambiguous: transferring model→reality in a distribution-free style by bounding the remainder with the model margin does not work. The remainder is around 4× the model and overtakes the vanishing model margin. The real four-corner holds, but not thanks to the model construction — which means something the CRT model does not see stands behind its stability. This is the parity problem: the hypothesis hrem, as formulated (through the model margin), is unattainable.

Conjecture 14.6 (open node). The real four-corner \(N_{00}^{real} N_{33}^{real} \le N_{03}^{real} N_{30}^{real}\) holds at arbitrarily large scales. Equivalently (by Theorem 14.4 (real_four_corner_decomp)): the remainder term R does not flip the sign of the real four-corner difference, that is, \(R \le -\Delta_{model}\).

Closure plan (and its boundary). The naive plan — to prove hrem via the model margin \(-\Delta_{model}\) — is refuted by measurement: the margin melts faster than the remainder grows. It is natural to conjecture that direct control of the sign of the real difference is needed, one that does not pass through the model: bounding R not from above by the number \(-\Delta_{model}\), but through the remainder's own structure (the exclusivity of two at the level of real, not model, counts). Here the line runs up against parity: any purely counting argument (via the model margin) is insufficient. By the programme's red line this node must NOT be closed by the distribution of primes or a large sieve. If the only available path demands exactly that — we stop and show the exact point; and this point is the hypothesis hrem, in its non-model version.

Note. The value of the chapter is not that the node is closed — it is open. The value is that the entire unresolved part of the problem is compressed into one exact integer inequality hrem on an explicitly written remainder term, isolated non-circularly and machine-verifiably (Theorem 14.5, real_four_corner_of_remainder). We know exactly what remains to be proven, and we know — from the numbers — that the model margin is insufficient for it.

Bridge to the next chapter¶

So we have an exact fork: real four-corner ⟸ model four-corner (proven) + hrem (open, non-model). In the next chapter 15 ToTwins we assemble exactly this fork into one machine-verified chain: the real four-corner plus the side-corner give N_{33} < N_{00}, whence a surviving carrier centre, whence a twin, whence TwinLowers.Infinite.

The real four-corner enters there as the open input H — a gate, that is, an honestly named missing statement (see the glossary); this is the first exact formulation of the programme's single distributional node, which will later be rethought no longer as a counting node but as a structural one 18 SNOL. In other words, chapter 15 shows that hrem is not one of many difficulties, but the difficulty — the single one to which the entire branch reduces.

← 13. The fractal layer · Table of contents · 15. The chain to twins →