Three complete worlds at a mixed prefix
Abstract
Three complete worlds at a mixed prefix
Theorem 1.1 (Exclusion with both first-response constraints).
Lean statement: D5/S3/Observer/CubicGain/MixedTripleExclusion.mixed_prefix_three_world_exclusion
Proof. Machine-checked in Lean as D5/S3/Observer/CubicGain/MixedTripleExclusion.mixed_prefix_three_world_exclusion (✓ std3). ∎
Source. Repository-derived.
Commentary.
Fix arbitrary real a0, j, m and b, with m-j nonzero, and a chronological word v equal to JM or MJ. The support T consists of exactly three complete worlds with pairwise different sources. Each source is a strictly entrywise positive real two by two matrix of rank one and trace one. Each world has one nonzero entire real gain polynomial of degree at most three and one arbitrary real drift. Every member has initial reading a0, first-J response j, first-M response m, and response b at the actual mixed clock-two matrix. Both first equations constrain the same fixed worlds; they do not denote two acquired reads.
A response child is the full intersection of the current support with the equality for the next actual read. Every node retains the requirement of at least two complete worlds. The continuation matrices multiply the actual prefix on the left, and the original clocks three through seven are retained. The conclusion excludes five further levels of losing recursion on this support and mixed history.
For a two-world losing child with at least three remaining levels, every retained continuation is the same whole pair. The equal-trace certificate for three subsequent actions forces equal drifts. The two-action certificate, composed with any fixed earlier continuation, then forces every weighted source difference from its second future clock onward to vanish. Different trace-one sources force both gain samples to be zero.
In particular, a two-world third child would have gain roots five, six and seven. Its common drift and initial value determine the same entire polynomial at four distinct nodes. A fourth root at clock one or two would violate the nonzero gain condition. The two first-response equalities and the selected mixed second equality then identify the sources, contrary to their distinction. Thus each third action retains all three worlds.
Normalize a source by its positive bottom-right entry d: x=P12/d, y=P21/d, R=[[xy,x],[y,1]], P=dR and d(1+xy)=1. The normalized entire gain is h=dg. Both first responses give h(1)=m-j and drift j-(m-j)(x+y). For a selected pair, equal drift therefore gives equal x+y. In the chronological JM orientation, the two third responses have trace factors xy+x+y and xy+2x+y+1. Eliminating the two third gain samples gives hW(3)(xW-xZ)(xWxZ+xW+xZ)=0. Positivity and different sources force both third gain samples to vanish; interpolation at zero, three, six and seven then excludes that fourth pair.
In the chronological MJ orientation, the third trace factors are x+y+1 and x+y+2. A fourth pair has a common normalized polynomial, fixed at one, three, six and seven. If the initial value differs from its common drift, the initial equation fixes the same xy; a nonzero second sample would already identify the source. Roots two, six and seven make samples four and five nonzero, and the actual fourth and fifth-J equations exclude each of the four choices of third and fourth actions. If the initial value equals the pair drift, roots zero, six and seven instead make samples two, four and five nonzero. The second read fixes xy+y; the fourth and fifth-J equations leave only the third-J/fourth-J choice. This exceptional pair differs at the fourth-M sibling. Recursion at the same third-J node requires a losing fourth-M response intersection; it cannot be a pair and so contains all three worlds, including both exceptional endpoints. Their required equality at that sibling contradicts the calculated difference. No drift equality with the third world is used in this argument.
Once all four fourth histories retain the triple, compare two members with weighted source difference D=gW(4)PW-gZ(4)PZ. The two-action equal-trace certificate gives QD=(driftZ-driftW)E11. In normalized coordinates, equality of the other three entries forces the two normalized scalar weights to agree. If this weight were nonzero, those entries would determine both x and y and hence identify the source. Thus both fourth samples vanish and the drifts agree. This comparison applies to every pair in the triple and establishes the common drift across the whole support.
A fifth child that is a pair has only two losing levels left. Its common drift is now inherited from the triple. All two-action continuations at clock seven give zero traces of the actual clock-five matrix times its weighted source difference. The two-action certificate and invertibility force both seventh samples to vanish. In the JM orientation every world already has root three, from the same positive factored identity used above. A fifth pair would therefore have roots three, four and seven; the common initial value and drift identify its entire gain, and then its source. In the MJ orientation the shared third reads determine the same normalized third sample. A fifth pair with nonzero initial offset has a common normalized gain from clocks one, three, four and seven; its clock-two sample must vanish. Samples five and six are consequently nonzero. The clock-five and both clock-six equalities would make the actual clock-five matrix scalar, contradicting its determinant minus one.
For zero initial offset in the MJ orientation, the whole triple has one normalized polynomial, determined at zero, one, three and four. A seventh root on any putative fifth pair is therefore a root of this common polynomial. Its second sample is nonzero, so the second reading fixes xy+y on the triple. Since x+y=s is common, every y solves y squared minus (s+1)y plus one fixed constant equals zero. Distinct sources require distinct y, but a quadratic cannot have three distinct real roots. Hence fifth children always retain the triple. The three-action trace certificate then forces all fifth samples to vanish. In the JM orientation, roots three, four and five and the common initial value identify the entire gain and source. In the MJ orientation, nonzero initial offset gives one normalized polynomial from clocks one, three, four and five and fixes xy; together with x+y=s this again permits at most two sources. Zero initial offset instead gives roots zero, four and five, a nonzero second sample and the preceding quadratic contradiction. These conclusions exclude the original five-level losing recursion on the same three worlds.