Add Commander-governed proof-producing congruence

[FreshSoftware4]

Purpose

Advance the execution-coherence rail from the native constraint core to proof-producing congruence. Equality is authority only when represented by a checked judgment, an attached witness, and a reconstructible provenance path.

Completed Commander chain

LOCUS64_PROOF_CONGRUENCE_CHANGE_CHAIN.athens is complete:

1. equality judgment
2. primitive equality witness
3. congruence lifting
4. evidence-path validation
5. canonical representative selection
6. forged-merge rejection and closure

The parent rail has advanced:

proof-producing-congruence  complete
incremental-closure         current
native-upper-projection     next

Native capability

• native TypeEquality judgments with deterministically attached EqualityWitness evidence
• checked reflexivity, exact structural equality, symmetry, and transitivity
• congruence lifting through type constructors and executable operations
• every premise references an earlier equality judgment carrying its own checked witness
• context-scoped proof visibility
• deterministic equality provenance paths
• route-minimal canonical representatives derived from the validated component
• no persisted equivalence class, representative cache, merge table, or union-find authority
• decoder-side re-execution rejects forged rules, missing witnesses, scope escape, and substituted congruence premises
• equality-bearing L64R1 -> L64D -> L64R1 -> L64D fixed point

Burden control

No public authority struct or enum was added. The surface remains at 10 public structs and 7 public enums. The implementation reuses the existing graph, port, route, journal, codec, RNA, and transactional machinery.

The native workflow now supports both main-target and stacked chatgpt/** pull requests through one inspectable PR gate; CLI paths are included in the watched surface.

Verification

Local isolated verification passed:

• 41 native tests
• formatting
• strict native-core Clippy
• recursive forbidden-ontology scan
• Commander containment audit

GitHub run 29997465633 passed on final head 8538461f25b1fba94408d43001204595fc495616:

• formatting
• complete workspace tests
• strict native-core Clippy
• native CLI equality proof fixed point

Remaining rail

The current stage is incremental dependency closure: reverse dependencies, exact invalidation, affected-scope recomputation, and local/global closure. It is followed by native upper projections and legacy authority quarantine.