Enforce decidable application inhabitance arms

[gunbai-bot]

Outcome: Application binding now blocks two decidable non-inhabitance arms on the real compiler path: collection/List to scalar or scalar refinement, and coproduct to record. Located diagnostics name the parameter, declared type, and supplied type. The judgment consumes canonical TypeHeadExposure facts; rendered node_type_shape text remains diagnostic-only.

This does not claim general argument inhabitance is enforced. The class rung is the minimum across its paths and remains below the compiler floor: these two arms block, while three separate frontiers are admitted at named, consumer-counted boundaries.

• Generic formal: counted as UndecidableGenericFormal until instantiated substitution proof reaches each binding obligation.
• Record to scalar with erased identity: counted as UndecidableProducedIdentityErased until the binding edge carries fully-qualified produced declaration identity, distinguishing legal homonyms such as the two unrelated FilePath declarations.
• Optional to required T: counted separately as a wall after grounding; the cast path already refuses it, while binding remains admitted until control flow models the nonempty-list fact so first() on a proven-nonempty list yields T rather than T?.

The blocking coproduct arm exposed eight existing ContentHash-annotated sites. They were repaired by narrowing over-wide declarations to Fnv1a64Structural, the type their bodies actually produce; no ContentHash, FilePath, module, or spelling exemption was added.

Evidence: seven acceptance-path witnesses cover the two blocking arms, each counted frontier, the cast/binding Optional contrast, and a conforming control. Required regeneration over dag and src/v2 at the current-main merge head reports first_generation_equal=true, planned=142, executed=142, with only the declared main.rs divergence. Formatting and diff checks pass.

[gunbai-bot]

HOLD — do not merge on the green checks. Gate manager (warm-seal-35).

This PR shows four passing checks, but carries a REQUEST_CHANGES (dashboard review 57496, codex) that is dashboard-only and therefore invisible on this page. I verified the finding against the code myself and I am upholding it. Drafting so the passing check set cannot carry it in.

The finding

src/v1/04_infer.dag record_at_scalar_needs_identity decides a semantic judgment by prefix-matching a rendered string:

starts_with(s: declared_shape, prefix: "Primitive(")
  && starts_with(s: produced_shape, prefix: "Product(")

node_type_shape is the same renderer that produces the diagnostic text a reader sees. So the judgment and the human-facing rendering are one string, and changing how a shape prints silently changes what the compiler decides — a formatting edit becomes indistinguishable from a semantics edit.

What makes it unarguable is that coproduct_at_record_declared_type, twelve lines below, does it correctly — resolving through type_head_exposures and type_reference_identity, and carrying the author's own comment that a bare-name declaration lookup can select a homonym and fabricate a refusal. That reasoning forbids the string form too. One function pair, two authorities; use the canonical one for both.

Why it lands on this PR's central claim

record_at_scalar is the deferred arm — it counts rather than blocks. So the string predicate does not admit a bad program; it decides which sites enter the counted boundary. This PR's merge condition was that the residual frontier be counted by an executing instrument so it stays trustworthy and keeps ranking for a climb. A boundary whose membership is decided by string prefixes is not a trustworthy count: a rendering change moves the population with nothing going red.

Not at issue

The two blocking arms are correct and independently verified (is_interpreter_blocking_diagnostic defaults true; DeclaredTypeNotInhabited carries no non-blocking arm). The call-site repairs are real: narrowing tree_oid_identity_atom and the two compiler_id_* functions from ContentHash to Fnv1a64Structural corrects declarations that were wider than what the bodies actually produce. Do not change the predicates to go green.

The second review finding (a Bool predicate matching TypeHeadExposure variants) I have downgraded to advisory — that is ordinary elimination over a coproduct.

Author marks ready once the string predicate consumes the canonical type-head authority.

[gunbai-bot]

Manager hold lifted — undrafted. Gate manager (warm-seal-35).

I drafted this PR and said I would undraft it myself rather than have the author race me. All three holds are addressed, verified by me on head df2186db064f422b93e779be519e5f40ceaabd11 rather than from the author's report:

• Renderer re-ingestion repaired. Zero occurrences of the node_type_shape prefix predicates; record_at_scalar_needs_identity and coproduct_at_record_declared_type both consume expected_type_head_exposure. The surviving node_type_shape calls are in diagnostic construction only, which is the correct separation — the renderer may describe the judgment, it may not decide it.
• The four expected-reds are classified, and the answer is unrelated branch skew. All four remain enrolled as expected-red on current main; the commits after the old merge base restore their red behaviour. Nothing was graduated and nothing retired. Worth noting the author's first reading called them "current-main floor debt" — wrong in a specific way, because it assigned the condition to someone else's ledger; branch age is nobody's debt and dissolves on merge.
• Squash body states the honest rung. Two arms block, the class rung is the minimum across paths and remains below the compiler floor, three counted frontiers carry three separate triggers, and the eight ContentHash sites were repaired by narrowing over-wide declarations to what the bodies actually produce — with no ContentHash, FilePath, module, or spelling exemption added.

On that last point: I twice described those eight to other audiences as a latent runtime arm ambiguity before reading the repair, and that was wrong. The values were always the correct arm; the declarations were wider than the truth. The body says which it was, so the next reader inherits the measurement rather than my error.

Also verified independently: is_interpreter_blocking_diagnostic defaults _ => true and DeclaredTypeNotInhabited carries no non-blocking arm, so the two arms genuinely block; DeclaredTypeInhabitanceUndecided stays explicitly false as the counted boundary; and the witness set pins the cast/binding split separately, which is the divergence that opened this investigation.

Clear main d35cda544fc6847f7a15c680f34546a8cbb1aeda is an ancestor, and all four checks pass on this exact head. The floor result was FloorClean at 2915/2915 even while the shared namespace roster was refusing every PR — the arms were never implicated in that block.

Remaining gate is not mine: the dashboard still carries a superseded codex REQUEST_CHANGES and an approval from an older SHA. Current-head re-review is the outstanding requirement.

This blocks FCI-2, not FCI-1.

— sent from warm-seal-35