Blind read-back of Definition.lean

cwFourthObj

For every universe level $u$, every type $K : \mathrm{Type}\,u$ equipped with a field structure, and every natural number $q$, including $q=0$, this defines an order-$3$ tensor object by the explicitly parenthesized fourfold Kronecker product $\operatorname{kron}(\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)),\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)))$; the imported notions $\mathrm{CWObj}$, tensor object, and Kronecker product are not further defined by this file, and this declaration asserts no additional property of the resulting object.

cwFourthPairGrade

For every $q\in\mathbb N$, including $q=0$, and every $p=((p_{00},p_{01}),(p_{10},p_{11}))$ whose four entries lie in $\operatorname{Fin}(q+2)$, let $g_q(r)$ denote the underlying natural-number value of the imported grade $\mathrm{cwSquarePairGrade}(q,r)$. This defines $\mathrm{cwFourthPairGrade}(q,p)\in\operatorname{Fin}(9)$ to be the finite index whose underlying value is exactly $g_q((p_{00},p_{01}))+g_q((p_{10},p_{11}))$; the supplied proof establishes that this sum is less than $9$, so no reduction modulo $9$ or truncation occurs.

fourthScalarTower

For every type $K : \mathrm{Type}\,u$ with a field structure and every type $V : \mathrm{Type}\,u$ with both an additive-commutative-group structure and a $K$-module structure, this private instance supplies an $\operatorname{IsScalarTower}(K,K,V)$ structure, using the scalar action induced by the algebra map; there are no further hypotheses on $K$ or $V$.

cwFourthCanonicalBasis

For every type $K : \mathrm{Type}\,u$ with a field structure, every $q\in\mathbb N$, and every component $s\in\operatorname{Fin}(3)$, this noncomputably defines a $K$-basis of the $s$-component of $\operatorname{kron}(\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)),\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)))$, indexed by $(\operatorname{Fin}(q+2)\times\operatorname{Fin}(q+2))\times(\operatorname{Fin}(q+2)\times\operatorname{Fin}(q+2))$, as the tensor-product basis of two copies of the imported basis $\mathrm{cwSquareCanonicalBasis}(K,q,s)$; $q=0$ and each of $s=0,1,2$ are included.

cwFourthCanonicalGrading

For every type $K : \mathrm{Type}\,u$ with a field structure and every $q\in\mathbb N$, this noncomputably defines a $9$-grade internal type grading of $\operatorname{kron}(\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)),\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)))$. For each component $s\in\operatorname{Fin}(3)$, its decomposition is the imported basis grading formed from the tensor-product basis of two copies of $\mathrm{cwSquareCanonicalBasis}(K,q,s)$, with an index $(r_0,r_1)$ assigned the $\operatorname{Fin}(9)$-grade whose underlying value is $\mathrm{cwSquarePairGrade}(q,r_0).\mathrm{val}+\mathrm{cwSquarePairGrade}(q,r_1).\mathrm{val}$; its internality field is the corresponding imported theorem $\mathrm{cwBasisGrade\_isInternal}$, and no claim beyond the data required by the grading structure is added.

cwFourthBlockType

For every $I,J,L\in\operatorname{Fin}(9)$, this defines a function $\operatorname{Fin}(3)\to\operatorname{Fin}(9)$ that sends $0$ to $I$, $1$ to $J$, and $2$ to $L$; these are all possible inputs in $\operatorname{Fin}(3)$.

cwFourthConstituent

For every type $K : \mathrm{Type}\,u$ with a field structure, every $q\in\mathbb N$, and every $I,J,L\in\operatorname{Fin}(9)$, this noncomputably defines an order-$3$ tensor object as the block subtensor, at componentwise grades $(I,J,L)$, of the $9$-grade internal grading of the fourfold Kronecker object $\operatorname{kron}(\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)),\operatorname{kron}(\mathrm{CWObj}(K,q),\mathrm{CWObj}(K,q)))$; that grading is obtained in each component from the tensor-product canonical basis and assigns a pair of square-basis indices the sum of their two imported square-pair grades, as an element of $\operatorname{Fin}(9)$.

classRep

This defines a function from $\operatorname{Fin}(10)$ to functions $\operatorname{Fin}(3)\to\operatorname{Fin}(9)$. Identifying each such function with its ordered triple of values at $0,1,2$, its ten values, in index order $0,\ldots,9$, are exactly $(0,0,8)$, $(0,1,7)$, $(0,2,6)$, $(0,3,5)$, $(0,4,4)$, $(1,1,6)$, $(1,2,5)$, $(1,3,4)$, $(2,2,4)$, and $(2,3,3)$.

classMultiplicity

This defines a natural-number-valued function on $\operatorname{Fin}(10)$ whose values at indices $0,\ldots,9$ are exactly $(1,2,2,2,1,1,2,2,1,1)$, respectively.

sameOrbit

For arbitrary functions $\sigma,\rho:\operatorname{Fin}(3)\to\operatorname{Fin}(9)$, $\mathrm{sameOrbit}(\sigma,\rho)$ means that there exists a permutation $e$ of the three-element set $\operatorname{Fin}(3)$ such that $\sigma(s)=\rho(e(s))$ for every $s\in\operatorname{Fin}(3)$; the declaration requires existence of at least one such permutation, not uniqueness of the permutation, and imposes no condition on the sums or repetition patterns of the values of either function.

instDecidableSameOrbit

For every pair of functions $\sigma,\rho:\operatorname{Fin}(3)\to\operatorname{Fin}(9)$, this noncomputable instance supplies a classical decision between the proposition that some permutation $e$ satisfies $\sigma(s)=\rho(e(s))$ for all $s$, and its negation; it uses classical proposition decidability and does not provide a computational orbit test.

E

For every $q\in\mathbb N$ and every $\tau\in\mathbb R$, this noncomputably defines $E(q,\tau)=\operatorname{Real.rpow}(2q,3\tau)$, where $2q$ is first computed as a natural number and then viewed as a real. There is no restriction on $q$ or $\tau$; in particular, at $q=0$ this uses the total real-power convention, with $\operatorname{Real.rpow}(0,0)=1$ and $\operatorname{Real.rpow}(0,r)=0$ for $r\ne0$.

H

For every $q\in\mathbb N$ and every $\tau\in\mathbb R$, this noncomputably defines $H(q,\tau)=\operatorname{Real.rpow}(q^2+2,3\tau)$, where $q$ is viewed as a real and $q^2$ is an ordinary natural-exponent square; the base is positive even when $q=0$, and $\tau$ may be negative, zero, or positive.

L

For every $q\in\mathbb N$ and every $\tau\in\mathbb R$, this noncomputably defines $L(q,\tau)=4\,\operatorname{Real.rpow}(q,3\tau)\bigl(\operatorname{Real.rpow}(q,3\tau)+2\bigr)$, with $q$ viewed as a real. No nonzero or positivity hypothesis is imposed: $q=0$ is included, giving $L(0,\tau)=0$ when $\tau\ne0$ under the total real-power convention and $L(0,0)=12$.

classValue

For every $q\in\mathbb N$ and $\tau\in\mathbb R$, write $R(x,r)=\operatorname{Real.rpow}(x,r)$, $e=R(2q,3\tau)$, $h=R(q^2+2,3\tau)$, and $\ell=4R(q,3\tau)(R(q,3\tau)+2)$. This noncomputably defines the real-valued function on $\operatorname{Fin}(10)$ whose values $v_0,\ldots,v_9$ are exactly $\bigl(1,\ R(4q,3\tau),\ R(6q^2+4,3\tau),\ R(4q(q^2+3),3\tau),\ R(q^4+12q^2+6,3\tau),\ 4(e^2+2\ell),\ 4(\ell+eh)(2h+\ell)/h,\ 4(e+\ell)(2+2e+h),\ (2h+\ell)^2(2+2e+h)/h,\ 4(e+\ell)^2(2h+\ell)/\ell\bigr)$, where the displayed squares and fourth power are ordinary natural-exponent powers. The definition has no restriction on $q$ or $\tau$; in particular $\ell$ can be $0$, and real division is total, so a quotient with denominator $0$ is defined using $x/0=0$, rather than making the function partial.

Q

For every real vector $a=(a_0,\ldots,a_9)$ indexed by $\operatorname{Fin}(10)$, with no sign or normalization assumption, this defines the real vector $Q(a)$ indexed by $\operatorname{Fin}(9)$ to be $\bigl(2a_0+2a_1+2a_2+2a_3+a_4,\ 2a_1+2a_5+2a_6+2a_7,\ 2a_2+2a_6+2a_8+a_9,\ 2a_3+2a_7+2a_9,\ 2a_4+2a_7+a_8,\ 2a_3+2a_6,\ 2a_2+a_5,\ 2a_1,\ a_0\bigr)$.

kernelSigma

This defines the real vector indexed by $\operatorname{Fin}(10)$ with coordinates, in index order $0,\ldots,9$, exactly $(0,0,1,0,-2,-2,0,2,0,-2)$.

kernelTau

This defines the real vector indexed by $\operatorname{Fin}(10)$ with coordinates, in index order $0,\ldots,9$, exactly $(0,0,0,1,-2,0,-1,1,2,-2)$.

InZ

For every real vector $a=(a_0,\ldots,a_9)$, $\mathrm{InZ}(a)$ means exactly that every coordinate is nonnegative, $a_i\ge0$ for all $i=0,\ldots,9$, and that $a_0+2a_1+2a_2+2a_3+a_4+a_5+2a_6+2a_7+a_8+a_9=1$; zero coordinates are allowed, and there is no strict-positivity condition.

InKernelQ

For every real vector $x=(x_0,\ldots,x_9)$, $\mathrm{InKernelQ}(x)$ means that all nine coordinates of $Q(x)$ vanish, namely $2x_0+2x_1+2x_2+2x_3+x_4=0$, $2x_1+2x_5+2x_6+2x_7=0$, $2x_2+2x_6+2x_8+x_9=0$, $2x_3+2x_7+2x_9=0$, $2x_4+2x_7+x_8=0$, $2x_3+2x_6=0$, $2x_2+x_5=0$, $2x_1=0$, and $x_0=0$.

InY

For every real vector $x=(x_0,\ldots,x_9)$, $\mathrm{InY}(x)$ means that there exist real numbers $s$ and $t$ such that $x=(0,0,s,t,-2s-2t,-2s,-t,2s+t,2t,-2s-2t)$; the definition asks only for existence of witnesses $s,t$, imposes no sign or normalization condition on them or on $x$, and does not itself state uniqueness.

InN

For every real vector $a=(a_0,\ldots,a_9)$, $\mathrm{InN}(a)$ means simultaneously that $a_i\ge0$ for every $i$, that $a_0+2a_1+2a_2+2a_3+a_4+a_5+2a_6+2a_7+a_8+a_9=1$, that $a_2a_7^2=a_4a_5a_9$, and that $a_3a_7a_8=a_4a_6a_9$; all powers in these two equations are ordinary natural-exponent powers, and zero coordinates are permitted.

marginal

For every real vector $a=(a_0,\ldots,a_9)$ and every $j\in\operatorname{Fin}(9)$, this noncomputably defines $\mathrm{marginal}(a,j)$ as one third of the $j$-th coordinate of $Q(a)$. Thus the nine marginal values are exactly $\frac{1}{3}\bigl(2a_0+2a_1+2a_2+2a_3+a_4,\ 2a_1+2a_5+2a_6+2a_7,\ 2a_2+2a_6+2a_8+a_9,\ 2a_3+2a_7+2a_9,\ 2a_4+2a_7+a_8,\ 2a_3+2a_6,\ 2a_2+a_5,\ 2a_1,\ a_0\bigr)$, with no sign or normalization hypothesis on $a$.

entropyProduct

For every real vector $a=(a_0,\ldots,a_9)$, this noncomputably defines $\mathrm{entropyProduct}(a)$ as $\operatorname{Real.rpow}(a_0,a_0)\operatorname{Real.rpow}(a_1,2a_1)\operatorname{Real.rpow}(a_2,2a_2)\operatorname{Real.rpow}(a_3,2a_3)\operatorname{Real.rpow}(a_4,a_4)\operatorname{Real.rpow}(a_5,a_5)\operatorname{Real.rpow}(a_6,2a_6)\operatorname{Real.rpow}(a_7,2a_7)\operatorname{Real.rpow}(a_8,a_8)\operatorname{Real.rpow}(a_9,a_9)$. The definition assumes neither nonnegativity nor positivity, so it uses the imported total real-power operation even at negative or zero bases; in particular a zero coordinate contributes $\operatorname{Real.rpow}(0,0)=1$.

globalRate

For every $q\in\mathbb N$, every $\tau\in\mathbb R$, and arbitrary real vectors $a=(a_0,\ldots,a_9)$ and $b=(b_0,\ldots,b_9)$, let $R(x,r)=\operatorname{Real.rpow}(x,r)$, $e=R(2q,3\tau)$, $h=R(q^2+2,3\tau)$, $\ell=4R(q,3\tau)(R(q,3\tau)+2)$, $m=(1,2,2,2,1,1,2,2,1,1)$, $v=\bigl(1,R(4q,3\tau),R(6q^2+4,3\tau),R(4q(q^2+3),3\tau),R(q^4+12q^2+6,3\tau),4(e^2+2\ell),4(\ell+eh)(2h+\ell)/h,4(e+\ell)(2+2e+h),(2h+\ell)^2(2+2e+h)/h,4(e+\ell)^2(2h+\ell)/\ell\bigr)$, and $c=\bigl(2a_0+2a_1+2a_2+2a_3+a_4,2a_1+2a_5+2a_6+2a_7,2a_2+2a_6+2a_8+a_9,2a_3+2a_7+2a_9,2a_4+2a_7+a_8,2a_3+2a_6,2a_2+a_5,2a_1,a_0\bigr)$. This noncomputably defines $\mathrm{globalRate}(q,\tau,a,b)=\left(\prod_{i=0}^{9}\left[R(v_i,a_i/3)\,R(a_i,a_i)\,R(b_i,-b_i)\right]^{m_i}\right)\left(\prod_{j=0}^{8}R(c_j/3,-c_j/3)\right)$, where the outer exponent $m_i$ is an ordinary natural-number power, while every occurrence of $R$ is total real exponentiation. There are no sign, normalization, nonzero-denominator, or range hypotheses: $q=0$, zero or negative coordinates, zero marginals, and a possible $\ell=0$ are all included, with real division by $0$ totalized as $x/0=0$.