C.2.3:14 - Assigning F in Practice

C.2.3:14.1 - First-pass questions

1. Can a competent reader misread the claim materially? If yes, the expression is likely at F0-F2; if not, it may be F3 or above.
2. Are the critical claims visible as explicit predicates or invariants? If yes, the expression is at least F4.
3. Does the expression have declared executable semantics? If yes, it is likely in the F5-F6 region.
4. Are proofs of the core claims checked by a logic kernel or a dependent type checker? If yes, the expression is likely F7-F8, or F9 if higher-equality machinery is essential.

C.2.3:14.2 - Quick rubric

• No full structure -> F0-F1
• Full structure but mostly placeholder criteria -> F2
• Controlled prose with one stable reading -> F3
• Explicit predicates / invariants -> F4
• Declared executable semantics -> F5
• Hybrid / layered formal obligations -> F6
• Machine-checked proof core -> F7
• Dependent proof-carrying core -> F8
• Higher-equality foundations are essential -> F9

C.2.3:14.3 - Typical delta-F moves

• F2 -> F3: replace loose prose with controlled phrasing and explicit acceptance statements.
• F3 -> F4: recast acceptance into typed predicates or invariants.
• F4 -> F5: give the expression declared executable semantics.
• F5 -> F6: make multi-layer obligations explicit.
• F6 -> F7/F8: move critical claims into machine-checked proof or dependent-type form.