forgo.cloud
Sign in
Repo workspace

forkjoin-ai/gnosis

Lean Transformation Family Plan

docs/LEAN_TRANSFORMATION_FAMILY_PLAN.md
forkjoin-ai/gnosis
Repo overview Open in workbench

Lean Transformation Family Plan

This is a Lean-first plan for the most useful bounded extraction from the anime-inspired ontology: formalize a transformation-family kernel around projection, reinforcement, and a new generic decomposition operator.

The goal is not to canonize anime lore. The goal is to capture one reusable formal substrate that already matches existing Gnosis work and can support new reducers, theorem ids, and cross-domain bridges.

Why This Candidate

This is the best next formalization candidate because:

  • projection already exists in the current Gnosis surface.
  • reinforcement already exists and already feeds useful downstream work, including cancer theorems.
  • decomposition is the missing operator from the same family and is the most natural formal reduction of the anime material.
  • The triad is small enough to mechanize honestly and useful enough to power a deterministic reducer instead of a one-off manuscript note.

The useful claim is simple:

  • projection creates structure,
  • reinforcement amplifies existing structure,
  • decomposition removes structure,
  • featureless states cannot be reinforced until structure is restored.

That last point is already repo-relevant because ../lean/Lean/ForkRaceFoldTheorems/CancerReinforcement.lean proves the same pattern in the oncology domain.

Proposed Lean Surface

Add two new modules:

  • lean/Lean/ForkRaceFoldTheorems/DecompositionTopology.lean
  • lean/Lean/ForkRaceFoldTheorems/TransformationFamily.lean

Keep them small and arithmetic-first. Do not start with franchise examples. Start with finite natural-number witnesses and explicit before/after states.

DecompositionTopology.lean

Define a generic topological object and a decomposition result:

structure TransformObject where
  crossings : Nat
  weight : Nat
  capacity : Nat
  hCapacity : 0 < capacity

structure DecompositionResult where
  residualCrossings : Nat
  releasedWeight : Nat
  residueUnits : Nat

Primary operator:

  • decompose : TransformObject → Nat → DecompositionResult

Where the second argument is a bounded decomposition budget or intensity.

Core semantic intent:

  • decomposition never increases crossings;
  • full decomposition can drive crossings to zero;
  • released weight and residue are non-negative;
  • decomposing a featureless object is idempotent.

TransformationFamily.lean

Import:

  • ReinforcementTopology
  • DecompositionTopology
  • optionally LiftProjectionCore only if the projection bridge actually needs it; do not import it by default if simple arithmetic witnesses suffice.

Define:

inductive TransformationMode
| projection
| reinforcement
| decomposition

structure TransformationWitness where
  beforeCrossings : Nat
  afterCrossings : Nat
  beforeWeight : Nat
  afterWeight : Nat

Use this module to state the pairwise relations between the three operator families without re-proving the full reinforcement surface.

Theorem Scope

Keep the first pass to 6-8 theorems total.

DecompositionTopology.lean

Planned theorem set:

  • decomposition_does_not_increase_crossings residualCrossings ≤ object.crossings
  • full_decomposition_yields_featureless full budget on a finite object yields residualCrossings = 0
  • decomposition_releases_nonnegative_residue releasedWeight and residueUnits are non-negative by construction
  • featureless_decomposition_idempotent decomposing an already featureless object preserves the featureless result

TransformationFamily.lean

Planned theorem set:

  • projection_adds_structure re-export or restate the existing projection witness in the family language
  • reinforcement_preserves_structure re-export or restate the existing reinforcement witness in the family language
  • decomposition_removes_or_preserves_structure decomposition cannot add crossings
  • projection_reinforcement_exclusive a single witness cannot both create crossings and preserve crossings
  • reinforcement_decomposition_exclusive a single witness cannot both strictly preserve and strictly reduce crossings
  • featureless_states_cannot_reinforce if beforeCrossings = 0, reinforcement cannot be the correct mode
  • decompose_then_reinforce_requires_restoration once a full decomposition yields zero crossings, any subsequent successful reinforcement requires an intermediate structure-restoring step

That last theorem is the practical bridge back to cancer reinforcement and is the main reason this family is useful.

TypeScript Mirror and Reducer

After the Lean layer exists, add one runtime mirror:

  • src/transformation-family-formalization.ts

Do not make it a sprawling ontology parser. Make it a deterministic reducer that classifies already-normalized transformation examples into the three families and emits theorem ids plus simple counts.

Suggested shape:

export type TransformationFamily =
  | 'projection'
  | 'reinforcement'
  | 'decomposition';

export interface TransformationFamilyInput {
  readonly id: string;
  readonly beforeCrossings: number;
  readonly afterCrossings: number;
  readonly beforeWeight: number;
  readonly afterWeight: number;
}

export interface TransformationFamilyEntry {
  readonly id: string;
  readonly family: TransformationFamily;
  readonly featurelessBefore: boolean;
  readonly featurelessAfter: boolean;
}

export interface TransformationFamilyBundle {
  readonly theoremIds: readonly TransformationFamilyTheoremId[];
  readonly entries: readonly TransformationFamilyEntry[];
  readonly aggregate: {
    readonly projectionCount: number;
    readonly reinforcementCount: number;
    readonly decompositionCount: number;
    readonly featurelessCount: number;
  };
}

Suggested theorem ids:

  • THM-TRANSFORMATION-PROJECTION-ADDS-STRUCTURE
  • THM-TRANSFORMATION-REINFORCEMENT-PRESERVES-STRUCTURE
  • THM-TRANSFORMATION-DECOMPOSITION-NONINCREASING
  • THM-TRANSFORMATION-PROJECTION-REINFORCEMENT-EXCLUSIVE
  • THM-TRANSFORMATION-REINFORCEMENT-DECOMPOSITION-EXCLUSIVE
  • THM-TRANSFORMATION-FEATURELESS-CANNOT-REINFORCE
  • THM-TRANSFORMATION-DECOMPOSE-THEN-REINFORCE-REQUIRES-RESTORATION

Planned Consumer Value

This is worth doing only if it pays rent outside the manuscript layer.

Immediate consumer value:

  • gives the anime-inspired ontology one honest reduced substrate;
  • supplies a reusable classifier for future cross-domain notes;
  • tightens the conceptual bridge from reinforcement magic to cancer reinforcement without adding franchise-specific canon;
  • creates a small formal vocabulary that future reducer bundles can use instead of inventing ad hoc operator names.

Likely downstream consumers:

  • FORMAL_LEDGER.md once promoted;
  • any future ontology-reducer note;
  • cross-domain theorem composition that needs to distinguish create / amplify / dismantle operations.

Out of Scope

Do not include these in the first implementation:

  • full anime universe matrices;
  • source-typology taxonomy across every franchise;
  • strategic-scale tiering;
  • expository examples inside Lean types or theorem names;
  • transmutation as a fourth operator unless decomposition is already stable.

If transmutation becomes useful later, model it as a composition built on top of decomposition plus reconstruction, not as day-one surface area.

Implementation Order

  1. Add DecompositionTopology.lean with the bounded arithmetic kernel and four theorems.
  2. Add TransformationFamily.lean as the bridge module over projection, reinforcement, and decomposition.
  3. Add src/transformation-family-formalization.ts with theorem ids and deterministic classification.
  4. Add a focused test file for the reducer only after the bundle shape is fixed.
  5. Add one short canonical summary to FORMAL_LEDGER.md only if the Lean and reducer surfaces both exist.
  6. Let Aeon link to the Gnosis summary only after Gnosis promotion.

Verification Plan

Lean:

  • module compiles sorry-free;
  • theorem names are stable and exported through the usual Gnosis surface;
  • no new axioms or placeholders.

TypeScript:

  • deterministic bundle generation from fixed inputs;
  • theorem ids appear in the bundle;
  • family classification is stable across repeated runs;
  • featureless cases classify correctly.

Docs:

  • the canonical ledger summary stays short and substrate-neutral;
  • franchise names, if preserved at all, stay outside the canonical theorem surface.

Success Criteria

This plan is successful if it yields all of the following:

  • one new operator family that the repo does not already have (decomposition);
  • one small bridge module that unifies the three transformation modes without duplicating existing theorem families;
  • one deterministic reducer bundle with stable theorem ids;
  • zero dependence on franchise-specific canonical naming.

If that cannot be achieved cleanly, the topic should remain a docs note rather than being promoted into the formal ledger.