Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
80 lines (63 loc) · 5.26 KB

AFFIRMATION.adoc

File metadata and controls

80 lines (63 loc) · 5.26 KB
Raw

AFFIRMATION — trope-checker

A dated, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION trio). This is the brief’s "STATUS" deliverable: what is proved, what is stubbed-and-named, what is deferred — stated plainly, verified by running the tools, never overclaimed.

As of 2026-06-22

Ground truth (commands actually run):

  • bash tests/conformance/run.sh → all 8 schema-invalid fixtures rejected by the Idris decoder at the named coordinate; the JSON Schema is the published contract.

  • just trope-build && bash tests/conformance/run.sh → 10/10 conformance cases pass; verdicts and witness edges match.

  • idris2 --typecheck verification/proofs/idris2/trope.ipkg → exit 0, six modules.

Proved, machine-checked, no axioms (see docs/status/PROOF-STATUS.adoc): L1 (associativity of ▷) and L2 (unit) on the full grade; decidability of ⊑; the Veridicality Derivation (exactly three deceptive duals); the Honest Generation Theorem (five atoms generate the honest fragment). No believe_me / assert_total / postulate anywhere.

Soundness advance (2026-06-22): the verdict-soundness corollary, T-Sub soundness, ⊑-preorder, and grade soundness for EXACT faithful lowering are now machine-checked (Trope.Order/Trope.Soundness); a machine-checked FINDING shows strict L4 fails for fate (Predicated ⊥ Dropped) so it is lax. Stubbed-and-named, NOT asserted: grade soundness for conservative lowering over fate + the term-language/fix operational model — the remaining open problem; L4/L5 as standalone lemmas; O1 exhaustiveness. Deferred: Haec compiler, Rust fast-core, the adjunction (O3), the fidelity-carrier question (O4).

Honest scope statement: the checker is sound, not complete; its guarantee is relative to faithful lowering (a front-end’s per-construct obligation, calculus O2); and veridicality is declared-and-propagated, not checked (calculus O5). The deploy variant is prevent (deception = validation-boundary fault, R-2026-06-22).

As of 2026-06-24 — grade-boundary ground truth + Theorem B

Ground truth (commands actually run):

  • just build-lean (≡ lake build in verification/proofs/lean4/grade-boundary/) → exit 0; axiom audit reports propext/Quot.sound only — no sorryAx, no user axiom, no native_decide.

  • just build-agda (≡ agda --safe --without-K All.agda + Smoke.agda in verification/proofs/agda/theorem-b/) → exit 0; zero postulate/sorry/TERMINATING/trustMe.

Proved, machine-checked: the grade-algebra honest/deceptive cancellation boundary — the non-commutative product monoid, full-carrier conicality, and the three-tier strict cancellation boundary (cancellation only on the finite-fidelity core) — in Lean; and over it, Theorem B’s intrinsic graded calculus, grade-exact value substitution, β/let subject reduction, and Honest Generation, in Agda. Two recorded results: symmetric cut is impossible (F2); tier-preservation is closure, not a homomorphism (F2×F4).

Stubbed-and-named, NOT asserted (the honest gap, stated plainly): Theorem B Target 3 is PARTIAL — fix/lfp subject reduction is NOT-REACHED and not postulated. There is no full subject reduction and no operational model for the calculus’s fix/routing dynamics; this is the central open problem (CO-1), gated by v0.1’s O4 (the limit carrier). The grade algebra itself is not at fault.

As of 2026-06-29 — tropical factorisation probe (a precondition, nothing more)

Ground truth (commands actually run): just build-lean → exit 0 over both verification/proofs/lean4/grade-boundary/ and verification/proofs/lean4/grade-factorisation/; the latter’s axiom audit reports propext/Quot.sound only (four theorems depend on no axioms) — no sorryAx, no user axiom, no native-evaluator decide. just falsify (in the subproject) PASS.

Proved, machine-checked: a nontrivial monoid homomorphism π : Grade → Δ onto the commutative tropical fidelity carrier exists (verdict (B) FACTORS but VERIDICALITY-BLIND), but every multiplicative map from Fate — and from Grade — into any commutative monoid is forced to identify the honest dropped with the deceptive falsified (forced_collapse_general, forced_collapse_grade). The blindness is co-located with the fate-axis non-commutativity; the commutative Bond/Merge deceptions remain tropically separable (psiBond_*).

NOT claimed (the honest boundary, stated plainly): this is a necessary-not-sufficient precondition. It does not solve, handle, or address recursion. Whether a fixpoint’s grade actually lives in the commutative part needs the operational model CO-1 and stays parked behind it (and O4). The probe can only narrow or fail to kill the tropical route; it cannot confirm it. Documentation gaps OPEN-B/B′ (Falsified/Misbound absent from v0.1 §3.1/§3.2) and OPEN-C (Withheld/Fused tier-2 membership not individually witnessed) are recorded, not filled. Full proved-vs-missing picture: verification/proofs/INTEGRATION-REPORT.adoc.

— Authored by the build agent under owner direction; signed in git history.