# Core 8.3 — source and proof correspondence

## Input contract

`Model Z A` has finite safe and goal sets, `goal ⊆ safe`, finite running and ending action catalogues at each observed state, and the actual finite successor set for each state/action pair. Every enabled action has at least one successor. The source-facing theorem assumes `Fintype Z`; the action universe need not be globally finite because each supplied catalogue already is finite. Empty state types remain admissible. An empty action catalogue is a real deadlock.

`endStep` is precisely `U ∪ {x ∈ safe | ∃ a ∈ finish x, post x a ⊆ U}`. `endStage` starts at the goal. `runStep` is precisely `{x ∈ U | ∃ a ∈ run x, post x a ⊆ U}`. `runStage` starts at the computed ending region. These are definitions on the supplied system, not hypotheses that a winning region exists.

## Fixed points and ranks

`FiniteFixedPoints.increasing_stabilization` proves an inflationary finite-set sequence becomes fixed within the number of initially missing states. `decreasing_stabilization` bounds a deflationary sequence by the size of its initial set. The proof uses strict cardinality changes, not a timeout or an experimentally observed convergence. `fixed_tail` proves permanence of a fixed point.

`ending_stabilizes` and `running_stabilizes` instantiate these results. `endRank` is the least stage containing a state in the ending region. The outside value zero is never used as a certificate of ending. `endRank_spec`, `endRank_min`, and `endRank_zero_iff` prove the first-entry meaning. `rank_action` produces one action whose every successor has smaller rank.

## Policy semantics

A `Config` consists of the previous state/action pairs and the current observed state. A `Strategy` maps that configuration to an optional action. `edge` requires the selected action to be in the actual catalogue, the next history to include that same selected action, and the next state to belong to the supplied successor set. The action is selected before the adversarial successor.

`EndingGuarantee` requires safety and a legal action at every reachable non-goal prefix and excludes an infinite legal non-goal execution. Neither requirement alone is enough. The deadlock example has no infinite execution, but fails the local legal-action obligation. `ending_prefix_extends` uses nonempty successor sets to show every non-goal winning prefix really can advance.

`PolicyInput` has a running branch and an ending branch with the configuration at the command epoch and the complete subsequent history. One policy function receives this input before it selects its next action. `SwitchingGuarantee` requires safe legal running at every no-command prefix and the ending guarantee after a command at any such prefix. Therefore the necessary direction includes arbitrary history-dependent policies, not only memoryless policies. The authentication and delivery of a real-world command are not proved by this formal input type.

## Necessity and sufficiency

For sufficiency, the ending action is selected from the rank-decreasing witness and the running action from the viability fixed point. Every legal ending step decreases rank, every running step stays in the running region, and every reachable command epoch remains inside the ending region. `running_has_infinite_path` constructs actual no-command execution, excluding vacuous success.

For necessity outside the ending region, `outside_successor` produces a successor still outside after the strategy has selected its action. Starting from a presumed history-dependent winning strategy, `guarantee_mem_ending` recursively constructs a legal infinite non-ending path. Its contradiction proves ending-region membership without imposing a time bound on arbitrary winning policies.

For necessity in the running phase, the set of states occurring in histories reachable under the given policy is contained in the ending region. It has at least one running action whose entire successor set remains in that reachable set. `running_maximal` places it in the actual decreasing fixed point. No action is chosen after observing its successor.

`safe_continuation_iff` is the exact region/one-policy equivalence. `source_core83` packages that equivalence together with the same constructed policy's universal rank budget. `command_rank_arrival` gives the first-entry-rank arrival statement at every reachable command epoch. These proofs do not assume the desired region/policy equivalence as a field.

## First arrival and the manuscript hold action

The source permits a safe hold action at the goal. This development stops the ending specification at first goal arrival and does not need that additional premise. It therefore applies to the source setting and also to settings without post-goal continuation. It does not establish arbitrary post-goal safety. The printed manuscript is unchanged, and this difference is a recorded strengthening rather than a silently omitted assumption.

## Checked examples

A three-state system has goal 0, stop-capable state 1, and safely idling trap 2. Its ending region is `{0,1}` and its running region is `{0}`. State 1 can stop immediately but loses that option by running once; state 2 can run indefinitely but cannot end. A separate system shows deadlock is neither successful running nor successful ending. A Boolean quantifier example detects hindsight-dependent selection. Finally, a history-dependent policy waits once and then ends although the state's minimum rank is one. The rank bound belongs to the constructed policy, not to every winning policy.

## Admission and exclusions

Current-source final/fresh gates, source API checks, complete project axiom audits, own-kernel replays, all 161 control contracts, upstream object hashes, and byte-identical production objects determine admission. No proof placeholder, custom production axiom, or native-decision proof shortcut is introduced. The three earlier unformalized targets remain pending. The monograph's wider integration chapters and the Large Signal Model denominator are not enlarged by this result.