Maximus Gorog
|
ba0a49823b
|
Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries
Initial commit. Six modules extracted from
cubical-transport-hott-lean4/CubicalTransport/Algebra/ and
re-namespaced as `Infoductor`:
- Foundation/Meta.lean — MetaCType, MetaClassifier,
MetaArtifact, MetaPosition
(with manual mutual decEq for
MetaClassifier's recursive
lattice arms)
- Foundation/Edit.lean — Edit monad + Context comonad +
distributive law +
MetaClassifier.atPosition
with lattice laws as theorems
- Foundation/Restructure.lean — universal `restructure` (5-field
comp-shaped operation), 6 frozen
aliases, headless apply +
brokenRefs / selfConsistent /
Edit.guarded
- Foundation/MacroAlias.lean — @[macroAlias] attribute +
EnvExtension registry
- Foundation/MetaPath.lean — @[metaPath src target]
attribute + registry +
findPathsFromSource/ToTarget
- Foundation/Methodology.lean — @[methodology classifier]
attribute + registry +
deriveByTransport (walks
metaPath registry) +
tryEntryAsClosed primitive +
cubical_search reference
demonstrator
Builds clean on lean4 v4.30.0-rc2, ten oleans. No deps beyond
Lean stdlib. Sub-libs Tactics / Pantograph / Runner are planned
under the same lakefile.toml but not yet implemented.
Pairs with Pantograph as the conductor sits atop the pantograph
on an electric train. "Info-ductor" — conducts information
(structure / classifications / methodology) through a Lean
codebase.
Forgejo: http://maxgit.wg:3000/max/infoductor
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
2026-05-01 07:20:36 -06:00 |
|