# Axiom and placeholder audit

## Active-source audit

`scripts/check_no_placeholders.py` removes nested block comments, line comments, strings, and character literals before checking executable source for:

- `sorry` or `admit`;
- top-level `axiom` declarations;
- top-level `constant` declarations that would introduce an assumption.

The packaged source has count zero in all categories. The machine-readable result is `notes/source-audit.json`.

## Kernel dependency report

`Erdos870/MainTheorem.lean` and `Erdos870/Main.lean` contain `#print axioms` commands for the core and public final declarations. The GitHub Actions workflow builds the project, re-elaborates `Main.lean`, and checks the output with `scripts/check_axioms.py`.

The accepted dependency boundary is:

```text
[propext, Classical.choice, Quot.sound]
```

These are standard Lean principles used through Mathlib. No `sorryAx` and no project-specific mathematical axiom is accepted.

## Verification boundary

The repository package was checked for source-level placeholders, local import resolution, file integrity, paper/source correspondence, and metadata consistency. A full Lean build was not available in the packaging sandbox. The first green GitHub Actions run is therefore the reproducible public kernel check under the pinned toolchain and Mathlib revision.

## Historical comments

The large construction files retain some comments describing retired proof routes and earlier development boundaries. Comments are not declarations and are ignored by the static audit. The clean build and `#print axioms` output determine the trusted theorem status.