Pedagogical Style Guide

Purpose

Grand Challenge pedagogy is not simplification. It is structural revelation and mathematical control.

The current programme-wide standard is the Grand Challenge Pedagogy Standard. This style guide is the sentence- and artifact-level companion to that standard. The binding campaign pattern is the Chaidez Pedagogical Protocol, and foundation sensitivity is governed by the Foundation-Aware MATH-PROGRAMME Doctrine.

The goal is to let a serious reader see what the object is, why it resists proof, which claims are supported, where the proof debt sits, what foundation profile is being used, and what exact action should happen next.

Current Grand Challenge additions

Every new page, Work Package, fixture, route doctrine, or reader-facing visual must now satisfy the rails-before-research standard:

• status before suspense;
• object before method;
• obstruction before optimism;
• claim ledger before persuasion;
• fixture before expansion;
• resource budget before expensive computation;
• semantic bridge before formalization claims;
• foundational profile before ambiguous existence claims;
• certification route before promotion;
• visual or mnemonic aid only when it teaches structure.

The author must quarantine imported corpus status, external classifications, generated traces, provider rankings, and source metadata until independent reconstruction has occurred.

The reader should always be able to tell whether a statement is exploratory, audited, exactly computed, certificate-replayed, formally proved, rejected, superseded, or still open.

Voice

Use a voice that is:

• lucid;
• exact;
• generous to the reader;
• severe with unsupported claims;
• comfortable with partial and negative results;
• explicit about proof debt;
• allergic to performance.

Avoid marketing, mysticism, vague difficulty claims, and victory language before certification.

Start with status

Every serious artifact begins with a compact result-status box:

• result status;
• conditional hypotheses;
• strongest supported claim;
• claims explicitly not made;
• computation or support-route class;
• foundational profile status;
• certification state;
• first executable step.

The reader should not need to infer whether the headline is proved, conditional, computational, open, certificate-replayed, or formally checked.

The nine-move exposition pattern

1. Status box

Say whether the artifact is exploratory, audited, computed, locally proved, certificate-replayed, formally checked, rejected, or superseded.

2. Plain object

Begin with the object in ordinary mathematical language. Do not begin with machinery unless the machinery is the object.

Answer:

What are we actually trying to understand?

3. Exact obstruction

Give a small calculation, toy model, counterexample, or failed mechanism that shows why the naive route breaks.

Answer:

What specifically prevents the obvious argument from working?

4. Working model

Give an example, picture, finite enumeration, or local model. The reader should be able to touch the object before encountering the full abstraction.

5. Restricted claim

State the strongest claim the package is actually equipped to investigate. Name every condition. Do not let the programme-wide conjecture stand in for the local target.

6. Theorem-spine location

Introduce definitions, propositions, lemmas, and exact hypotheses. Every item must state its role in the global theorem spine and its dependencies.

A lemma without a role is a loose gear. A theorem list without a dependency graph is not a campaign.

7. Support route

Present the mathematical action. Classify each support route as exploratory evidence, regression audit, exact finite verification, certificate replay, formal proof, continuum proof, or negative result.

CAS output is not certification. A Lean statement with sorry is not a proof. A visualization is not mathematical evidence unless the evidence itself is separately replayable.

8. Debt and claim boundary

Separate:

• what is proved;
• what is checked;
• what remains open;
• what was imported but not audited;
• what requires external verification.

Link unresolved steps to the proof-debt register and state what would discharge them.

9. First executable step

End with one bounded action with named input, output, and completion test. "Continue research" is not an executable step.

Required explanatory moves

A serious Work Package must explain:

• why this definition is the right definition;
• what examples it admits and excludes;
• what invariant is being preserved;
• where naive approaches fail;
• which spine node the package advances;
• which dependencies are consumed;
• which finite computations are checks rather than proof;
• which proof debt is created or discharged;
• what formalization would require;
• what semantic bridge connects the human claim to the formal or computational claim;
• what foundational profile the object carries;
• what would change the claim status;
• why the next step is the correct local move.

Negative-result discipline

Negative results teach when they identify an exact obstruction. Record:

1. the attempted route;
2. why it was plausible;
3. the smallest exact failure;
4. what the failure rules out;
5. what it leaves viable;
6. the next restricted problem.

Do not conclude only that an approach failed.

Decorative and mnemonic discipline

Decoration is welcome when it teaches. Diagrams, tables, callouts, analogies, character roles, app-like layouts, and names are useful if they compress structure.

Decoration is harmful when it hides uncertainty or substitutes atmosphere for content.

Use ornament as a lantern, not a curtain.

Mnemonic devices such as the Minderlings are reader aids. They may help a reader remember who discovers, who organizes, who certifies, who maps, who stewards, and who keeps fixtures stable. They do not create mathematical authority.

Sentence-level guidance

Prefer:

This computation is an exact finite verification for families of size at most 4. It does not establish the unrestricted claim.

Avoid:

This computation provides strong evidence for the conjecture.

Prefer:

The obstruction is not enumeration; it is the lack of a monotone quantity that survives arbitrary unions.

Avoid:

The problem is challenging and important.

Prefer:

This lemma discharges debt item PD-07 by converting the singleton argument into an injective counting statement.

Avoid:

We prove a useful lemma.

Prefer:

The dataset marks this problem as unknown; the programme records that as imported metadata until the source status is independently reconstructed.

Avoid:

The dataset shows that this is an open problem.

Final paragraph test

The final paragraph of every Work Package must answer:

1. What did we clarify?
2. What remains unproved?
3. What proof debt blocks the next spine node?
4. What foundation or semantic bridge remains unresolved?
5. What is the first executable step?
6. What would promote the strongest claim in the ledger?