printExamples
plain-language theorem explainer
This definition emits a boxed header and two sentences describing a toy-model witness for the CPM standalone certificate. Users of the audit CLI cite it to confirm that the A/B/C assumptions remain consistent and usable within the model. The body is a direct sequence of IO.println calls that produce console output without invoking any verification predicates or performing calculations.
Claim. The procedure outputs a boxed header labeled Example Witness followed by text asserting that the CPM standalone certificate contains a toy-model witness confirming consistency and usability of the A/B/C assumptions.
background
The CPM audit module supplies a command-line interface that prints verified constants, consistency checks, and probability bounds. It depends on the model construction that assembles a Model from a Hypothesis bundle containing defectMass, orthoMass, energyGap, and tests. Consistency is expressed by the predicate requiring an assignment that satisfies both a CNF formula and an XORSystem. The active edge count A equals 1 in the IntegrationGap, Masses.Anchor, and Modal.Actualization contexts, corresponding to the φ-power balance identity at D=3. The actualization operator maps each configuration to the minimal J-cost realization.
proof idea
The definition is a direct do-block containing eight IO.println statements. It prints the boxed header, two blank lines, and the two explanatory sentences about the toy-model witness and the A/B/C assumptions.
why it matters
This definition supplies the final output section called by the main entry point of the CPM audit CLI. It completes the sequence that also invokes printHeader, printConstants, printConsistency, and printProbability. Within the Recognition framework it supports explicit presentation of the standalone certificate, linking the model construction and the consistency predicate to the φ-ladder and J-cost minimization steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.