Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Full Original World Mean Span

Abstract

The unrestricted original world mean family affinely spans all seventeen real coordinates.

Theorem 1.1 (Four positive normalized source columns are independent).

Lean statement: D5/S3/Observer/CubicGain/FullWorldMeanSpan.source_certificate

Proof. Machine-checked in Lean as D5/S3/Observer/CubicGain/FullWorldMeanSpan.source_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each i in Fin 4, sourceR(i) is strictly between zero and one and sourceB(i) is positive. The determinant of programColumns is exactly 1/768. The four source pairs are (1/4,1/8), (1/4,1/6), (1/4,1/4), and (1/3,1/8); programColumns uses column vectorization (00,10,01,11) of sourceMatrix(r,b). The certificate concerns only sources and is independent of the degree or coordinates of a gain.

An original world consists of one program matrix P=[[r,b],[c,1-r]], one whole polynomial g(t)=a₀+a₁t+a₂t²+a₃t³, and one real drift d. Its complete domain has 0<r<1, b>0, c>0, bc=r(1-r), and g not identically zero. There are no bounds or history equations. Every degree from zero to three, zero samples, repeated roots and zero drift remain included.

The native carrier OriginalWorld stores (r,b,d,a) in ordinary coefficient order. FullWorld requires precisely the strict r,b conditions and originalPolynomial W≠0. Since b>0, the source equation forces c=r(1-r)/b; conversely this value is positive and satisfies bc=r(1-r). Thus sourceMatrix gives exactly every source program, and Polynomial.ofFn 4 a gives exactly its whole polynomial. The coefficient map is injective, so nonzero means that the four coefficients are not all zero. Gain here names the four-coordinate type; these coordinates are ordinary coefficients, rather than the sample values used in gainPoly.

Column vectorization is vec(X)=(X₁₁,X₂₁,X₁₂,X₂₂). The native mean uses the same sourceMatrix in every coefficient block. Coordinates are numbered 0 through 16: coordinate 0 is d and coordinate 1+4k+j is a_k vec(P)_j, for k,j from 0 through 3. Write P(W), d(W) and a(W,k) for these components, and let the calligraphic W denote this complete domain. Let M be its image under the mean.

Choose source programs with (r,b,c) equal to (1/4,1/8,3/2), (1/4,1/6,9/8), (1/4,1/4,3/4), and (1/3,1/8,16/9), in that order. All are legal. Let A have their column-vectorizations as columns. Its determinant is 1/768, so its columns span the full four-coordinate block.

Theorem 1.2 (Full unrestricted affine span).

Proof. Machine-checked in Lean as D5/S3/Observer/CubicGain/FullWorldMeanSpan.full_world_mean_span (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a coefficient index k. The worlds with g(t)=t^k and d=0 give the four program vectors in that block. Differences relative to the first program have trace zero because every program has trace one. The difference between g(t)=2t^k and g(t)=t^k at the first program gives its absolute block vector. Every polynomial in these pairs is nonzero. Adding this vector to the three program differences yields all four columns; invertibility of A therefore places every vector in this block in the direction of the affine hull. This holds separately for all four k, while each individual world still has one common P.

Keeping P and g fixed and changing only d gives an arbitrary drift direction. Any vector in the literal seventeen-coordinate space decomposes into this drift vector and its four four-coordinate blocks. Thus the direction of the nonempty affine hull is the whole space, and the affine hull itself is the whole space. No zero-polynomial world is introduced.

This is an exact statement about the complete deterministic mean family. It asserts no equality of Gaussian laws, instrument realization, observation procedure, statistical limit, physical mode count or optimal carrier dimension.

Application: complete seven-reading fibers

This application concerns the same unrestricted domain but a specified seven-reading observation map. It is separate from the affine-span theorem above: full_world_mean_span does not assert the bound below. The application reuses the existing model definitions and the interpolation, finite-cardinality and polynomial-root results named below; it introduces no separate Lean declaration or theorem description. The full even-node atlas and its proof are in FIB_C35_ENTIRE_JM_RESPONSE_INJECTIVITY, §16.1–16.3.

Native parameters are W=(r,b,d,a): r=W.1, b=W.2.1, d=W.2.2.1 and a=W.2.2.2. In the namespace D5.S3.Observer.CubicGain, OriginalWorld is the full product carrier, originalPolynomial W=Polynomial.ofFn 4 a, sourceMatrix r b=[[r,b],[r(1-r)/b,1-r]], and sourceJ r b=b+r(1-r)/b. FullWorldMeanSpan.FullWorld requires 0<r<1, b>0 and originalPolynomial W≠0. These existing frozen declarations give exactly the original positive trace-one rank-one matrices P=[[r,b],[c,1-r]] with bc=r(1-r), because c=r(1-r)/b>0. Conversely every such P, every nonzero real polynomial g of degree at most three, and every independent real drift d give a unique W: Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt recovers g from its ordinary coefficients, and Polynomial.injective_ofFn makes that representation unique. The type Gain here supplies four ordinary coefficients, not four newly fitted samples.

Use the existing frozen matrices actionJ=J=[[0,1],[1,0]] and actionM=M=[[0,1],[1,1]]. E is J or M, corresponding respectively to the Boolean e=false or e=true in the seven-reading parameterization. Its chronological actions are J,M,J,M,J,E. Put Q₀=I and Qᵢ=EᵢQᵢ₋₁ for i=1,…,6, with reading d+g(i)tr(QᵢP). Each row uses the same P, the same whole g and the same d. This action list is specified here explicitly: ParentCoordinates.chronological and originalRead use a fifth M, so their later rows are not this observation map.

Fix E, arbitrary real observations A,C,z,Y,p,v and one b>0. Write F_E(b;A,C,z,Y,p,v) for all FullWorld W with this source entry b and readings (0,A,C,z,Y,p,v). Put j=sourceJ r b, T=1+b, U=1+2b, k=2 for E=J or 3 for E=M, and V=1+kb. Multiplying the six matrices gives the following exact seven-row correspondence: clock 0, Q₀=I, trace 1, d+g(0)=0; clock 1, action J, trace j, d+g(1)j=A; clock 2, action M, trace T, d+g(2)T=C; clock 3, action J, trace j+r, d+g(3)(j+r)=z; clock 4, action M, trace U, d+g(4)U=Y; clock 5, action J, trace j+2r, d+g(5)(j+2r)=p; clock 6, action E, trace V, d+g(6)V=v.

Define K=16TUV>0, B₀=−dTUV, B₂=(C−d)UV, B₄=(Y−d)TV and B₆=(v−d)TU. Set G₁=5B₀+15B₂−5B₄+B₆, G₃=−B₀+9B₂+9B₄−B₆ and G₅=B₀−5B₂+15B₄+5B₆. Each G is affine in d. The drift polynomial is H_E(b,d)=(A−d)G₃G₅−2(z−d)G₁G₅+(p−d)G₁G₃. Its variable is d; g remains the world’s possibly lower-degree polynomial in the clock variable s.

For i∈{0,2,4,6}, let ℓᵢ(s) be the product of (s−q)/(i−q) over the other three even nodes q. The four even rows force g(s)=−dℓ₀(s)+(C−d)ℓ₂(s)/T+(Y−d)ℓ₄(s)/U+(v−d)ℓ₆(s)/V. This uses Polynomial.eq_of_degrees_lt_of_eval_index_eq with s=Finset.univ on Fin 4 and nodes i↦2i, together with Polynomial.ofFn_degree_lt. Both candidate polynomials have degree less than four; the nodes are distinct and T,U,V are positive. Hence at a fixed drift the whole polynomial and all four ordinary coefficients are fixed, not merely four unrelated gain values. Evaluating the displayed basis gives Kg(1)=G₁, Kg(3)=G₃ and Kg(5)=G₅.

The odd rows become G₁j=K(A−d), G₃(j+r)=K(z−d) and G₅(j+2r)=K(p−d). If R₁,R₃,R₅ are the left sides minus their right sides, then R₁G₃G₅−2R₃G₁G₅+R₅G₁G₃=−KH_E, since j−2(j+r)+(j+2r)=0. Thus every retained world gives H_E(b,d)=0, without dividing by any odd sample. Conversely, a triple (d,j,r) gives exactly a complete world when 0<r<1, j>b, b(j−b)=r(1−r), the displayed interpolant is nonzero and all three odd equations hold. Reconstruct c=j−b, P and that single interpolant; their seven rows recover the data. The cubic equation alone does not certify a world. Under z≠A the nonzero-interpolant filter is automatic: g=0 would force all responses, including A and z, to equal d=0.

Expansion gives the coefficient of d³ in H_J as 16b(1+2b)²(4b³+16b²+5b+8), and in H_M as 192b⁴(3b²+12b+4). All factors are positive for every b>0. Since H_E has degree at most three by its defining products, it is a nonzero polynomial of degree exactly three for every choice of the observations. Polynomial.card_roots’ bounds its real-root multiset, with algebraic multiplicity, by three. This is a fact about the drift polynomial, not an exact-degree assumption on g.

Assume from now on z≠A. At a retained drift, G₁ and G₃ cannot both vanish: their odd equations and K≠0 would force A=d=z. A G₅-only configuration and an all-zero configuration are therefore impossible. Every retained drift has either at least two active G values, only G₁ active, or only G₃ active. Vanishing samples remain allowed; their rows require only that the corresponding response equal d.

If at least two G values are nonzero, their rows fix two distinct affine traces j+ir, i∈{0,1,2}. Subtracting fixes r and then j. The even rows already fixed the entire gain, so this gives at most one complete world over that drift. More generally, for two worlds at fixed b,d, equality of r implies equality of g by four-node interpolation, equality of a by Polynomial.injective_ofFn, and equality of W by product extensionality. This supplies the needed injective map from complete worlds at that drift to their r coordinates.

For an explicit bound that also covers the one-active cases, take any finite set S of worlds at the fixed drift and a member with coordinate r₀, unless S is empty. At least one early index i=0 or 1 is active, so its equation fixes j+ir. Substitution of j=b+r(1−r)/b gives (r−r₀)(r+r₀−1−ib)=0 for every member. Thus the injective image under W↦r lies in {r₀,1+ib−r₀}. Finset.card_image_iff, Finset.card_le_card and Finset.card_le_two give |S|≤2, including when the two displayed values coincide. No existence of either source is inferred.

If only G₁ is active, the zero rows give d=z=p and the active row fixes j=K(A−d)/G₁. Legal sources solve r²−r+b(j−b)=0 with 0<r<1. There are at most two distinct legal sources. At this drift d₀=z=p, G₃ and G₅ vanish. In the polynomial variable X, every term of H_E has two factors X−d₀: use G₃G₅ in the first term, (z−X)G₅ in the second and (p−X)G₃ in the third. Polynomial.dvd_iff_isRoot, product divisibility and addition/subtraction of divisible terms therefore give (X−C(d₀))² dividing H_E, where C(d₀) denotes the constant polynomial. Polynomial.le_rootMultiplicity_iff, using H_E≠0, gives root multiplicity at least two.

If only G₃ is active, the zero rows give d=A=p and n=j+r=K(z−d)/G₃ is fixed. Legal sources solve r²−(1+b)r+b(n−b)=0, again with at most two distinct legal roots. At d₀=A=p, G₁ and G₅ vanish; the respective terms contain (A−X)G₅, G₁G₅ and (p−X)G₁. The same divisibility argument gives (X−C(d₀))² dividing H_E and root multiplicity at least two. Division by G₁ or G₃ occurs only in its explicitly active branch. A repeated quadratic root contributes one world; square divisibility does not assert that two worlds exist.

For any finite set S of distinct complete worlds in the fiber, let D(S) be the multiset of their drifts, with repetitions kept, and let R(H_E) be the real-root multiset with algebraic multiplicity. For each real drift d, restrict S to that drift. An empty restriction has count zero. A nonempty restriction of size at most one is paid for by H_E(d)=0, hence multiplicity at least one. If two distinct worlds occur, the two-active case is impossible; one of the one-active cases applies, the source bound gives count at most two, and the square factor gives multiplicity at least two. Thus the count at every d is bounded by its count in R(H_E). Polynomial.count_roots and Multiset.le_iff_count give D(S)≤R(H_E); Multiset.count_map identifies the left count with the restriction of this same S. Distinct-drift counting alone would miss the possible source multiplicity.

Taking multiset cardinalities, Multiset.card_map and Multiset.card_le_card give |S|=|D(S)|≤|R(H_E)|≤3 for every finite subset S of the actual fiber. If that fiber were infinite, Set.Infinite.exists_subset_card_eq would supply a subset of size four, a contradiction. It is therefore finite, and applying the same bound to its finite enumeration, with Set.ncard_coe_finset, proves that its number of distinct complete worlds is at most three. Both finiteness and the bound are conclusions; a bound on Set.ncard alone would not establish finiteness. The empty fiber is included.

The result is quantified separately for each E∈{J,M}, each b>0 and all real A,C,z,Y,p,v with z≠A. It includes zero drift, all signs of gain coefficients, zero samples, nonsampled roots, repeated roots, every degree drop from three to zero, and degenerate source quadratics. Apart from explicitly active samples, denominators are only b,T,U,V and fixed differences of distinct interpolation nodes. The excluded worlds are precisely those outside FullWorld, including an identically zero g, r=0 or 1 and b≤0. There is no upper bound on b or c, genericity premise or bounded source box. The statement gives no bound on the union over b, no existence or sharpness assertion, no physical realization or resource claim, and no literature novelty claim.

The reused project declarations are FullWorldMeanSpan.FullWorld, OriginalWorld and originalPolynomial, ParentCoordinates.Gain and Mat, ParentCoordinates.sourceMatrix, StrictDriftVector.sourceJ, and ParentCoordinates.actionJ and actionM, with module-qualified addresses in D5/S3/Observer/CubicGain. The Polynomial, Finset, Multiset and Set endpoints named in this derivation refer to the pinned Mathlib revision 56a005855ea17e0b0958f73ec801ae140b0a1679. The polynomial identities, branch conditions and native parameter correspondence above specify their application; none of these individual model declarations is itself a seven-reading cardinality theorem.

References