This directory is an incomplete Lean 4 translation of the native .hm files.
The pinned toolchain is Lean 4.14.0. A successful compilation accepts declarations
containing sorry; it does not establish their conclusions. Native FORM labels
in source comments record the .hm classification, not completed Lean proofs.
From this directory, run:
python -u audit.py
The command prints source counts, performs a verbose build, reports the transitive
axiom dependencies of selected central declarations, checks independent finite
countermodels, finite traces, observations, and models of all logical clauses,
including the required finite-action countermodel. Each subprocess
has a 60-second timeout, output streams as
it arrives, and a silent subprocess receives a progress observation after 40 seconds.
Use --timeout 90 to adjust the bound or --lake PATH to select the Lake executable.
--inventory-only --details lists every declared assumption without running Lean.
Exit meanings:
0: the audited checks passed and no admitted proof was found in those surfaces.1: a build, tool, dependency report, or countermodel check failed.2: admitted theorem proofs remain; this is the current expected proof-gate result.124: a subprocess exceeded its time bound.Even exit zero would not prove the consistency or arithmetic completeness of the declared axioms, the soundness of the native language, or fidelity of every translation.
The original checkout failed to compile. Bodyless Lean opaque declarations
requested Inhabited defaults; they were replaced by explicit axiom declarations
for the source's uninterpreted type, function, and predicate parameters. This
exposes their assumed status. No admitted theorem was changed into a new axiom.
The original 29 parameter declarations are now explicit assumptions. Two further
source-backed projections, pathStart and pathEnd, express the actual endpoint
clause of L3_ordinatics.hm:97–99; the earlier translation confused path objects
with Forms and path length with the endpoint. No endpoint equations were invented.
The remaining 38 declarations are the translation's logical axiom clauses.
The finite-trace repair subsequently replaces
the D parameter with its finite congruence-preserving witness definition.
It constructively proves dIsReflexive without changing its proposition-level API.
The subsequent finite arithmetic repair
defines the finite ground closure and refutes the universal ground-spanning
claim. There are now 29 source parameters, 38 logical clauses, and 16 admissions.
The latest three admissions were withdrawn after a full-clause countermodel
refuted their entailment. Their original propositions remain as
ordinalZeroIdentityClaim, ordinalSuccAppliesClaim, and
pathLengthArithmeticClaim; they were not proved or replaced by new axioms.
Missing external ℕ/iteration notation was replaced by Lean core Nat and
Nat.repeat. orbitStructure now uses the already declared traceLevels axiom
for its third pair, rather than applying symmetry to a proposition with the wrong
endpoints. The attempted reverse-filtration argument in
plusAndAdditionallyAreDistinct remains an explicit open proof premise.
Countermodels.lean imports only the generic, axiom-free Hypermath.Trace module
and declares no custom axiom or admitted proof. It constructs a Boolean model
of all 24 logical L0/L1 axiom clauses:
similarity and congruence are universal, simulation is equality, application maps
every element to true, and ground is false. In that model:
Derives is symmetric, contradicting the advertised directionality consequence;A second model uses three forms, equality for congruence and simulation, and
application 0 ↦ 1, 1 ↦ 2, 2 ↦ 1. It satisfies the same prefix but has no
congruence-preserving application edge. Its trace-defined D is equality, so
ground does not reach every form even though the deriver 1 returns after two
applications. The earlier unconstrained-D reflexivity probe has been replaced;
it would no longer model the current definition.
These are missing-implication witnesses for the stated prefix. They are not models of all later L2/L3 assumptions and do not refute every possible completion of the intended theory. Future changes to those axiom clauses require updating and reviewing the countermodel correspondence.
FullAxiomModel.lean separately checks all 38 declared logical clauses in an
explicit two-chain interpretation. It excludes admitted theorems and stronger
prose glosses; its vacuous upper-bound implication and opaque path endpoints
make the remaining specification gaps visible. ObservationChecks.lean checks
that endpoint-only observations can lose path length while retained traces keep it.
Hypermath/FiniteAction.lean proves that finite addition and multiplication
respect equality of ground-orbit numeral representations without an injectivity
assumption. It also gives a surjective encoding of the witnessed finite orbit;
an explicit numeral-injectivity premise yields checked two-sided encode/decode
laws and implies the global compatibility condition. Its stronger exact-action
criterion concerns every starting Form: equal numeral
Forms must induce equal iterates on all of them. The existence direction uses
classical choice, is noncomputable, and remains conditional on that criterion.
Agreement through a relation requires the corresponding compatibility; the
generic necessity theorem takes symmetry and transitivity as explicit premises.
FiniteActionCountermodel.lean checks all 38 clauses on six Forms. Ground enters
a two-cycle while the limit lies in a separate three-cycle. Congruent is an
explicit equivalence relation. The first and third numeral Forms coincide,
yet their actions on the other cycle differ even modulo Congruent. Thus neither
an exact nor a congruence-valued action can agree with every finite iteration
on every Form in this model. The same model refutes the three retained
computation claims. It also satisfies the exact current selfDerivation
proposition, proving that this target does not entail those arithmetic bridges.
It does not encode the stronger unformalized native intent
that all Forms arise from ground, and does not refute finite-orbit addition or
multiplication.
The audit binds 34 proved production milestone declarations and their reviewed
dependencies. Its seven required processes are lean_build,
dependency_output, countermodel, finite_trace, observation, full_model,
and finite_action; the last runs the six-form model and its failure witnesses.
Audit.lean prints dependencies without exporting its report as library theorems.
In particular, Hypermath.selfDerivation currently depends on sorryAx through
its admitted components. The file does not remove, discharge, or hide those gaps.