FPRD LabShare an approach

← Claims

Theorem · conditional quotient transfer

FPRD-LT-T02

Target-isolating poDFA quotients suffice

Exact statement

Let M=⟨S⟩M=\langle S\rangle and let f:Q→Qf:Q\to Q be the target. A polynomial-time computable poDFA action ρ:Mop→TP\rho:M^{\mathrm{op}}\to T_P and code tf∈TPt_f\in T_P suffice for the conditional NP transfer when, for every g∈Mg\in M, ρ(g)=tf\rho(g)=t_f if and only if g=fg=f; full faithfulness of ρ\rho is unnecessary.

StatusProved conditionally; a uniform compact target-isolating construction remains open
External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

Membership asks whether one target is generated, so a quotient need not distinguish pairs of non-target monoid elements.

Hypotheses and scope

  • The restriction of ρ\rho to MM is a homomorphism and its generator images form a polynomial-size poDFA action.
  • For every g∈Mg\in M, the exact target-code condition ρ(g)=tf⟺g=f\rho(g)=t_f\Longleftrightarrow g=f holds; if f∉Mf\notin M, the fibre is empty.
  • The observation is produced by a uniform polynomial-time construction whose fibre property is established mathematically.

Proof or evidence

Image membership is equivalent to original target membership by the exact target-code condition. Ryzhikov and Wolf's Proposition 9 shortens an image word to length at most |P|(|P|+1)/2, and word reversal transfers it from the opposite monoid back to M.

Target-fibre theorem and proof →

Verification notes

The proof was checked in both directions, including targets outside M. The revised statement never writes rho(f) unless f is known to be in the domain, and the construction requirement remains separate from merely guessing an image action.

Limitations

  • This theorem does not construct the required observation and does not settle NP versus PSPACE-hardness.
  • Efficient verification of an arbitrarily guessed fibre condition is not claimed.

Open work

Construct target-isolating poDFA observations directly from the supplied L-trivial action, beginning with fixed alphabets and principal-left-ideal features.