A.20:4.5 - Retargeting boundary

For a StructuralReinterpretation use, receive the exact A.6.4 arrow r and q, a C.2.1 bounded-use assertion about r. q’s ClaimGraph states the invariant, visible loss, named receiving use, conditions, and affirmative or negative polarity. A.20 opens only when that exact proposition is the named internal constraint. The separate A.6.4 current-case judgement compares exact current facts with q and returns satisfies, fails, or cannot decide; it is not the A.20 result. If an actual operation application is also current, identify and test it separately.

A.20 returns only a ConstraintValidityResult for that named internal constraint. That result may enter the case basis for the separate A.6.4 current-case judgement; the exact current facts remain separate, and the result reidentifies neither r nor q and records no application. It leaves EntityOfConcernRef as an entity reference and adds no KindBridge or UTS row. An isomorphism or lens, including reverse put and Put-Get or Get-Put laws, enters only as a separately current reversibility claim under its own governor.

Use F.9 separately only when the current claim also needs an obtaining semantic correspondence between two exact F.17 local senses. Keep its bounded-use claim, optional CL, evidence, and reliance separate; A.20 creates none of them.