Skip to content

Математическое описание Модели Отношений / Mathematical Description of Relations Model#7

Merged
netkeep80 merged 7 commits intonetkeep80:masterfrom
konard:issue-6-af90e6f6d4c7
Feb 4, 2026
Merged

Математическое описание Модели Отношений / Mathematical Description of Relations Model#7
netkeep80 merged 7 commits intonetkeep80:masterfrom
konard:issue-6-af90e6f6d4c7

Conversation

@konard
Copy link
Contributor

@konard konard commented Feb 4, 2026

Summary

This PR implements the mathematical description of the Relations Model (Модель Отношений) in set theory terms from the perspective of Links Theory (Теория связей).

Fixes #6

Changes

Documentation

  • doc/relations-model-ru.md — Mathematical description in Russian
  • doc/relations-model-en.md — Mathematical description in English

Formal Verification (Rocq/Coq)

  • proofs/rocq/RelationsModel.v — Formal proofs and definitions
  • proofs/rocq/Makefile — Build configuration
  • proofs/rocq/_CoqProject — Coq project file
  • proofs/rocq/README.md — Documentation

CI/CD

  • .github/workflows/rocq-proofs.yml — GitHub Actions workflow for proof compilation with Coq 8.18 and 8.19

Key Mathematical Formalizations

1. Basic Definitions

  • Reference Set: L ⊆ ℕ₀ (natural numbers as unique identifiers)
  • Duplet: D = L² (ordered pair of references)
  • Triplet: T = L³ = {(s, r, o) : s, r, o ∈ L}

2. Relations Model as Four Interconnected Sets

RM = {E, O, R, S}

R ⊆ (S × O) × E
O ⊆ (E × R) × S
S ⊆ (R × E) × O
E ⊆ (O × S) × R

3. Triplet to Duplet Reduction (Theorem 3.1)

Triplets can be equivalently represented as nested ordered pairs:

(s, r, o) = ((s, r), o)

The four sets reduce to duplet sets:

RM = {ER, OS, RE, SO}

4. Associative Network Representation (Theorem 4.1)

The Relations Model is a 3D associative network:

λ : L → L³

5. Triune Entity

Each entity is defined by a triplet (s, r, o) implementing the MVC pattern:

  • s (subject) → View
  • r (relation) → Controller
  • o (object) → Model

Proven Theorems

  1. Triplet-Duplet Equivalence — Conversion is lossless
  2. 3D to 2D Network Transformation — Information is preserved
  3. Conjugation Involutivity — Link type conjugation is involutive

References

Test Plan

  • Verify Rocq/Coq proofs compile successfully via CI
  • Review mathematical descriptions for accuracy
  • Verify documentation links work correctly

🤖 Generated with Claude Code

konard and others added 2 commits February 4, 2026 19:41
Adding CLAUDE.md with task information for AI processing.
This file will be removed when the task is complete.

Issue: netkeep80#6
This commit implements issue netkeep80#6: Mathematical description of the Relations Model
(Модель Отношений) from the perspective of Links Theory (Теория связей).

Changes:
- doc/relations-model-ru.md: Mathematical description in Russian
- doc/relations-model-en.md: Mathematical description in English
- proofs/rocq/RelationsModel.v: Formal verification in Rocq/Coq language
- proofs/rocq/Makefile, _CoqProject: Build configuration for proofs
- proofs/rocq/README.md: Documentation for the proof files
- .github/workflows/rocq-proofs.yml: CI/CD for proof compilation
- README.md: Added links to new documentation

Key mathematical formalizations:
1. Triplets (tuples of length 3) as nested ordered pairs
2. Relations Model as 3D associative network: λ : L → L³
3. Four interconnected sets {E, O, R, S} equivalent to {ER, OS, RE, SO}
4. Triune entity implementing MVC pattern at language level

References:
- Links Theory: https://habr.com/ru/articles/895896/
- Deep Theory: https://github.com/deep-foundation/deep-theory

Fixes netkeep80#6

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@konard konard changed the title [WIP] Написать математическое описание Модели отношений Математическое описание Модели Отношений / Mathematical Description of Relations Model Feb 4, 2026
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@konard konard marked this pull request as ready for review February 4, 2026 18:48
@konard
Copy link
Contributor Author

konard commented Feb 4, 2026

🤖 Solution Draft Log

This log file contains the complete execution trace of the AI solution draft process.

💰 Cost estimation:

  • Public pricing estimate: $4.230218 USD
  • Calculated by Anthropic: $2.861344 USD
  • Difference: $-1.368874 (-32.36%)
    📎 Log file uploaded as Gist (621KB)
    🔗 View complete solution draft log

Now working session is ended, feel free to review and add any feedback on the solution draft.

@konard konard marked this pull request as draft February 4, 2026 19:03
@konard
Copy link
Contributor Author

konard commented Feb 4, 2026

🤖 AI Work Session Started

Starting automated work session at 2026-02-04T19:03:30.295Z

The PR has been converted to draft mode while work is in progress.

This comment marks the beginning of an AI work session. Please wait working session to finish, and provide your feedback.

konard and others added 2 commits February 4, 2026 20:04
Add before_script and after_script to handle permission issues when
running coqc in docker-coq-action. The docker container runs as
coq user (UID=1000) while GitHub Actions uses different UIDs.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Add .github/workflows/rocq-proofs.yml to the paths filter so CI
runs when the workflow itself is modified.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@konard konard closed this Feb 4, 2026
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@netkeep80 netkeep80 reopened this Feb 4, 2026
The before_script and after_script parameters are not used when
custom_script is specified, as custom_script replaces the entire
execution flow. Move the chown commands inside custom_script.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@netkeep80 netkeep80 marked this pull request as ready for review February 4, 2026 19:18
@netkeep80 netkeep80 merged commit 526396a into netkeep80:master Feb 4, 2026
2 checks passed
@konard
Copy link
Contributor Author

konard commented Feb 4, 2026

🤖 Solution Draft Log

This log file contains the complete execution trace of the AI solution draft process.

💰 Cost estimation:

  • Public pricing estimate: $4.925130 USD
  • Calculated by Anthropic: $3.054800 USD
  • Difference: $-1.870330 (-37.98%)
    📎 Log file uploaded as Gist (447KB)
    🔗 View complete solution draft log

Now working session is ended, feel free to review and add any feedback on the solution draft.

@konard
Copy link
Contributor Author

konard commented Feb 4, 2026

🤖 Solution Draft Log

This log file contains the complete execution trace of the AI solution draft process.

💰 Cost estimation:

  • Public pricing estimate: $4.925130 USD
  • Calculated by Anthropic: $3.054800 USD
  • Difference: $-1.870330 (-37.98%)
    📎 Log file uploaded as Gist (452KB)
    🔗 View complete solution draft log

Now working session is ended, feel free to review and add any feedback on the solution draft.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Написать математическое описание Модели отношений

2 participants