Analyze current identity at authorization calls

Prove that the configured authorization identity fields match one successfully checked provider call in the same local statement sequence. Seed identity origins only at an exact approved provider CALL. Require a complete success condition and a branch that exits for every non-success result. Support explicit level 88 conditions with bounded Boolean logic and existing terminal rejection paths. Preserve pending or checked provider evidence across an independent read-only rejection whose rejected path terminates. This does not grant provider success. Propagate complete equal-width PIC X copies through at most 64 intervening statements and 64 stored origins. After provider success, complete terminal equality checks can establish exact current values for at most eight configured pairs under native character comparisons. Evaluate up to 256 equality combinations with bounded Boolean conditions. Never grant evidence when no combination continues. Equality establishes current values without changing their historical origins or proving saved-data freshness. Preserve proof across disjoint plain scalar MOVEs, validated default initialization, no-ops and literal messages. Writes to provider storage, unknown effects, other calls and unsupported branches invalidate it. A later provider call needs its own success check. Require complete ordinary source and unaliased local DISPLAY record layouts. Alternate ENTRY and NEXT SENTENCE prevent the proof. Report missing identity mappings without changing code or treating unknown origins as trusted. A positive result proves only the supplied current identity mapping at that call. It does not prove provider authentication internals, resource authorization, action or key mapping, authorization-response handling, later protected use or validity across tasks.