FINAL VERIFICATION REPORT
=========================
Date: 2026-09-01

1. Exact Python replay
----------------------
Authoritative command:
  uv run --frozen bash ./reproduce.sh
Locked environment:
  CPython 3.11.15; SymPy 1.14.0; transitive hashes in uv.lock

Normal Python and PYTHONOPTIMIZE=1 both verify:
  - the complete release-path/SHA-256 manifest;
  - 37 translation-normalized protected templates;
  - identical normalized catalogues for N=3,4,5,6;
  - 117 boundary-decorated signatures and 234 decorated/degree containments;
  - all 74 k=4,5 protected local certificates;
  - reconstructed velocity-node and one-sided source/output target-row order;
  - H*B=0, E*X=0, S*X=s_X*B, A*E=s_A*H*S;
  - literal K=H^T, B*D+H^T*R=s_0*I, D*B=s_0*I, R*B=0;
  - P*C=0 and T*C=s_C*B;
  - all 74 exact reference norm bounds through two separately implemented
    exact backends;
  - max C_ref^2=8121511/55 at configuration 21, k=5, hence C_ref<385;
  - the exact degree-four two-cube macro-patch certificate and independent
    symbolic macro-patch audit;
  - the captured Lean axiom report against a strict whitelist.

Independent-backend gates:
  - a coordinated corruption of the shared edge-star geometry constructor is
    accepted by the deliberately corrupted generator/primary-verifier pair and
    rejected by verify_all_edge_star_certificates_independent.py;
  - a coordinated non-maximal Gram corruption is accepted by the deliberately
    corrupted norm generator/primary-verifier pair and rejected by
    verify_all_edge_star_norm_bounds_independent.py.

Mutation/regeneration suite:
  28 tests pass in ordinary Python and the same 28 pass with Python optimization
  enabled.  Mutations of C, B, node_order, K/H^T, catalogue metadata, norm data,
  norm provenance, macro witness, manifest paths/hashes, manifest symlinks, and
  unreadable traversal are rejected.  Certificate JSON, norm JSON, both
  catalogue CSVs, generated Lean tables, and SHA256SUMS regenerate byte-for-byte.
  Every public verifier resolves release data with no positional arguments.
  No verification script contains a Python assert statement.

Primary exact-data hashes:
  all_edge_star_certificates.json
    f14caddc60c75542c2d426a0f871be2adf2a8dfd6f966317f40bdfd2958931f3
  all_edge_star_norm_bounds.json
    af169660100ffcb3b3981c199edf82b3137455f4376cd4c4206c5c1637a6327e
  p4_macro_patch_certificate.json
    5b4b8d0b386590f0e9a00f78a10d2d1629626109664175aa5928b6909e0c4aba

2. Lean 4 kernel build
----------------------
Project:
  lean/freudenthal_k4_edge_star_lean
Pinned toolchain:
  Lean 4.30.0; Mathlib tag v4.30.0
Commands:
  lake build
  lake exe edgeStarAudit
Result: EXIT 0

Build facts:
  - 8,487 Lean library jobs completed;
  - edgeStarAudit executable build completed through job 16,960;
  - 74 local records were checked by eight bounded decide +kernel chunks;
  - no native_decide, sorry, admit, project-declared axiom, unsafe/extern
    declaration, or native-decision trust axiom occurs;
  - edgeStarAudit reported 37 configurations, 74 certificates, 74 norm records,
    74 norm factorizations, 189 colours, raw overlap 19, and dependency depth 0.

Expanded AxiomCheck:
  - 18 named aggregate, strict-bound, assembly, colour, overlap, and product
    theorems were captured in AXIOM_REPORT.txt;
  - allowed dependencies are only propext, Classical.choice, and Quot.sound;
  - several finite arithmetic theorems depend on no axioms;
  - no sorryAx, Lean.ofReduceBool, or Lean.trustCompiler appears.

Hostile macro replay:
  - an auxiliary theorem using plain decide failed to reduce the closed Array
    computation and consequently displayed the elaborator's sorryAx placeholder;
  - the release theorem and a corrected auxiliary theorem use decide +kernel,
    exit zero, and each reports exactly [propext].
  See KERNEL_REPLAY.txt.

3. Manuscript build
-------------------
Command:
  ./build_article.sh
Result: EXIT 0

The script fixes SOURCE_DATE_EPOCH=1788134400 and TZ=UTC.  Two consecutive clean
builds under the toolchain recorded in BUILD_ENVIRONMENT.txt produced the same
PDF hash:
  a2c2280c5b5e786c4749051712f5ce9402972389c2f063d52866802152334f4b

PDF facts:
  - 14 pages;
  - no LaTeX/package warnings, overfull boxes, underfull boxes, undefined
    references, or multiply-defined references in the final log;
  - visual audits covered title/abstract, proof pages, exact-verification page,
    acknowledgments/bibliography, the complete 37-row landscape table, and the
    schema appendix;
  - no clipping or overlap was found;
  - long verifier and theorem identifiers remain intact and readable;
  - no front-page Verification Status or draft banner appears.

The PDF is byte-stable under the recorded TeX Live 2025 environment.  The bundle
does not claim cross-distribution byte identity without a hermetic TeX closure.

4. Release integrity
--------------------
- SHA256SUMS is generated deterministically from the release tree and excludes
  only itself and the export-ignored internal AGENTS.md.
- The verifier requires SHA256SUMS to be a regular non-symlink, raises on every
  traversal error, rejects missing/extra/unsafe paths and file/directory
  symlinks, and checks every digest.
- A core.autocrlf=true checkout replay is required to pass.
- SOURCE_ATTACHMENTS_SHA256.txt preserves the six original Sol Pro attachment
  hashes and safe ZIP census without redistributing the attachments.
- The final git archive is replayed from a clean extraction before delivery.

5. Formalization boundary
-------------------------
Lean checks the complete stored finite algebra and separately proves generic
conditional assembly/colouring lemmas and finite arithmetic.  It does not derive
the semantic hypotheses of assembleProtected_eq from the 74 records, instantiate
a formal global Freudenthal mesh, reconstruct the FE matrices, or perform the
117 decorated-source census.  Those bridges are exact Python and manuscript
arguments.  Affine Sobolev scaling, bounded-patch estimates, and Zhang's
published stages remain mathematical arguments in the article.

FINAL VERDICT
-------------
No concrete fatal or load-bearing mathematical gap was found in the protected
k=4,5 lifting or its integration with the k>=6 result.  All concrete verifier,
claim-boundary, and release-integrity defects found by hostile review were
repaired and regression-tested.  Local verification does not substitute for
external specialist review, publication, or prize acceptance.
