lean4/Hypermath/TransportCountermodel.lean proves that the 38 currently
declared logical clauses do not entail the reproduction needed for the
conditional path-transport construction, even after
adding the current self-derivation proposition and its stronger two-step
cycle certificate. Both related starting forms in the counterexample are
generated by finite primitive forming from ground.
This is a result about the present formalization. The model's relation named
Simulation fails the stronger source description of mutual continuation
reproduction. That mismatch identifies operational content the declared
clauses have not captured; it does not refute the author's intended concept.
Forms are six distinct values. Primitive forming f2f and the labels defining
simulation are:
| Form | Next form | Simulation class | Position from ground |
|---|---|---|---|
a0 |
a1 |
0 | 0 |
a1 |
a2 |
1 | 1 |
a2 |
a3 |
2 | 2 |
a3 |
a4 |
1 | 3 |
a4 |
a3 |
1 | 4 |
limit |
limit |
3 | Not reached by finite forming from ground |
Class labels and finite positions are dimensionless natural numbers. The
labels are not ordinals or arithmetic truth ranks. Ground is a0, and the
deriver is a3. Simulation means equality of the displayed class labels;
simulation_is_equivalence proves reflexivity, symmetry, and transitivity.
Similarity (~~) and congruence (=~) are universal in this model.
Simulation (==) remains a separate, narrower relation.
Every forming edge is admitted by DStep, because its congruence guard is
true. The deriver's actual path a3 -> a4 -> a3 preserves simulation at both
steps and closes. cycleWitness constructs the same three fields as the
native DriverCycleWitness: a simulation path, its actual length of two,
and endpoint simulation closure. self_derivation_holds separately proves
all four conjuncts of the current selfDerivation proposition.
Nevertheless, a1 and a3 have the same simulation label, while the witnessed
step a1 -> a2 has no finite reproduction from a3 whose endpoint
simulates a2. Every finite path from a3 stays in {a3, a4} and hence in
class 1; a2 belongs to class 2. The theorem path_stays_in_cycle proves the
invariant by induction over the actual path. no_finite_reproduction includes
all finite lengths, including zero. It is not inferred from the bounded probe.
Thus allowing several forming steps instead of one does not, by itself, repair this particular declared model. Either the relatedness evidence or the admissible continuation semantics must impose a stronger constraint. No claim is made here about transfinite reproduction or different next-layer carriers and operations.
FullAxioms repeats the exact 38 native logical clause types under the model's
parameter interpretation, and full_axioms_hold supplies every field. The
software checks compare those types against the reviewed native declarations.
A further contract check compares the cycle-witness fields, the one-step
transport law, and the self-derivation proposition with their native sources.
The model also interprets the opaque path and ordinal parameters. In
particular, ordinalSucc takes ground to a1 and every other form to ground.
It satisfies the declared axSuccExtends clause: its result is derivable under
the model's endpoint-congruence definition and is not simulation-equivalent
to its input. It does not satisfy the additional proposal equating ordinal
successor with primitive forming. That proposal is not one of the 38 clauses.
Neither these parameters nor their names supply an ordinal interpretation.
The joint theorem full_model_with_cycle_without_reproduction puts all of
the following into one certificate: the 38 clauses, the original target,
the stronger cycle witness, both finite ground-generation witnesses, the
related starting forms, the original derivation step, and absence of any
finite reproduced endpoint. Empty derivation structure, a missing cycle, or
an unreachable starting form cannot explain away this result.
The layer reporter requires 15 new dependency records, including that joint theorem and its construction. They use only Lean's built-in propositional extensionality and quotient soundness where reported; no native Hypermath assumption or admitted proof is used. The source is bound by its reviewed digest, and missing model, cycle, or obstruction reports invalidate the audit. Existing native assumptions and admissions are unchanged.
The source specifies more than a returning endpoint:
| Source statement | Required bridge content | Current evidence |
|---|---|---|
| Chapter 24 makes completed trajectories the atoms of the next grammar and retains their formation history | Reify the whole checked trajectory, with its layer and recoverable derivation | PathLayers retains supplied witnessed paths; native generation of the representation remains open |
| Chapter 36 distinguishes generative meta-closure from zero-order self-verification | Generated structure must participate in subsequent applications of the operation | The existing two-step cycle alone does not establish this generative correspondence |
| The relations source describes simulation as mutual reproduction of paths and futures | Explain which continuations and observations are preserved, and construct their correspondence | PathTransport supplies finite preservation conditional on a transport operation; the native operation remains unconstructed |
These are documented design requirements, not newly proved native laws.
The first two statements allow the next layer to have a different carrier.
They do not require compressing every trajectory into an unchanged base
Form, or identifying kernel self-derivation with sequencing identity.
Similarity (~~), congruence (=~), and simulation (==) keep their source
meanings; the following interpreter symbols do not establish a translation.
A September 12, 2026 read-only probe refreshed the previously documented
boundary in the live precursor interpreter.
Its ordinary grammar-schema path compares normalized endpoint strings (=),
unwrapped bases (≡), or lexical overlap/unwrapped bases (~). The source
README calls the general axiom checks a computational approximation.
In this implementation = is string equality; it is not a certificate of
Hypermath simulation, path identity, or mutual continuation reproduction.
Each case used layer="grammar", universe U, ground $, operator □,
terminals a, $, U, nonterminal S, and the sole rule S -> a.
The listed chain was supplied as derivation_chain to
HypergrammarInterpreter.evaluate_source.
| Supplied chain | is_valid |
closed_form |
Reported relation |
|---|---|---|---|
$, □($), □(□($)) |
True | True | ≡ |
$, □($), □(□($)), $ |
True | True | = |
$, UNJUSTIFIED_STEP, □($), □(□($)), $ |
True | True | = |
$, □(□($)), □($), $ |
True | True | = |
All five reported checks were true in each case. The inserted term and reordered interior do not cause a rejection. This reproduces the endpoint boundary; it does not newly discover a proof-system defect or establish that the schema was specified as an executable derivation. The separate Metamath proof-execution path was not exercised in this refresh, and these results make no claim about its correctness or the validity of native derivations.
The probe ran with a 60-second process limit and bytecode writing disabled.
All eight Python source-file hashes remained unchanged. Exact inputs, results,
and source digests are in the local evidence file
build/live-closure-probe.json, SHA-256 1c233d20d0b83533ad534e66a4bbbf1c30931cd19ee24d5a9a6481692bd8090f.
The source snapshot is external to the Hypermath native audit and package pin.
A simple design check rules out an inadequate replacement for simulation.
Suppose the only transitions are x -> f(x) for a total unary function f,
and no observations or guards are required to agree. Relate every pair of
states. For any step from x, the step from any y reaches f(y), and the
two successors are again related. The same argument works in reverse.
Thus this universal relation satisfies that bare mutual step-matching rule.
This argument concerns unguarded, unobserved transitions, not the native
guarded DStep, and is not an assertion that native simulation is universal.
It shows why simply adding a generic step-matching definition would not
recover the intended distinctions. Verification geometry must supply the
observations or admissibility conditions that exclude inappropriate matches,
as well as evidence for reproducing the permitted paths. No particular
observation semantics is selected by this note.
On September 12, the author specified: "A cycle in the inner self-derivation core/kernel with pathway through the ground or self-derivation roots." This identifies the kernel/root pathway as part of the intended verification geometry. It does not, by itself, specify whether the connection is directed both ways, how a relational return is traversed, or whether routing steps are observationally silent. The following is a proposed concrete interpretation.
For a chosen root r, retain actual checked paths r ->* x and x ->* r
for each participating form x. Here ->* means a finite path of justified
edges, including an empty path; a nontrivial cycle additionally requires
positive length. Given forms x and y with these witnesses, and an original
continuation p : x ->* z, construct:
y ->* r ->* x ->* z.
The first two segments are the supplied inward route from y and outward
route to x. The final segment is exactly p, with the same endpoint z.
This computes a replay from witnessed routes; it does not assume an arbitrary
transport operation. Swapping x and y gives the converse construction.
The additional routing is retained explicitly. For example, in the cycle
r -> a -> b -> r, the continuation a -> b can be replayed from b as
b -> r -> a -> b.
The local draft build/RootedContinuationDraft.lean checks six theorem
dependency reports. It proves exact retention of the continuation's edges
as a suffix, the added route length, compatibility with subsequent path
composition, and exact recovery of the grouped used routes and continuation
through any finite number of existing representation lifts. Three reports
use no axioms; three use only Lean's propositional extensionality. A concrete
three-vertex example also passed after four lifts. The proof was checked with
lake env lean ../build/RootedContinuationDraft.lean from lean4, with a
60-second process bound. Its SHA-256 digest is ef6d4d1d29a14e80117d5c7fb734348a7eecca5ed23e3e73eaeb7d5327635377.
The draft also proves that the countermodel's pair a1, a3 cannot both
carry such two-way routes through any common root. A route from a3 to a1
would contradict the already proved cycle invariant. Mere generation from
ground was insufficient; this candidate requires actual return and outward
paths for each participant. Naming a3 as a root alone does not supply them.
This is a checked finite candidate, outside the production native audit and
package. It does not construct native kernel roots or their paths, identify
the candidate with native simulation ==, or prove that additional routing
is invisible to every continuation. The lifted surface retains the routes
used for this replay; packaging both complete input cycle certificates as
reusable native forms remains further work. A literal return to ground is
not inferred from a similarity statement. The author's broader root pathway
may require a different transition or relational-return representation.
The preservation theorems remain usable once an appropriate reproduction
operation is supplied. The next native step is to derive evidence of mutual
continuation reproduction from the intended verification geometry, with
an explicit observation relation and a rule for corresponding steps or
subpaths. It must exclude the pair a1, a3 in this model as mutually
reproducing, or supply genuinely different admissible continuation structure.
The choice between one-for-one reproduction, finite subpath reproduction, or a richer ranked rule remains open. The model adds no new native axiom, changes no source relation, and establishes no arithmetic completeness result.