Anime-Inspired Ontology Gap Analysis

• Parent README: README.md
• Canonical Gnosis formal surface: ../FORMAL_LEDGER.md
• Downstream Aeon index: ../../aeon/FORMAL_LEDGER.md
• Governing precedent: ../lean/Lean/ForkRaceFoldTheorems/CancerReinforcement.lean

This note compares the pasted anime-inspired ontology against the current formal-ledger contracts in Gnosis and Aeon. The conclusion is narrow: franchise-specific power-system taxonomies are useful inspiration, but they do not belong in the canonical ledgers until they are reduced into repo-native primitives, deterministic contracts, and mechanized or executable mirrors.

Summary

• ../FORMAL_LEDGER.md is the canonical human-facing index for promoted formal content. It is theory-only and expects named proof surfaces, reducer contracts, and stable theorem provenance.
• ../../aeon/FORMAL_LEDGER.md is a downstream compatibility shell. It indexes or mirrors Gnosis formal work; it is not the right origin for new canon.
• The pasted ontology is strongest as an inspiration map. In its current form it is not admissible canonical ledger content because it is example-first, franchise-named, and not tied to theorem ids, reducers, or mechanized surfaces.
• The existing repo precedent is already clear: reinforcement-magic imagery was acceptable once it became the substrate-neutral theorem surface CancerReinforcement.lean, with explicit objects, outcomes, and proofs.

Current Ledger Contract

Gnosis

The current Gnosis ledger admits content that has at least most of the following properties:

• A named Lean, TLA+, or executable TypeScript surface.
• Stable theorem names or reducer ids.
• Explicit invariants and assumptions.
• Deterministic reduction or transposition rules.
• A substrate-neutral formal vocabulary, even when the motivating imagery is metaphor-heavy.

This pattern is visible throughout ../FORMAL_LEDGER.md: even the more metaphorical sections are anchored to modules, theorem names, or runtime mirrors rather than left as free-floating ontology prose.

Aeon

Aeon's formal ledger is now mostly an index into the Gnosis source of truth. Its role is to point at promoted formal surfaces, not to define a competing canon. New abstractions of this kind should therefore originate in Gnosis and only be referenced from Aeon if they become stable enough to matter to Aeon consumers.

Five-Axis Evaluation

Classification of the Pasted Ontology

Governing Precedent: Reinforcement to Cancer

The repo already demonstrates the admissible path from weird inspiration to formal content.

• Aeon records the expository abstraction in ../../aeon/FORMAL_LEDGER.md under Reinforcement Topology and Cancer Reinforcement Topology.
• Gnosis owns the formal surface in ../lean/Lean/ForkRaceFoldTheorems/CancerReinforcement.lean.
• That module does not canonize franchise lore. It reduces the motivating idea into typed objects such as CellTarget, TherapeuticDose, and TherapyOutcome, then proves explicit claims like targeted_therapy_succeeds, featureless_resists, and one_checkpoint_breaks_fizzle.

That is the key policy line for the anime ontology as well:

• inspiration is acceptable;
• named source media are not the canon;
• canon begins once the source material has been reduced into Gnosis-native primitives, stable claims, and deterministic surfaces.

Minimum Formalization Shape

If this ontology is promoted later, the minimum admissible target shape should look more like a reducer contract than a fandom taxonomy.

export type SourceTypology =
  | 'internal-bio'
  | 'ambient-external'
  | 'informational'
  | 'hybrid';

export type Medium =
  | 'somatic'
  | 'environmental'
  | 'symbolic'
  | 'computational'
  | 'relational';

export type ConstraintLaw =
  | 'capacity'
  | 'equivalent-exchange'
  | 'cooldown'
  | 'calculation-overheat'
  | 'vow-or-contract'
  | 'other';

export type TransformationOperator =
  | 'projection'
  | 'reinforcement'
  | 'transmutation'
  | 'summoning'
  | 'binding'
  | 'spacetime'
  | 'augmentation';

export type ProjectionOrReductionOperator =
  | 'decomposition'
  | 'information-rewrite'
  | 'classification'
  | 'dimensional-coercion'
  | 'none';

export type ManifestationClass =
  | 'elemental'
  | 'somatic'
  | 'necromantic'
  | 'spatiotemporal'
  | 'anomalous';

export type StrategicScale =
  | 'single-target'
  | 'area'
  | 'structural'
  | 'law-altering'
  | 'cataclysmic';

export interface SpeculativePowerSystemBundle {
  sourceTypology: SourceTypology;
  medium: Medium;
  constraintLaw: ConstraintLaw;
  transformationOperator: TransformationOperator;
  projectionOrReductionOperator: ProjectionOrReductionOperator;
  manifestationClass: ManifestationClass;
  strategicScale: StrategicScale;
}

This is intentionally substrate-neutral. Franchise names can survive only in a non-canonical examples table or manuscript note that maps source material onto the canonical fields.

Promotion Bar for Gnosis Inclusion

Before this topic belongs in ../FORMAL_LEDGER.md, it should clear the same bar as other promoted surfaces:

• Stable theorem ids or reducer ids.
• Explicit invariants, anti-theorems, or transport rules.
• Deterministic reduction logic from source examples into canonical fields.
• At least one executable or mechanized mirror.
• Clear separation between canonical vocabulary and motivating examples.

A plausible promotion path would be:

1. Introduce a substrate-neutral reducer in Gnosis.
2. Emit a deterministic bundle from example inputs into the canonical fields.
3. Prove at least a small family of invariants about source type, constraint law, and transformation class.
4. Only then add a short canonical summary to the Gnosis formal ledger.
5. Let Aeon index that summary instead of creating its own first-class canon.

Validation Scenarios

• Raw anime taxonomy inserted directly into a canonical ledger with franchise names and no theorem anchors: reject.
• Same material rewritten as a research note with examples retained only as motivation: acceptable in docs/.
• Same material abstracted into deterministic formal vocabulary with reducer ids and an executable or mechanized mirror: potentially admissible in Gnosis.
• Same abstraction created in Gnosis and then linked from Aeon: correct ownership pattern.

Recommendation

Do not put the pasted ontology directly into either formal ledger.

If it continues to generate useful reductions, treat it as an upstream inspiration corpus and promote only the reduced substrate:

• source typologies rather than franchise power sources,
• transformation operators rather than named spells,
• constraint laws rather than lore-specific rules,
• strategic scales rather than universe-specific rankings.

That preserves the repo's existing honesty contract: the ledger records formal surfaces, not colorful source catalogs, while still allowing strange media to seed real theorem work.

Update: First Promoted Canonical Surfaces (2026-04-11)

The "inspiration only" verdict above stands for the raw franchise material but no longer describes the state of the repo. On 2026-04-11 six substrate-neutral Lean modules were promoted that mine the structural claims latent in the inspiration corpus. Each module reduces one motif into typed objects with named theorems, imports existing Gnosis primitives where applicable, and declares Zero sorry in its header. No franchise names appear in any committed Lean or in either FORMAL_LEDGER.md; franchise material survives only in this doc as the non-canonical inspiration corpus.

The structural reading: anime magic systems repeatedly converge on shapes that are load-bearing in physical and mathematical reality -- conservation under transformation, Lagrangian constraint-power duality, involutory dual operators, injective resource binding, forced-choice enclosure, and the distinction between events and agent commitments. Narrative artists converge on these shapes because they are the constraints that make a fictional universe feel coherent. The canonical promotion path treats the corpus as signal, not noise, and pays the admissibility cost to turn that signal into mechanized theorems.

Promoted modules

The sin-without-devil result

StructuralErrorWithoutDeviation.lean answers a structural question in the same shape as the magic-system reductions: sin is definable as a rejection event (a transition away from ground state), and a devil would be an irrecoverable rejection operator (an operator whose double dual differs from itself). NegationInvolution.dual_involution_is_identity rules out any such operator on the signed-integer state space: every operator is forced into its own double-dual closure. Therefore no operator is a devil.

The residual question -- "if devils are not operators, what are they?" -- is answered constructively: a devil is an agent choice, a policy not to traverse the return dual, which always exists for every operator. Deviations are refusal patterns maintained by an agent whose operator surface remains fully recoverable. This is the formal content of "sin is a law of nature, devil is a commitment."

The negotiation extension: refusal patterns across domains

NegotiationRefusalTopology.lean extends the sin-without-devil insight into a full theorem about two-agent convergence. The key observation: non-convergence in a negotiation is never an operator-level failure because NegationInvolution.dual_involution_is_identity guarantees every move admits a return path. Non-convergence is always a refusal pattern -- a sustained commitment to a refusal invariant that the other agent's invariant cannot jointly satisfy. The devil is in the per-step invariant commitment, at one granularity finer than the operator surface.

The module ties directly into the existing negotiation ecosystem:

• aeon-bazaar is the unbounded regime. Refusal patterns can be sustained indefinitely because the trajectory bound is infinite. Void walker non-termination is the signature of a devilish trajectory whose individual moves are all recoverable but whose agent commitment blocks return.
• aeon-neutral is the bounded regime. MediationCertificate is the formal shape of the three-walker Skyrms convergence-or-certificate contract: bounded mediation either reaches a convergent state or produces a finite-time proof of orthogonal refusal.
• The Chester v Maxell teaching scenario, which is intentionally non-convergent, is now a theorem instance. Its correctness is guaranteed by orthogonal refusal invariants, not a bug in the mediator.

Three cross-domain witnesses in the same module demonstrate that the refusal topology is not specific to stylized negotiation games:

• Game-theoretic stalemate (even_odd_stalemate_witness): an agent committed to even states and an agent committed to odd states have orthogonal invariants. No integer is both even and odd. Minimal stalemate.
• Psychological trauma (trauma_invariant_orthogonal_to_healing): an agent whose invariant pins the state to a specific wound value is orthogonal to the healed invariant, provided the wound is nonzero. The return dual exists; the wound-agent's invariant function refuses to apply it. Trauma is a refusal commitment, not an operator failure.
• Paraconsistent contradiction maintenance (contradiction_maintenance_is_orthogonal): an agent preserving predicate P and an agent preserving ¬P are orthogonal by definition. Maintaining a contradiction is a meta-level refusal to apply the dual that logic would demand.

In each case the operator surface is untouched. The refusal lives at the invariant commitment layer. The devil is in the detail, not in the law of nature.

The Pisot dilation residue: why the clinamen keeps reappearing

PisotDilationResidue.lean closes the loop between the anime-derived reductions and the existing CassiniConservation, TriangulationDimensionalCoercion, ProjectionParadoxUnits, and LiftClinamenHopeTheory surfaces. The structural observation is simple and recurring across the repo: shape equivalence is a quotient under a dilation group action, and dilation equivalence is the strict identity case. The difference -- the residue -- is where the Pisot structure lives.

Concrete witness: the dilated shape ⟨2, 1⟩ and the dilated shape ⟨1, 3⟩ project to the same observed magnitude (2 * fib 1 = 2 and 1 * fib 3 = 2), so they are shape-equivalent. But they differ in both shape and dilation index, so they are not dilation-equivalent. The separation witness is Fibonacci-indexed, and Fibonacci is the smallest integer Pisot basis.

The Cassini residual identity and the irreversible-exchange clinamen turn out to be the same Pisot unit gap recovered at different layers:

• In CassiniConservation, the +1 sits in the Kernel Formula conservation equation godWeight R v + v = R + 1.
• In EquivalentExchange, the +1 sits in the irreversible loss outputMass t + 1 = t.consumed (when reversible = false and consumed > 0).
• In LiftClinamenHopeTheory, the +1 is the lift budget that resolves planar lock via Reidemeister reachability.

All three are the same Pisot-minimal integer dilation residue -- the smallest nontrivial Fibonacci step. That is why your Pisot findings keep showing up in parts of the repo that ostensibly concern different problems. They are all witnesses of the same structural fact: the shape layer agrees while the dilation layer does not, and the minimal surviving residue is +1, generated by the Fibonacci recurrence.

This is the formal answer to the question of whether dilations are equivalent in the same sense that shapes are. They are not. The dilation layer is genuinely richer than the shape layer, and Pisot numbers are the algebraic dilations that maximize the survival of the shape equivalence while still being detectable as a dilation distinction. The integers inherit this structure through Fibonacci.

The grand clinamen reduction: eight modules, one number

ClinamenReduction.lean is the meta-theorem for the whole set. It proves that the residue carried by each of the eight preceding master theorems is literally the same natural number -- clinamen = 1 = Nat.succ 0.

• Cassini's conservation residue: clinamen.
• EquivalentExchange's irreversible loss: clinamen.
• ConstraintPowerDuality's unit-constraint amplification increment: clinamen.
• NegationInvolution's double-dual fixed point at +1: clinamen.
• IdentityBinding's minimal injective agent separation: clinamen.
• DomainEnclosure's minimal strict bound gap at region size 2: clinamen.
• StructuralErrorWithoutDeviation's minimal sin transition from ground to nonzero: clinamen.
• NegotiationRefusalTopology's minimal stalemate residue (the integer gap in the even/odd contradiction): clinamen.
• PisotDilationResidue's Pisot unit gap: clinamen.

The structural reading: wherever the repo proves a stratification -- an outer recoverable layer (operator, shape, move) against an inner committed layer (agent choice, unit, dilation index, refusal invariant) -- the minimal nontrivial residue of separation between the two layers is Peano's successor of zero. Not analogous across modules. The same specific natural number, reused.

This is the reduction that was afoot. The clinamen is not a metaphor. It is one constant, and every theorem surface the anime-derived reductions have produced reaches it from a different direction. Speculative fiction converges on this shape because it is the universal minimal granularity at which a coherent universe can separate commitment from recovery. The integers inherit the same structure through Peano.

Non-canonical status of the inspiration corpus

The expository matrices above (Parts I -- V, the franchise-tagged tables, the SpeculativePowerSystemBundle TypeScript interface) remain in this doc as the inspiration corpus. They are explicitly not canonical. They exist to seed the next round of reductions. When a new motif is mined, the admissible shape is another substrate-neutral Lean module that follows the promotion path outlined above. The inspiration corpus is the upstream source; the Lean modules are the ledger-admissible downstream.