diff --git a/research/frobenius-tensor-characters/README.md b/research/frobenius-tensor-characters/README.md new file mode 100644 index 0000000000..b62f9a906e --- /dev/null +++ b/research/frobenius-tensor-characters/README.md @@ -0,0 +1,160 @@ +# Determinant characters for Frobenius-truncated local algebras + +This package extends the promised tensor class in PR5316 to multivariable local +algebras with unequal characteristic-power cutoffs. It derives the full +stabilizer determinant image and the resulting special-linear orbit count. +It is an algebraic interface result. The complete kappa calculation is unchanged. + +## The algebra and character formula + +Let K=F_q have characteristic p. Choose r>=1 integers e_i>=1, set n_i=p^e_i, +and let + +``` +A = K[x_1,...,x_r] / (x_i^n_i for every i), +N = product_i n_i, +E_i = N (n_i-1) / 2, +h = gcd(q-1,E_1,...,E_r). +``` + +Each E_i is an integer. Let mu in A* tensor A* tensor A be multiplication, +with the ordinary covariant action on its three tensor factors. Then + +``` +Delta(mu) = {(u,v,w) in (K*)^3 : (u v w)^((q-1)/h) = 1}. +``` + +The image has (q-1)^3/h elements. The one GL orbit splits into exactly h +orbits under the product of the three special linear groups. These statements +hold after independent changes of basis in all three tensor factors. +They assume the tensor belongs to this algebra's GL orbit. They do not +recognize that orbit or produce a transporter. + +For equal e_i=1 and odd p, h=(p-1)/2, independent of r and the extension degree +of K. For p=2 and e_i=1, h=1. Unequal or higher cutoffs can change the image: +over F4, the univariate cutoff four has h=3, whereas two cutoff-two variables +have h=1. Both algebras have dimension four, but their determinant images differ. + +## Automorphisms must preserve the height flag + +Write J for the radical. Every automorphism induces an invertible map L on J/J +squared. If the image of x_i has a nonzero linear x_j term, then e_j<=e_i. +Indeed the p^e_i power of that linear term gives a nonzero x_j^(p^e_i) term +when e_j>e_i. Frobenius removes mixed terms. Terms of degree at least two have +power degree at least 2p^e_i and cannot cancel that term. Thus L preserves the +flag given by the spans of variables of height at most e. + +Conversely, every invertible flag-preserving linear substitution respects all +relations: each allowed x_j has n_j dividing n_i. Its inverse preserves the same +flag and relations, so it is an algebra automorphism. More generally, a valid +substitution with invertible tangent map is an automorphism by the finite +radical filtration. Validity of the relations remains a separate condition; +an invertible tangent matrix alone does not authorize forbidden height mixing. + +An automorphism and its linear substitution induce the same map on the +associated graded algebra. Ordering monomials by total degree therefore shows +that they have equal determinants. Higher terms do not change the determinant. + +## Compute the automorphism and unit characters + +A diagonal change x_i -> c x_i has determinant c^E_i. The sum of the x_i +exponents over all N monomials is N(n_i-1)/2. An allowed elementary change +x_i -> x_i+c x_j has determinant one: order monomials by the x_i exponent; +every new term has a smaller exponent, and the diagonal stays one. The +flag-preserving linear group is generated by these elementary changes and +diagonal changes. Within an equal-height block, they generate its full GL group. +If L_e is the tangent block for height e, this proves + +``` +det(sigma) = product_e det(L_e)^(N(p^e-1)/2). +``` + +Independent diagonal scalings attain all products of these power subgroups. +Since K* is cyclic, the exact automorphism determinant image is H_h={c^h:c in K*}. +No determinant of a formal untwisted group algebra is used. + +For a unit a, multiplication by a is triangular on the radical filtration +with constant diagonal a_0. Thus det(L_a)=a_0^N. Since N is a power of p, +N is coprime to q-1, so these unit determinants fill K*. + +The classical unital commutative autotopism normalization, retained in PR5316 +and PR5252, writes every F(x)G(y)=H(xy) as + +``` +F=L_a sigma, G=L_b sigma, H=L_(ab) sigma. +``` + +For completeness, evaluate at 1 to get H(x)=F(x)b=aG(x), where a=F(1), b=G(1). +Bijectivity makes both multiplication maps bijective, hence a,b are units. +Then sigma=(ab)^-1 H is an algebra automorphism. The converse follows by +multiplication. The covariant tensor action uses (F^-T,G^-T,H). If x,y are the +unit determinants and z the automorphism determinant, its ordered triple is + +``` +(u,v,w) = (x^-1 z^-1, y^-1 z^-1, x y z). +``` + +The inverse equations x=vw, y=uw, z=(uvw)^-1 prove the displayed image formula. +Conjugation preserves determinants under independent basis changes. Finally, +the product SL group is the kernel of the determinant map from the product GL +group; its orbits in the fixed GL orbit are the cosets of Delta(mu). This proves +the image size and orbit count. + +The promised character equation can be computed without constructing A. To +compute E_i modulo m=q-1, multiply p^(sum e_i) and p^e_i-1 modulo 2m, then +halve the even residue. Use modular powers and gcd. This uses polynomially +many bit operations in the supplied parameter sizes and avoids constructing +the potentially huge integer N. The characteristic and algebra-class promise +are inputs; this calculation does not factor q or recognize a tensor. + +## Evidence and reproduction + +```sh +python3.12 -B scripts/research_package.py --package research/frobenius-tensor-characters +``` + +The standalone Python 3.12 checker uses its standard library. It implements F4 +as F2[t]/(t squared+t+1), as well as prime fields. It builds literal quotient +multiplication tables and substitution matrices, checks all defining power +relations, compares ambient determinants with the tangent-block formula, and +checks basis products. Three complete automorphism domains include nonlinear +substitutions and unequal heights. Additional bounded domains check elementary +linear and nonlinear maps through algebra dimension 49. Unit multiplication +matrices and the full determinant-triple sets are checked independently. + +Controls distinguish forbidden height mixing, equal dimensions with different +images, the inverse-input convention, and modular exponent extraction. Normal +and optimized checks use explicit exceptions. The written proof supplies the +general finite-field theorem; finite matrix checks are corroboration, not +proof-kernel verification. No predecessor executable is imported. + +## Sources and scope + +The direct handoff is [PR #5316](https://github.com/CrocSwap/integer-mult-bounds/pull/5316) +and its [pinned univariate proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/truncated-tensor-characters/README.md). +Nick Petalas's [PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) +and [finite-etale proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/etale-tensor-determinant-image/README.md) +retain the normalization and inverse-input convention. David Ganz's atlas +retains the character-equation and tensor-action framework. Sources are pinned +as provenance in SOURCES.json. The all-state multivariable/determinant search +and full tracked-note/Discussion search found no same height-flag result; +unposted work and arbitrary historical diffs remain outside coverage. + +## Open next questions + +A next useful task is recognition of this promised algebra class from a +multiplication tensor, with a verified transporter. Start with its radical +filtration and recover the allowed height flag. A field factorization and +basis-recovery algorithm with complete correctness bounds is still missing. +Physical coefficient preparation, native realization, movement, precision and +supplier admission remain separate and unpriced. No selected cold replay, +Lean, Docker, independent human review or new multiplication theorem is claimed. + +## Credit + +Ali Romman's PR5316 supplies the univariate method and explicit multivariable +question. Nick Petalas (@petalas) supplies the finite-etale normalization and +nilpotent follow-up. David Ganz and the atlas sources retain their attribution. +Finite local-algebra filtrations, elementary generators and cyclic power +subgroups are classical. New proof and checks by Ali Romman with substantial +OpenAI Codex assistance; Apache-2.0. No general literature-priority claim is made. diff --git a/research/frobenius-tensor-characters/SOURCES.json b/research/frobenius-tensor-characters/SOURCES.json new file mode 100644 index 0000000000..778cbf67f4 --- /dev/null +++ b/research/frobenius-tensor-characters/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/truncated-tensor-characters/README.md", + "usage": "provenance", + "git_blob": "9dac5ac07eb867ff2ff44bd8f033d0ac1114fb82", + "sha256": "2ebd7660dc342ea7a20c3c67dd58530b8ebf3d224ca13c5f689956338d3a32d7" + }, + { + "path": "research/etale-tensor-determinant-image/README.md", + "usage": "provenance", + "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208", + "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba" + } + ] +} diff --git a/research/frobenius-tensor-characters/TASK.json b/research/frobenius-tensor-characters/TASK.json new file mode 100644 index 0000000000..690ccee053 --- /dev/null +++ b/research/frobenius-tensor-characters/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact stabilizer determinant image for multivariable characteristic-power truncated polynomial algebras, with unequal heights.", + "scope_change_reason": "Take PR5316 multivariable handoff as a written algebraic interface theorem and exact checker.", + "bottleneck_link": "Extend the promised tensor-character class while preserving the inverse-input convention and nilpotent relations.", + "budget_minutes": 60, + "stop_rule": "Prove characters and check finite substitutions; do not claim tensor recognition or a physical supplier.", + "outcome": "completed", + "evidence": "README.md proof; verify.py literal algebra, automorphism, unit and determinant-image checks.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Can this algebra class be recognized from its multiplication tensor with a transporter?", + "why_it_matters": "It would remove the current orbit promise.", + "first_step": "Recover the radical filtration and candidate height flag.", + "blocked_by": "No complete basis-recovery and recognition algorithm is supplied." + } + ] +} diff --git a/research/frobenius-tensor-characters/VERIFY.json b/research/frobenius-tensor-characters/VERIFY.json new file mode 100644 index 0000000000..22f567ae8a --- /dev/null +++ b/research/frobenius-tensor-characters/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact substitution matrices, complete small automorphism domains, unit characters and covariant triples." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact substitution matrices, complete small automorphism domains, unit characters and covariant triples." + } + ] +} diff --git a/research/frobenius-tensor-characters/verify.py b/research/frobenius-tensor-characters/verify.py new file mode 100644 index 0000000000..4d0edc29d6 --- /dev/null +++ b/research/frobenius-tensor-characters/verify.py @@ -0,0 +1,214 @@ +#!/usr/bin/env python3 +"""Check determinant characters in exact finite local algebras. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import product +from math import gcd,prod +import json + + +def require(c,m): + if not c: raise ValueError(m) + + +class Field: + def __init__(self,q): + require(q in (2,3,4,5,7),'unsupported fixture field') + self.q=q; self.p=2 if q==4 else q + self.plus=[[a^b if q==4 else (a+b)%q for b in range(q)] for a in range(q)] + def multiply(a,b): + if q!=4: return a*b%q + c=0 + for _ in range(2): + if b&1: c^=a + b>>=1; a<<=1 + if a&4: a^=7 + return c + self.times=[[multiply(a,b) for b in range(q)] for a in range(q)] + def add(self,a,b): return self.plus[a][b] + def neg(self,a): return a if self.q==4 else -a%self.q + def mul(self,a,b): return self.times[a][b] + def power(self,a,n): + out=1 + while n: + if n&1: out=self.mul(out,a) + a=self.mul(a,a); n//=2 + return out + def inv(self,a): + require(a!=0,'zero inverse'); return self.power(a,self.q-2) + def det(self,A): + A=[list(r) for r in A]; out=1 + for k in range(len(A)): + pivot=next((i for i in range(k,len(A)) if A[i][k]),None) + if pivot is None: return 0 + if pivot!=k: A[k],A[pivot]=A[pivot],A[k]; out=self.neg(out) + out=self.mul(out,A[k][k]); iv=self.inv(A[k][k]) + for i in range(k+1,len(A)): + if A[i][k]: + factor=self.mul(A[i][k],iv) + for j in range(k+1,len(A)): + A[i][j]=self.add(A[i][j],self.neg(self.mul(factor,A[k][j]))) + return out + + +class Algebra: + def __init__(self,q,heights): + self.F=Field(q); self.heights=heights; self.r=len(heights) + self.cutoffs=[self.F.p**e for e in heights] + self.monomials=list(product(*(range(n) for n in self.cutoffs))) + self.N=len(self.monomials); self.index={m:i for i,m in enumerate(self.monomials)} + self.zero=(0,)*self.N; self.one=(1,)+(0,)*(self.N-1) + self.variables=[] + for i in range(self.r): + ex=[0]*self.r; ex[i]=1; v=[0]*self.N; v[self.index[tuple(ex)]]=1; self.variables.append(tuple(v)) + self.table=[] + for a in self.monomials: + row=[] + for b in self.monomials: + c=tuple(x+y for x,y in zip(a,b)); row.append(self.index.get(c,-1)) + self.table.append(row) + def add(self,a,b): return tuple(self.F.add(x,y) for x,y in zip(a,b)) + def scaled(self,c,a): return tuple(self.F.mul(c,x) for x in a) + def mul(self,a,b): + out=[0]*self.N + for i,x in enumerate(a): + if x: + for j,y in enumerate(b): + k=self.table[i][j] + if y and k>=0: out[k]=self.F.add(out[k],self.F.mul(x,y)) + return tuple(out) + def power(self,a,n): + out=self.one + while n: + if n&1: out=self.mul(out,a) + a=self.mul(a,a); n//=2 + return out + def tangent(self,images): + indices=[v.index(1) for v in self.variables] + return [[images[j][i] for j in range(self.r)] for i in indices] + def substitution(self,images): + powers=[] + for a,n in zip(images,self.cutoffs): + row=[self.one] + for _ in range(1,n): row.append(self.mul(row[-1],a)) + powers.append(row) + columns=[] + for monomial in self.monomials: + v=self.one + for i,e in enumerate(monomial): v=self.mul(v,powers[i][e]) + columns.append(v) + return columns + + +def image_index(p,q,heights): + m=q-1; modulus=2*m; N=pow(p,sum(heights),modulus); h=m + for e in heights: + residue=N*(pow(p,e,modulus)-1)%modulus + require(residue%2==0,'even exponent numerator') + h=gcd(h,residue//2) + return h + + +def verify_map(A,images,full): + F=A.F + require(all(a[0]==0 and A.power(a,n)==A.zero for a,n in zip(images,A.cutoffs)), 'invalid substitution relation') + L=A.tangent(images); require(F.det(L)!=0,'singular tangent') + for i,ei in enumerate(A.heights): + for j,ej in enumerate(A.heights): + require(ej<=ei or L[j][i]==0,'height flag violation') + predicted=1 + for e in set(A.heights): + ids=[i for i,h in enumerate(A.heights) if h==e] + block=[[L[i][j] for j in ids] for i in ids] + predicted=F.mul(predicted,F.power(F.det(block),A.N*(F.p**e-1)//2)) + columns=A.substitution(images); actual=F.det(list(zip(*columns))) + require(actual==predicted,'automorphism determinant character') + pairs=0 + indices=range(A.N) if full else [x.index(1) for x in A.variables] + for i in indices: + for j in range(A.N): + k=A.table[i][j]; expected=A.zero if k<0 else columns[k] + require(A.mul(columns[i],columns[j])==expected,'literal multiplication identity'); pairs+=1 + return actual,pairs + + +def main(): + maps=products=units=controls=0; contexts=[]; complete={} + for q,heights in [(4,(2,)),(4,(1,1)),(2,(1,2))]: + A=Algebra(q,heights); count=0; images_seen=set() + radical=[(0,)+v for v in product(range(q),repeat=A.N-1)] + for images in product(radical,repeat=A.r): + if not A.F.det(A.tangent(images)): continue + if any(A.power(a,n)!=A.zero for a,n in zip(images,A.cutoffs)): continue + value,checks=verify_map(A,images,True); images_seen.add(value); count+=1; maps+=1; products+=checks + predicted={A.F.power(c,image_index(A.F.p,q,heights)) for c in range(1,q)} + require(images_seen==predicted,'complete automorphism image') + expected={(4,(2,)):48,(4,(1,1)):2880,(2,(1,2)):2048}[(q,heights)] + require(count==expected,'complete substitution census') + complete[str((q,heights))]=count; contexts.append((q,heights)) + for q,heights in [(2,(1,1,1)),(3,(1,)),(3,(1,1)),(3,(1,1,1)),(5,(1,)),(5,(1,1)),(7,(1,)),(7,(1,1)),(4,(1,2))]: + A=Algebra(q,heights); images_seen=set(); candidates=[] + for i in range(A.r): + for c in range(1,q): + images=list(A.variables); images[i]=A.scaled(c,images[i]); candidates.append(images) + for j in range(A.r): + if i!=j and heights[j]<=heights[i]: + for c in range(1,q): + images=list(A.variables); images[i]=A.add(images[i],A.scaled(c,images[j])); candidates.append(images) + nonlinear=[] + for k,m in enumerate(A.monomials): + if sum(m)<2: continue + v=tuple(int(j==k) for j in range(A.N)) + if A.power(v,A.cutoffs[i])==A.zero: nonlinear.append(v) + for v in nonlinear[:3]: + images=list(A.variables); images[i]=A.add(images[i],v); candidates.append(images) + for images in candidates: + value,checks=verify_map(A,images,A.N<=9); images_seen.add(value); maps+=1; products+=checks + h=image_index(A.F.p,q,heights) + predicted={A.F.power(c,h) for c in range(1,q)} + # Independent diagonal scales attain the entire product subgroup. + attained={1} + for i in range(A.r): + values={A.F.power(c,A.N*(A.cutoffs[i]-1)//2) for c in range(1,q)} + attained={A.F.mul(x,y) for x in attained for y in values} + require(attained==predicted and images_seen<=predicted,'predicted determinant subgroup') + contexts.append((q,heights)) + triples=0 + for q,heights in contexts: + A=Algebra(q,heights); F=A.F; h=image_index(F.p,q,heights) + selected=[] + if A.N<=4: + selected=[v for v in product(range(q),repeat=A.N) if v[0]] + else: + for c in range(1,q): + for j in range(A.N): + v=[0]*A.N; v[0]=c + if j: v[j]=1 + selected.append(tuple(v)) + for u in selected: + columns=[A.mul(u,tuple(int(i==j) for i in range(A.N))) for j in range(A.N)] + require(F.det(list(zip(*columns)))==F.power(u[0],A.N),'unit determinant'); units+=1 + zs={F.power(c,h) for c in range(1,q)} + actual={(F.inv(F.mul(x,z)),F.inv(F.mul(y,z)),F.mul(F.mul(x,y),z)) + for x,y,z in product(range(1,q),range(1,q),zs)} + predicted={(u,v,w) for u,v,w in product(range(1,q),repeat=3) + if F.power(F.mul(F.mul(u,v),w),(q-1)//h)==1} + require(actual==predicted and len(actual)==(q-1)**3//h,'covariant determinant image'); triples+=len(actual) + A=Algebra(4,(1,2)); bad=list(A.variables); bad[0]=A.add(bad[0],bad[1]) + require(A.power(bad[0],2)!=A.zero,'forbidden height mixing'); controls+=1 + require(image_index(2,4,(2,))==3 and image_index(2,4,(1,1))==1,'height-sensitive image'); controls+=1 + F=Field(7); require(F.power(4,2)!=1 and F.power(F.mul(F.mul(4,1),2),2)==1,'inverse input convention'); controls+=1 + for p in (2,3,5,7): + for q in (p,p*p,p**3): + for heights in ((1,),(2,),(1,2),(2,3),(3,3)): + N=p**sum(heights); expected=q-1 + for e in heights: expected=gcd(expected,N*(p**e-1)//2) + require(image_index(p,q,heights)==expected,'modular exponent extraction'); controls+=1 + require(image_index(2,4,(10**100+1,10**90+2))==1,'large binary-encoded heights'); controls+=1 + print('PASS_FROBENIUS_TENSOR_CHARACTERS '+json.dumps(dict(contexts=len(contexts), + substitution_maps=maps,basis_product_checks=products,unit_maps=units, + determinant_triples=triples,controls=controls,complete_automorphism_domains=complete),sort_keys=True)) + + +if __name__=='__main__': main()