Spec v0.2 review findings deferred to the owner (L3, L6, C2, detect profile, O1-carrier citation) #106

Bot review of PR #102 (Phase 0: make the status surfaces true) raised findings that ask for changes to normative content of spec/calculus.adoc v0.2. The Phase 0 brief forbids that pass from editing spec rules, the carrier, ADR decisions or proof statements, so each was answered "deferred to the owner" on its thread and left unresolved. This issue collects them so they do not get lost in the PR.

Each item needs an owner ruling; several would be an ADR 0006 and a carrier/proof migration if accepted.

1. L3 and the fate rule Attenuated(⊤) ▷ Dropped = Dropped (CodeRabbit)

Thread: #102 (comment)
L3 says no honest absorber launders deception; the fate table lets honest Dropped absorb Attenuated(⊤), whose fidelity Unknown L3/C3 classify as deceptive. Current reading implemented by the proofs: Unknown is a two-sided zero within fidelity (TB.Grade.unknown-absorbL), and on the fate chain Attenuated(⊤) sits above Dropped, so the rule is the chain meet. Decision: exclude Attenuated(⊤) from Dropped's absorption, or state the exception in L3/L5.

2. L3 lists fidelity Unknown among the deceptive bottoms (Codex, opposite direction to 1)

Thread: #102 (comment)
attenuate[⊤] is writable and schema-accepted; TB.Honest.movesHonestFate (Attenuate d) treats every attenuation, unknown included, as honest; §7 calls ⊤ an honest answer; only Falsified/Misbound/Conflated are the three deceptive duals. Decision: is Unknown deceptive (L3/C3 as written) or honest-but-unbounded (executable semantics)? Items 1 and 2 are the same question from two sides.

3. L6 (commutativity) on labelled grades (CodeRabbit + Codex)

Threads: #102 (comment) , #102 (comment)
Predicated(P) ▷ Predicated(Q) = Predicated(Q) and Fused(τ₁ ⊗ τ₂) are order-sensitive in their labels; the three proofs (GradeR.instCommMonoid, FateA.comp_comm, grade-comm) are on the label-erased carrier (PROOF-STATUS "Modelling notes"). Decision: (a) state the quotient in L6, (b) make label composition commutative, or (c) demote L6.

4. C2 (cancellation boundary) stated over the unnormalised carrier (Codex)

Thread: #102 (comment)
C2 cites GradeR.gradeR_leftCancel_iff ("left-cancellative iff ε"), a theorem about the unquotiented datatype whose counterexample distinguishes Present from Attenuated(Q 0); A3 removes that value at ingest and FateA.atten_cancel_on_normalForms shows finite attenuation is cancellative on normal forms. Decision: state C2 over the normalised carrier (and what split/rejoin designs that admits).

5. Detect profile for every deceptive dual (Codex)

Thread: #102 (comment)
§9's normative variant was renamed from conflation to deception but still admits only Conflated as writable; spec/trope-ir.adoc says deceptive grades are representable in the detect profile. Decision: add the Falsified/Misbound rules and validation behaviour, or keep the variant explicitly conflation-only.

6. O1-carrier is cited for the ratified carrier but proved on the v0.1 Grade (Codex)

Thread: #102 (comment)
EffectAtoms.lean imports GradeBoundary; there is no GradeR.atom_factorization. The status docs on PR #102 now say so (PROOF-STATUS row + Open item "O1-carrier on GradeR", AFFIRMATION finding 4). The spec's §6/§10 wording ("RESOLVED", cited as ratified-carrier) is the owner's. The port is expected to be mechanical (the factorisation is componentwise) and would close the item outright.